http://www.impredicative.com/wiki/index.php?title=Basic_Example_of_Type_Classes_as_Predicates_Over_Types&feed=atom&action=historyBasic Example of Type Classes as Predicates Over Types - Revision history2024-03-29T10:07:53ZRevision history for this page on the wikiMediaWiki 1.19.20+dfsg-2.3http://www.impredicative.com/wiki/index.php?title=Basic_Example_of_Type_Classes_as_Predicates_Over_Types&diff=113&oldid=prevAdam Chlipala: Example of automatic resolution2010-12-14T14:22:20Z<p>Example of automatic resolution</p>
<table class='diff diff-contentalign-left'>
<tr valign='top'>
<td colspan='1' style="background-color: white; color:black;">← Older revision</td>
<td colspan='1' style="background-color: white; color:black;">Revision as of 14:22, 14 December 2010</td>
</tr></table>Adam Chlipalahttp://www.impredicative.com/wiki/index.php?title=Basic_Example_of_Type_Classes_as_Predicates_Over_Types&diff=112&oldid=prevKarn Kallio: An example of viewing type classes as predicates over types2010-12-13T23:36:45Z<p>An example of viewing type classes as predicates over types</p>
<p><b>New page</b></p><div>Here is a simple example trying to show how type classes can be viewed as predicates over types.<br />
<br />
<pre><br />
structure Example : sig<br />
type socrates <br />
type alice<br />
type bob<br />
<br />
type trigger<br />
type silver<br />
type hidalgo<br />
<br />
class human<br />
class horse<br />
class mortal<br />
<br />
val human_socrates : human socrates<br />
val human_alice : human alice<br />
val human_bob : human bob<br />
<br />
val horse_trigger : horse trigger<br />
val horse_silver : horse silver<br />
val horse_hidalgo : horse hidalgo<br />
<br />
val humans_mortal : t ::: Type -> human t -> mortal t <br />
end = struct<br />
<br />
(*<br />
* We will make some types to represent objects.<br />
*)<br />
<br />
type socrates = unit<br />
type alice = unit<br />
type bob = unit<br />
<br />
type trigger = unit<br />
type silver = unit<br />
type hidalgo = unit<br />
<br />
(*<br />
* Now we use type classes as predicates over these types.<br />
*)<br />
<br />
class human t = unit<br />
class horse t = unit<br />
class mortal t = unit<br />
<br />
(*<br />
* We use type class instances to say of which types these<br />
* predicates are true.<br />
*)<br />
<br />
val human_socrates : human socrates = () <br />
val human_alice : human alice = () <br />
val human_bob : human bob = () <br />
<br />
val horse_trigger : horse trigger = ()<br />
val horse_silver : horse silver = ()<br />
val horse_hidalgo : horse hidalgo = ()<br />
<br />
(*<br />
* Humans are mortal<br />
*)<br />
fun humans_mortal [t ::: Type] (h : human t) : mortal t = h <br />
end<br />
<br />
open Example<br />
<br />
(*<br />
* The Ur/Web type class facility can check our proof that Socrates is mortal<br />
*)<br />
<br />
val mortal_socrates : mortal socrates = humans_mortal<br />
<br />
(*<br />
* But there is no value we can put on the right to show Hidalgo is mortal<br />
*)<br />
<br />
(* val mortal_hidalgo : mortal hidalgo = () *)<br />
<br />
fun main () = return <xml><br />
<head><br />
<title>Type Classes as Predicates in Ur/Web</title><br />
</head><br />
<body><br />
<h1>Type Classes as Predicates in Ur/Web</h1><br />
<p><br />
The Ur/Web type class mechanism can represent predicates.<br />
</p><br />
<h2><br />
An illustracion <br />
</h2><br />
</body><br />
</xml><br />
</pre></div>Karn Kallio