Intro_to_PL (Week 4)
Type Inference
Analysis the constraints (e.g., a > 0
infers a : int
).
Use type variables (e.g., ’a) for any unconstrained types in function arguments or results.
Here is an example:1
fun compose (f, g) = fn x => f (g x)
- The function
compose
has the type:T1 * T2 -> T3
. - The anonymous function has the type:
T3 = T4 -> T5
. g
has the type:T4 -> T6
.f
has the type:T6 -> T7
.T7 = T5
.compose
has the type:(T6 -> T5) * (T4 -> T6) -> (T4 -> T5)
.- Using Type Variant:
('a -> 'b) * ('c -> 'a) -> ('c -> 'b)
.
The Value Restriction
Only by Type Inference is not enough.1
2
3val x = ref NONE (* type of r : ?.X1 option ref *)
val _ = x := SOME "hi"
val _ = 1 + valOf (!x)
This creates a dummy type for x
, which cannot be used later.
In general, ML will give a variable in a val-binding a polymorphic type only if the expression in the val-binding is a value or a variable. This is called the value restriction. In our example, ref NONE
is a call to the function ref
. Function calls are not variables or values.
Similarly, val pairWithOne = List.map (fn x => (x,1))
does not work.
Mutual Inference
1 | datatype t1 = Foo of int | Bar of t2 |
Modual System
Syntax: structure Name = struct bindings end
1 | structure MyLib = struct |
Signature matching
structure FOO :> BAR
A signature’s type binding for a function must be more specific than the type binding for the function in the module.
Here is an example,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
52signature MySig =
sig
datatype rational = Whole of int | Frac of int * int
exception BadFrac
val make_frac : int * int -> rational
val add : rational * rational -> rational
val toString : rational -> string
end
structure MyRational :> MySig =
struct
datatype rational = Whole of int | Frac of int * int
exception BadFrac
fun make_frac (x,y) =
if y = 0
then raise BadFrac
else if y < 0
then Frac(~x,~y)
else Frac(x,y)
fun add (r1,r2) =
case (r1,r2) of
(Whole(i),Whole(j)) => Whole (i + j)
| (Whole(i),Frac(j,k)) => Frac(j+k*i,k)
| (Frac(j,k),Whole(i)) => Frac(j+k*i,k)
| (Frac(a,b),Frac(c,d)) => Frac(a*d + b*c, b*d)
fun toString r =
let fun gcd (x,y) =
if x=y
then x
else if x < y
then gcd(x,y-x)
else gcd(y,x)
fun reduce r =
case r of
Whole _ => r
| Frac(x,y) =>
if x=0
then Whole 0
else
let val d = gcd(abs x,y) in
if d=y
then Whole(x div d)
else Frac(x div d, y div d)
end
in
case reduce r of
Whole i => Int.toString i
| Frac(a,b) => (Int.toString a) ^ "/" ^ (Int.toString b)
end
end
Equivalence
It is important to think whether some functions have side effects.
The following code is not equivalent in ML:1
2
3val y = 2
fun f1 (f, g) = (f x) + (f x)
fun f2 (f, g) = y * (f x)
This is because f
might print out something or increment a variable.
Intro_to_PL (Week 4)