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
|
(* This example is interesting because at the time of generalization of f, the
* tyvar 'a is in scope, but does not appear in type types of any of the
* variables in the environment (x's type has not yet been determined to be 'a).
* Nevertheless, it is essential to not generalize 'a at g
*)
val 'a f = fn x =>
let
exception E of 'a
fun g (E y) = y
| g _ = raise Fail "bug"
in
E x
end
(* This example is interesting because it binds a type variable at a scope where
* the type variable does not appear in the type. Nevertheless, it is essential
* to keep the type variable there, because it occurs in an inner scope.
*)
fun 'a f () =
let
val x: 'a = raise Fail "bug"
in
()
end
(* This example shows that type variables can be rebound in nested datatype
* declarations, unlike the situation for nested value declarations.
*)
val 'a x =
fn () =>
let
datatype 'a t = T of 'a
in
()
end
(* This example verifies that datatype replication is allowed, even when the
* right-hand side isn't a datatype.
*)
type 'a t = 'a * 'a
datatype u = datatype t
val _: int u = (13, 14);
(* The following examples demonstrate acceptable forms of type variable scoping.
*)
fun f (x: 'a) =
let
fun g (y: 'a) = y
in
()
end
fun f (x: 'a) =
let
fun 'b g (y: 'b) = y
in
()
end
fun 'a f (x: 'a) =
let
fun g (y: 'a) = y
in
()
end
fun 'a f (x: 'a) =
let
fun 'b g (y: 'b) = y
in
()
end
val 'a x =
fn () =>
let
datatype 'a t = T of 'a
in
()
end
(* This example confirms that bools can be used as labels. *)
val {false = x, ...} = {false = 13};
|
