~thon/thon

ref: 7df98af35b3b2508aa44e751dc7faff15320d22c thon/examples/manual-datatype.thon -rw-r--r-- 2.4 KiB
7df98af3Evan Bergeron Some excerpts on datatypes 3 months ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
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)))))
)