Disjointness fun - creating records using type level functions
From Impredicative Wiki
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?"