/
datatype.levy
70 lines (49 loc) · 1.92 KB
/
datatype.levy
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
58
59
60
61
62
63
64
65
66
67
68
69
# Sums and products are (awkwardly) introduced into Levy by the datatype
# mechanism; polymorphism would make this much less awkward. Here we see an
# encoding of `int + bool` and `int * bool`.
data IAmAnInt: int -o intorbool
| IAmABool: bool -o intorbool ;;
val v1 = IAmAnInt 4 ;;
val v2 = IAmABool false ;;
data Pair: int -o bool -o intandbool ;;
val v3 = Pair 12 true ;;
# Datatype declarations are most useful for their introduciton of inductive
# datatypes, like lists of integers or trees containing integers.
data Nil: list
| Cons: int -o list -o list ;;
data Emp: tree
| Node: tree -o int -o tree -o tree ;;
val v4 = Cons 4 (Cons 6 (Cons 19 (Cons (-4) Nil)))
val v5 = Node (Node Emp 3 Emp) 5 (Node Emp 7 (Node Emp 9 Emp)) ;;
val nil = thunk fun x: list ->
match x with
| Nil -> return true
| y -> return false ;;
force nil Nil ;;
force nil (Cons 4 Nil) ;;
val sumlist = thunk rec sumlist : list -> F int is
fun xs : list ->
match xs with
| Nil -> return 0
| Cons x xs -> force sumlist xs to y in return x + y ;;
force sumlist v4 ;;
val map = thunk fun f : U (int -> F int) ->
rec mp : list -> F list is fun xs : list ->
match xs with
| Nil -> return Nil
| Cons x xs ->
force f x to y in
force mp xs to ys in
return Cons y ys ;;
force map (thunk fun x : int -> return 0 - x) v4 ;;
force map (thunk fun x : int -> return x * x) v4 ;;
# The syntax we have chosen lets us define mutual recursive datatypes in a
# simple way, as we can see from the following definition of even/odd unary
# natural numbers. A lack of mutually recursive functions in Levy means that
# this isn't terribly useful, but there you go.
data Z: even
| EO: even -o odd
| OE: odd -o even ;;
val four = OE (EO (OE (EO Z))) ;;
# At the end of a datatype declaration the type is closed; it would be an error
# to have a subsequent declaration like `data One: even`