Basic Example of Type Classes as Predicates Over Types
From Impredicative Wiki
(Difference between revisions)
(An example of viewing type classes as predicates over types)
(Example of automatic resolution)
Latest revision as of 09:22, 14 December 2010
Here is a simple example trying to show how type classes can be viewed as predicates over types.
structure Example : sig type socrates type alice type bob type trigger type silver type hidalgo class human class horse class mortal val human_socrates : human socrates val human_alice : human alice val human_bob : human bob val horse_trigger : horse trigger val horse_silver : horse silver val horse_hidalgo : horse hidalgo val humans_mortal : t ::: Type -> human t -> mortal t end = struct (* * We will make some types to represent objects. *) type socrates = unit type alice = unit type bob = unit type trigger = unit type silver = unit type hidalgo = unit (* * Now we use type classes as predicates over these types. *) class human t = unit class horse t = unit class mortal t = unit (* * We use type class instances to say of which types these * predicates are true. *) val human_socrates : human socrates = () val human_alice : human alice = () val human_bob : human bob = () val horse_trigger : horse trigger = () val horse_silver : horse silver = () val horse_hidalgo : horse hidalgo = () (* * Humans are mortal *) fun humans_mortal [t ::: Type] (h : human t) : mortal t = h end open Example (* * The Ur/Web type class facility can check our proof that Socrates is mortal *) val mortal_socrates : mortal socrates = @humans_mortal human_socrates (* * Since the point of type classes is automatic resolution, we can also get the * compiler to find the proof for us. *) val mortal_socrates' : mortal socrates = _ (* * But there is no value we can put on the right to show Hidalgo is mortal *) (* val mortal_hidalgo : mortal hidalgo = () *) fun main () = return <xml> <head> <title>Type Classes as Predicates in Ur/Web</title> </head> <body> <h1>Type Classes as Predicates in Ur/Web</h1> <p> The Ur/Web type class mechanism can represent predicates. </p> <h2> An illustracion </h2> </body> </xml>