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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
datatype 'a t = R of 'a | L of 'a t t
val rec build: int -> int t =
fn 0 => R 17
| n => L (R (build (n - 1)))
val rec depth: int t -> int =
fn R _ => 0
| L (R z) => 1 + depth z
| _ => raise Match
val n = depth (build 13)
val _ =
if n = 13
then ()
else raise Fail "bug"
(*
val _ = R 13
val _ = L (R (R 13))
val rec build: int -> int t =
fn 0 => R 13
| n => L (R (build (n - 1)))
val _ = f 13
*)
(*
val rec f =
fn R _ => 0
| L (R z) => 1 + f z
val v0: int t = R 13
val v2: int t t = R v0
val v1: int t = L (v2: int t t)
val _ = L (L (R (R (R 13))))
val _ = L (R (L (R (R 13))))
val _ = L (L (R (R (R (R (R 13))))))
*)
(*
datatype 'a t = A of 'a | B of ('a t * 'a t) t
val v1 = A 13
val v2 = A (v1, v1)
val v3 = A (v2, v2)
val v4 = B v3
val v5 = B v4
val x = A 1 : int t
val y = B (A (x, x))
val z = B (A (y, y))
val a = B (A (z, z))
fun d ((A _) : 'a t) : int = 0
| d ((B (A (x, _))) : 'a t) : int = 1 + d x
val n = d a
*)
(*
Here's (the relevant part of) what the monomorphiser in smlc returns
for your program.
datatype t_0 = B_0 of t_1 | A_0 of int
and t_1 = A_1 of (t_0 * t_0)
It figures out exactly your observation that every use of B must be
followed by A.
[z0 = int t]
datatype z0 = A of int | B of z1
[z1 = (z0 * z0) t]
datatype z1 = A of z0 * z0 | B of z2
[z2 = (z1 * z1) t]
datatype z2 = A of z1 * z1 | B of z3
[z3 = (z2 * z2) t]
B z1
B (B z2)
B (B (A (z1, z1)))
B (B (A (A (z0,z0), A (z0,z0))))
B (B (A (A (v1, v1), A (v1, v1))))
B (B (A (A (v1, v1), A (v1, v1))))
datatype z = A of int | B of (z * z) t
datatype w = A of z * z | B of (w * w) t
*)
|
