(*
* Datatypes are a combination of three different language features:
* sum types, recursive types, and existential types.
*
* From "A type-theoretic interpretation of standard ML":
*
* A datatypes declaration elaborates to a structure consisting of
* a type together with operations to create and analyze values of
* the type. ... The underlying implementation type is defined to
* be a recursive sum type, with one summand corresponding to each
* constructor in the declaration. The constructores are
* represented by total functions that inject values into the
* appropriate summand of the recursive type. ... The structure is
* sealed with a signature derived from the datatype declaration
* in which the implementation type is held abstract, and the
* operations described above are declared as operations on that
* abstract type. Holding the implementation type abstract captures
* the "generativity" of datatype declarations in Standard ML; the
* declared type is "new" in the sense that it is represented by a
* path that is, by alpha-conversion, distinct from all previous
* types in the program. Analogously, datatype specifications
* (which may occur in signatures) are elaborated into the same
* signature used to seal the structure resulting from elaboration
* of the correspond datatype declaration.
*
* So here's some thon code that manually implements
*
* data List = Nil | Cons of int * List
*
*)
let ListImpl : (some t. (t * (((nat * t) -> t)))) =
impl (some t. (t * (((nat * t) -> t))))
with (u l. (unit | (nat * l))) as
(
(* Nil - since this takes no args, may as well return val directly *)
fold u l. (unit | (nat * l))
with left unit : (unit | (nat * (u l . (unit | (nat * l)))))
,
(* Cons *)
\ natAndNatList : (nat * (u l. (unit | (nat * l)))) ->
fold u l.(unit | (nat * l))
with right natAndNatList : (unit
| (nat * (u l. (unit | (nat * l)))))
)
in use ListImpl as (li, List) in
let Nil : List = fst li in
let Cons : (nat * List) -> List = snd li in
Z