Disjointness fun - creating records using type level functions

From Impredicative Wiki
Jump to: navigation, search

Example taking 2 names and 2 types then 2 values yielding a record expression illustrating how to use guarded types

 (* Here is a function which takes two names and two types (type level) yielding
    a function taking two values returning a rect
    type level argumenst are surrounded by [].
 *)
 fun twor [a :: Name] [b :: Name]
          (* proof that both names are distinct, note, you don't have to pass
          it, could be put later in the argument list  *)
          [[a] ~ [b]]
          [c :: Type] [d :: Type]
          (* the values (type level stuff end): *)
          (x : c) (y : d)
          (* the return type *)
          : {a : c, b : d} =
          {a = x, b = y}
 (* usage example *)
 val rec_twor = twor [#A] [#B] [int] [string] 3 "4" (* this yields the expression:  {A = 3, B = "4"} *)
 val rec_twor_explicit = twor [#A] [#B] [int] [string] 3 "4" (* should be equal to  {A = 3, B = "4"} *)


Constructing a record type taking two names and two types. Because disjointness can't be proofed at type level it must be done at expression level.

 (* type level function returning a record type *)
 con build_record = fn  (a::Name)   (b::Name)  (c::Type) (d::Type) => [[a] ~ [b]] => {a: c, b:d}
 (* usage *)
 val r : build_record #A #B int string  = fn [[A] ~ [B]] => {A = 3, B = "s"}

Adam's description can be found on the mailinglist: date: December 20 2010, Subject: "simple example about constructing rects - guarded types?"

Personal tools