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
|
(* From Chapter 5 of Elsman's PhD thesis; these examples should
* elaborate. *)
(* Decrease in generativity *)
functor f() = struct type a = int
val a = 232
val pr = Int.toString
end :> sig type a
val a : a
val pr : a -> string
end
structure f = f()
val _ = print ("f.a = " ^ f.pr f.a ^ "\n")
functor g() = struct datatype a = A | B
fun pr_a A = "A"
| pr_a B = "B"
val pr_b = pr_a
type b = a
end :> sig type a type b
val A : a
val B : b
val pr_a : a -> string
val pr_b : b -> string
end
structure g = g()
val _ = print ("g.A = " ^ g.pr_a g.A ^ "\n")
val _ = print ("g.B = " ^ g.pr_b g.B ^ "\n")
functor h(s : sig type a val pr : a -> string val a : a end) =
struct
val pr = s.pr
val b = s.a
type b = s.a
end :> sig type b
val pr : b -> string
val b : b
end
structure h = h(struct type a = int val pr = Int.toString val a = 343 end)
val _ = print ("h.b = " ^ h.pr h.b ^ "\n")
(* Increase in generativity *)
functor i() = struct datatype a = A
and b = B | C
type c = a * b
val c = (A,C)
fun pr (A,B) = "(A,B)"
| pr (A,C) = "(A,C)"
end :> sig type c val c : c val pr : c -> string end
structure i = i()
val _ = print ("i.c = " ^ i.pr i.c ^ "\n")
(* Signature S below is well-formed, but after opacity elimination it
* is not. No real structure (i.e., a structure existing outside of a
* functor body) can match the signature S. The signature should
* elaborate, however. *)
structure S = struct type s = int * int
end :> sig eqtype s end
signature S = sig datatype u = A
end where type u = S.s
|
