Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | (* From Chapter 5 of Elsman's PhD thesis; these examples should |
2 | * elaborate. *) | |
3 | ||
4 | (* Decrease in generativity *) | |
5 | ||
6 | functor f() = struct type a = int | |
7 | val a = 232 | |
8 | val pr = Int.toString | |
9 | end :> sig type a | |
10 | val a : a | |
11 | val pr : a -> string | |
12 | end | |
13 | ||
14 | structure f = f() | |
15 | val _ = print ("f.a = " ^ f.pr f.a ^ "\n") | |
16 | ||
17 | functor g() = struct datatype a = A | B | |
18 | fun pr_a A = "A" | |
19 | | pr_a B = "B" | |
20 | val pr_b = pr_a | |
21 | type b = a | |
22 | end :> sig type a type b | |
23 | val A : a | |
24 | val B : b | |
25 | val pr_a : a -> string | |
26 | val pr_b : b -> string | |
27 | end | |
28 | ||
29 | structure g = g() | |
30 | val _ = print ("g.A = " ^ g.pr_a g.A ^ "\n") | |
31 | val _ = print ("g.B = " ^ g.pr_b g.B ^ "\n") | |
32 | ||
33 | ||
34 | functor h(s : sig type a val pr : a -> string val a : a end) = | |
35 | struct | |
36 | val pr = s.pr | |
37 | val b = s.a | |
38 | type b = s.a | |
39 | end :> sig type b | |
40 | val pr : b -> string | |
41 | val b : b | |
42 | end | |
43 | ||
44 | structure h = h(struct type a = int val pr = Int.toString val a = 343 end) | |
45 | val _ = print ("h.b = " ^ h.pr h.b ^ "\n") | |
46 | ||
47 | (* Increase in generativity *) | |
48 | ||
49 | functor i() = struct datatype a = A | |
50 | and b = B | C | |
51 | type c = a * b | |
52 | val c = (A,C) | |
53 | fun pr (A,B) = "(A,B)" | |
54 | | pr (A,C) = "(A,C)" | |
55 | end :> sig type c val c : c val pr : c -> string end | |
56 | ||
57 | structure i = i() | |
58 | val _ = print ("i.c = " ^ i.pr i.c ^ "\n") | |
59 | ||
60 | (* Signature S below is well-formed, but after opacity elimination it | |
61 | * is not. No real structure (i.e., a structure existing outside of a | |
62 | * functor body) can match the signature S. The signature should | |
63 | * elaborate, however. *) | |
64 | ||
65 | structure S = struct type s = int * int | |
66 | end :> sig eqtype s end | |
67 | ||
68 | signature S = sig datatype u = A | |
69 | end where type u = S.s |