~thon/thon

7df98af35b3b2508aa44e751dc7faff15320d22c — Evan Bergeron 3 months ago 0984535
Some excerpts on datatypes
1 files changed, 57 insertions(+), 0 deletions(-)

A examples/manual-datatype.thon
A examples/manual-datatype.thon => examples/manual-datatype.thon +57 -0
@@ 0,0 1,57 @@
(*
 * Datatypes are a combination of three different language features:
 * sum types, recursive types, and existential types.
 *
 * Here's a slightly reworded snippet from the introduction of the
 * paper "Typed Compiliation of Recursive Datatypes":
 *
 *    Harper and Stone [translate] a datatype declaration as a module
 *    containing an abstract type and functions to construct and
 *    deconstruct values of that type ... datatypes *are* abstract
 *    types.
 *
 * Or 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
 *     rperesented 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 delcaration
 *     in which the implementation type is held abstract, and the
 *     operations describe above are declared as operations on that
 *     abstrac 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.
 *
 * At the time of writing, I don't understand the last sentence of the
 * above paragraph, but we'll do the rest of it.
 *
 * So here's some thon code that manually implements
 *
 * data List = Nil | Cons of int * List
 *
 * Still want to double-check this.
 *
 *)
impl (some t. ((unit -> t) * (((nat * t) -> t))))
with (u l. (unit |  (nat * l))) as
(
    (* Nil *)
    \ inUnit : unit ->
        fold u l. (unit | (nat * l))
        with left inUnit : (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)))))
)