Basic Example of Type Classes as Predicates Over Types
From Impredicative Wiki
Revision as of 09:22, 14 December 2010 by Adam Chlipala
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>