Basic Example of Type Classes as Predicates Over Types

From Impredicative Wiki
Revision as of 09:22, 14 December 2010 by Adam Chlipala (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

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>
Personal tools