~thon/thon

ref: 5180b858109c12b20eac00c11eff87b0f5dc993a thon/examples/manual-datatype.thon -rw-r--r-- 2.2 KiB
5180b858Evan Bergeron Use List in datatype example 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
(*
 * 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