Programming Languages
ML
CSCI-GA.2110-003 Fall 2020
ML overview
■ originally developed for use in writing theorem provers
■ functional: functions are first-class values
■ garbage collection
■ strict evaluation (applicative order)
■ no coercion
■ strong and static typing; powerful type system
◆ parametric polymorphism
◆ structural equivalence
◆ all with type inference!
■ advanced module system
■ exceptions
■ miscellaneous features:
◆ datatypes (merge of enumerated literals and variant records)
◆ pattern matching
◆ ref type constructor (like “const pointers” (not “pointers to const”))
2 / 45
Sample SML interactive session
– val k = 5; val k = 5 : int
user input system response
– k * k * k;
val it = 125 : int
‘it’– last computation
– [1, 2, 3];
val it = [1,2,3] : int list
– [“hello”, “world”];
val it = [“hello”,”world”] : string list
– 1 :: [ 2, 3 ];
val it = [1,2,3] : int list – [ 1, “hello”];
error
3 / 45
Operations on lists
– null [1, 2];
val it = false : bool
– null [ ];
val it = true : bool
– hd [1, 2, 3]; val it = 1 : int
– tl [1, 2, 3];
val it = [ 2, 3 ] : int list
– [ ];
val it = [ ] : ’a list this list is polymorphic
4 / 45
Simple functions
A function declaration:
– fun abs x = if x >= 0.0 then x else ~x
val abs = fn : real -> real
A function expression:
– fn x => if x >= 0.0 then x else ~x val it = fn : real -> real
5 / 45
Functions, II
– fun length xs = if null xs
then 0
else 1 + length (tl xs);
val length = fn : ’a list -> int
’a denotes a type variable; length can be applied to lists of any element type The same function, written in pattern-matching style:
– fun length [] = 0
| length (x::xs) = 1 + length xs
val length = fn : ’a list -> int
6 / 45
Type inference and polymorphism
Advantages of type inference and polymorphism:
■ frees you from having to write types.
A type can be more complex than the expression whose type it is, e.g., flip
■ with type inference, you get polymorphism for free:
◆ no need to specify that a function is polymorphic
◆ no need to ”instantiate” a polymorphic function when it is applied
7 / 45
Multiple arguments?
■ All functions in ML take exactly one argument
■ If a function needs multiple arguments, we can
1. pass a tuple:
– (53, “hello”); (* a tuple *)
val it = (53, “hello”) : int * string
We can also use tuples to return multiple results.
2. use currying (named after Haskell Curry, a logician)
8 / 45
The tuple solution
Another function; takes two lists and returns their concatenation
– fun append1 ([ ], ys) = ys
| append1 (x::xs, ys) = x :: append1 (xs, ys);
val append1 = fn: ’a list * ’a list -> ’a list
– append1 ([1,2,3], [8,9]);
val it = [1,2,3,8,9] : int list
9 / 45
Currying
The same function, written in curried style:
– fun append2 [ ] ys = ys
| append2 (x::xs) ys = x :: (append2 xs ys);
val append2 = fn: ’a list -> ’a list -> ’a list
Note: α → β → δ means α → (β → δ). – append2 [1,2,3] [8,9];
val it = [1,2,3,8,9] : int list
– val app123 = append2 [1,2,3];
val app123 = fn : int list -> int list
– app123 [8,9];
val it = [1,2,3,8,9] : int list
10 / 45
More partial application
But what if we want to provide the other argument instead, i.e., append [8,9] to its argument?
■ here is one way: (the Ada/C/C++/Java way) fun appTo89 xs = append2 xs [8,9]
■ here is another: (using a higher-order function) val appTo89 = flip append2 [8,9]
flip is a function which takes a curried function f and returns a function that works like f but takes its arguments in the reverse order.
In other words, it “flips” f’s two arguments.
We define it on the next slide…
11 / 45
Type inference example
fun flip f y x = f x y Thetypeofflipis(α→β→γ)→β→α→γ. Why?
■ Consider (f x). f is a function; its parameter must have the same type as x.
f : A → B x : A (f x) : B
■ Now consider (f x y). Because function application is left-associative, f x y ≡ (f x) y. Therefore, (f x) must be a function, and its parameter must have the same type as y:
(fx): C→D y: C (fxy): D
■ NotethatBmustbethesameasC→D. WesaythatBmustunify with C → D.
■ The return type of flip is whatever the type of f x y is. After renaming the types, we have the type given at the top.
12 / 45
Type rules
The type system is defined in terms of inference rules. For example, here is the rule for variables:
and the one for function calls:
and here is the rule for if expressions:
(x : τ) ∈ E E⊢x:τ
E⊢e1 :τ′ →τ E⊢e2 :τ′ E ⊢ e1 e2 : τ
E⊢e:bool E⊢e1:τ E⊢e2:τ E ⊢ifethene1 elsee2 : τ
13 / 45
Passing functions
– fun exists pred [ ] = false
| exists pred (x::xs) = pred x orelse
val exists = fn : (’a -> bool) -> ’a list -> bool
■ pred is a predicate : a function that returns a boolean
■ exists checks whether pred returns true for any member of the list
– exists (fn i => i = 1) [2, 3, 4]; val it = false : bool
exists pred xs;
14 / 45
Applying functionals
– exists (fn i => i = 1) [2, 3, 4]; val it = false : bool
Now partially apply exists:
– val hasOne = exists (fn i => i = 1);
val hasOne = fn : int list -> bool
– hasOne [3,2,1]; val it = true : bool
15 / 45
Functionals 2
fun all pred [ ] = true
| all pred (x::xs) = pred x andalso all pred xs
fun filter pred [ ] = [ ]
| filter pred (x::xs) = if pred x
all: (α →bool) → αlist→bool filter : (α → bool) → αlist → αlist
then x :: filter pred xs else filter pred xs
16 / 45
Block structure and nesting
let provides local scope:
(* standard Newton-Raphson *)
fun findroot (a, x, acc) =
let val nextx = (a / x + x) / 2.0
end
(* nextx is the next approximation *)
in
if abs (x – nextx) < acc * x then nextx
else findroot (a, nextx, acc)
17 / 45
Quicksort in functional form
fun quicksort op< [] = []
| quicksort op< [x] = [x]
| quicksort op< (a::bs) =
let fun |
partition (left, right, []) = (left, right) partition (left, right, x::xs) =
if x < a
then partition (x::left, right, xs)
val
else partition (left, x::right, xs) (left, right) = partition ([], [], bs)
in
quicksort op< left @ (a :: quicksort op< right)
end
(Corrections courtesy Xingjian Guo)
quickSort : (α ∗ α → bool) → αlist → αlist
18 / 45
A variant of Quicksort
fun quickSort op< [] = []
| quickSort op< [x] = [x]
| quickSort op< (a::bs) =
let fun
deposit (x, (left, right)) = if x < a
then (x::left, right)
else (left, x::right)
val
(left, right) = foldr deposit ([], []) bs
in
quickSort op< left @ (a :: quickSort op< right)
end
(Corrections courtesy Xingjian Guo)
quickSort : (α ∗ α → bool) → αlist → αlist
19 / 45
The type system
■ primitive types: bool, int, char, real, string, unit
■ constructors: list, array, product (tuple), function, record
■ “datatypes”: a way to make new types
■ structural equivalence (except for datatypes)
◆ as opposed to name equivalence in e.g., Ada
■ an expression has a corresponding type expression
■ the interpreter builds the type expression for each input
■ type checking requires that type of functions’ parameters match the type
of their arguments, and that the type of the context matches the the type of the function’s result
20 / 45
ML records
Records in ML obey structural equivalence (unlike records in many other languages).
A type declaration: only needed if you want to refer to this type by name type vec = { x : real, y : real }
A variable declaration:
val v = { x = 2.3, y = 4.1 }
Field selection:
#x v
Pattern matching in a function:
fun dist {x,y} =
sqrt (pow (x, 2.0) + pow (y, 2.0))
21 / 45
Tuples
Tuples are actually records.
("I", "Love", "Programming", "Languages")
is actually. . .
{1="I", 2="Love", 3="Programming", 4="Languages"} Expression #2 extracts the second element of the tuple. Or, "Love" above.
22 / 45
Datatypes
A datatype declaration:
■ defines a new type that is not equivalent to any other type (name equivalence)
■ introduces data constructors
◆ data constructors can be used in patterns
◆ they are also values themselves
23 / 45
Datatype example
datatype tree = Leaf of int
| Node of tree * tree
tree is a type constructor.
Leaf and Node are data constructors:
■ Leaf : int → tree
■ Node : tree * tree → tree
We can define functions by pattern matching:
Or:
fun sum (Leaf t) = t
| sum (Node (t1, t2)) = sum t1 + sum t2
fun sum x = case x of Leaf t => t
| Node(t1,t2) => sum t1 + sum t2
24 / 45
More on datatypes
Functions accepting data constructors as arguments must provide an exhaustive definition (cover every data constructor for the datatype). Consider again:
datatype tree = Leaf of int
| Node of tree * tree
fun sum (Leaf t) = t;
stdIn:94.5-94.28 Warning: match nonexhaustive Leaf t => …
25 / 45
Parameterized datatypes
fun flatten (Leaf t) = [t] | flatten (Node (t1, t2)) =
flatten t1 @ flatten t2
datatype ’a gentree = Leaf of ’a
flatten : tree → int list
| Node of ’a gentree * ’a gentree
val names = Node (Leaf “this”, Leaf “that”)
names : string gentree
26 / 45
The rules of pattern matching
Pattern elements:
■ integer literals: 4, 19
■ character literals: #’a’
■ string literals: “hello”
■ data constructors: Node (· · ·)
◆ depending on type, may have arguments, which would also be patterns ■ variables: x, ys
■ wildcard: _
Convention is to capitalize data constructors and structure names. Also, start variables and type constructors with lower-case.
27 / 45
More rules of pattern matching
Special forms:
■ (), {} – the unit value
■ [] – empty list
■ [p1,p2,···,pn]
means(p1::(p2:: ··· (pn::[])···))
■ (p1,p2, ···,pn)– a tuple
■ (p1,_,···,pn)
– a partially specified tuple using a wildcard.
■ {field1, field2, · · · fieldn} – a record
■ {field1, field2, · · · fieldn, …}
– a partially specified record using a wildcard.
■ vasp
– v is a name for the entire pattern p
Example: M as x::xs binds M to the pattern x::xs.
28 / 45
Common idiom: option
option is a built-in datatype:
datatype ’a option = NONE | SOME of ’a
Defining a simple lookup function:
fun lookup eq key [] = NONE | lookup eq key ((k,v)::kvs) =
if eq (key, k)
then SOME v
else lookup eq key kvs
Is the type of lookup:
(α ∗ α → bool) → α → (α ∗ β) list → β option?
No! It’s slightly more general:
(α1 ∗α2 →bool)→α1 →(α2 ∗β)list→βoption
29 / 45
Another lookup function
We don’t need to pass two arguments when one will do:
fun lookup _ [] = NONE | lookup checkKey ((k,v)::kvs) =
if checkKey k
then SOME v
else lookup checkKey kvs
The type of this lookup:
(α → bool) → (α ∗ β) list → β option
30 / 45
Useful library functions
■ map: (α → β) → αlist→ βlist
map (fn i => i + 1) [7, 15, 3]
=⇒ [8, 16, 4]
■ foldl:(α∗β→β)→β→αlist→β
foldl (fn (a,b) => “(” ^ a ^ “+” ^ b ^ “)”) “0” [“1”, “2”, “3”]
=⇒ “(3+(2+(1+0)))”
■ foldr:(α∗β→β)→β→αlist→β
foldr (fn (a,b) => “(” ^ a ^ “+” ^ b ^ “)”) “0” [“1”, “2”, “3”]
=⇒ “(1+(2+(3+0)))”
■ filter : (α → bool) → αlist → αlist
31 / 45
Overloading
Ad hoc overloading interferes with type inference:
fun plus x y = x + y
Operator ‘+’ is overloaded, but types cannot be resolved from context
(defaults to int).
We can use explicit typing to select interpretation:
fun mix1 (x, y, z) = x * y + z : real fun mix2 (x: real, y, z) = x * y + z
32 / 45
Parametric polymorphism/generics
■ a function whose type expression has type variables applies to an infinite set of types
■ equality of type expressions means structural not name equivalence
■ all applications of a polymorphic function use the same body: no need to
instantiate
let val val
ints = [1, 2, 3];
strs = [“this”, “that”];
in
end;
ints + (* int list -> int *) len strs (* string list -> int *)
len
33 / 45
ML signature
An ML signature specifies an interface for a module.
signature STACKS = sig
end
type stack
exception Underflow
val empty : stack
val push : char * stack -> stack val pop : stack -> char * stack val isEmpty : stack -> bool
34 / 45
ML structure
structure Stacks : STACKS = struct
end
type stack = char list exception Underflow val empty = [ ]
val push = op::
fun pop (c::cs) = (c, cs)
| pop [] = raise Underflow
fun isEmpty [] = true | isEmpty _ = false
35 / 45
Signature ascription
Opaque ascription (denoted :>) hides the identity of types beyond that which is conveyed in the signature. That is, additional type information provided by the structure will be considered abstract.
structure Stacks :> STACKS = …
Transparent ascription (denoted 🙂 exposes the identity of types beyond that conveyed in the signature. That is, additional type information provided by the structure will augment the signature.
structure Stacks : STACKS = …
Both: prohibit the introduction of identifiers not already present in the signature. This is component hiding.
Both: permit types (in structures) which are broader than the signature. Permitted:
Signature: var blah : int -> int; // int -> int
Structure: fun blah x = x; // ’a -> ’a
36 / 45
Opaque ascription
signature SetSignature = sig
end;
type ’a set
val empty : ’’a set
val singleton : ’’a -> ’’a set
structure Set = struct type ’a set = ’a list; val empty = [];
fun singleton a = [a] val aux = [];
end;
structure Set2 :> SetSignature = Set; Set2.aux; (* error – component hiding *) Set2.singleton(2) = [2]; (* error – list
representation hidden *)
37 / 45
Transparent ascription
signature SetSignature = sig
end;
type ’a set
val empty : ’’a set
val singleton : ’’a -> ’’a set
structure Set = struct type ’a set = ’a list; val empty = [];
fun singleton a = [a] val aux = [];
end;
structure Set2 : SetSignature = Set; Set2.aux; (* error – component hiding *) Set2.singleton(2) = [2]; (* okay *)
38 / 45
ML functor
A functor creates a structure from a structure.
signature TOTALORDER = sig
type element;
val lt : element * element -> bool;
end;
functor MakeBST(Lt: TOTALORDER): sig
type ’label btree;
exception EmptyTree;
val create : Lt.element btree;
val lookup : Lt.element * Lt.element btree
-> bool;
val insert : Lt.element * Lt.element btree
-> Lt.element btree;
39 / 45
Functors (cont’d)
end;
val deletemin : Lt.element btree -> Lt.element * Lt.element btree;
val delete : Lt.element * Lt.element btree -> Lt.element btree;
end = struct open Lt;
datatype ’label btree = Empty |
Node of ’label val create = Empty;
* ’label btree * ’label btr
fun lookup(x, Empty)
fun insert(x, Empty) exception EmptyTree;
fun deletemin(Empty)
fun delete(x,Empty) = …;
= …; = …;
= …;
40 / 45
Invoking the Functor
structure String : TOTALORDER = struct
type element = string; fun lt(x,y) =
end; end;
let
fun lower(nil) = nil |
lower(c::cs) =
(Char.toLower c)::lower(cs);
in
implode(lower(explode(x))) < implode(lower(explode(y)))
structure StringBST = MakeBST(String);
41 / 45
Unification, Currying & ML Types
fun B x y z = x (y z)
What type is this?
42 / 45
Unification, Currying & ML Types
fun B x y z = x (y z)
val it = fn : (’a -> ’b) -> (’c -> ’a) -> ’c -> ’b
43 / 45
Unification, Currying & ML Types
fun B x y z = x (y z)
fun B = fn x => fn y => fn z => x (y z)
fun B = fn (x : T1) => fn(y : T2) => fn(z : T3) = x (y z) : T4
TR = T1 -> T2 -> T3 -> T4
(y z) :: T2 = T3 -> T5
x (y z) :: T1 = T5 -> T6
T4 = T6
44 / 45
Unification, Currying & ML Types
fun B x y z = x (y z)
fun B = fn x => fn y => fn z => x (y z)
fun B = fn (x : T1) => fn(y : T2) => fn(z : T3) = x (y z) : T4
TR = T1 -> T2 -> T3 -> T4
(y z) :: T2 = T3 -> T5
x (y z) :: T1 = T5 -> T6
T4 = T6
Now put it together:
TR = (T5 -> T6) -> (T3 -> T5) -> T3 -> T6
(’a -> ’b) -> (’c -> ’a) -> ’c -> ’b
val it = fn : (’a -> ’b) -> (’c -> ’a) -> ’c -> ’b
45 / 45