Comp 302 Final Types & Option

Concepts (∗ Base types: bool , int , char, float , ’a list , option ∗)

(∗ ’x denotes a polymorphic type (Java Generics) ∗)
let curry f = (fun x y −> f (x, y))
type ’a option = None | Some of ’a
let curry2 f x y = f (x, y)
(∗ Constructors can be used to match within types
let curry3 = fun f −> fun x −> fun y −> f (x, y)
match cases are sufficient once all constructors are matched ∗)
let uncurry f = (fun (x, y) −> f x y)
type rational = Integer of int
| Fraction of rational ∗ rational
(∗ Functions are right associative ∗)
type ’param int pair = int ∗ ’param
(∗ Functions are not evaluated until they need to be ∗)
let x = (3, 3.14) (∗ val x : int ∗ float = 3, 3.14 ∗)
let test a b = a ∗ a + b
(∗ Valid specified type ∗)
test 3 = fun y −> 3 ∗ 3 + y (∗ Not 9 + y ∗)
let (x : int pair ) = (3, 3.14) (∗ val x : int pair = 3, 3.14 ∗)
Syntax
Do not forget about ’rec’, ’let ... in’, brackets, Higher Order Functions
constructors or tuples
match x with (∗ sum : (int −> int) −> int ∗ int −> int ∗)
| a −> (∗ return ∗) let rec sum f (a, b) =
| b −> (∗ Nested matching ∗) if a > b then 0
begin match ... with else f a + sum f (a + 1, b)
| ... −> (∗ sumCubes : int ∗ int −> int = <fun> ∗)
end let sumCubes (a, b) = sum (fun x −> x ∗ x ∗ x) (a, b)
| −> (∗ wildcard return ∗)

let name arg1 arg2 =

Induction
let inner’ arg1’ arg2’ = out’ in • Mathematical, Structural
inner’ arg1 arg2 • Can generalize theory when proving
Eg rev (x::t) = rev’ (x::t) [] ⇒ rev l @ acc = rev’ l acc
exception Failure of string e⇓v multi step evaluation from e to v
raise (Failure ”what a terrible failure ”) e ⇒ e0 single step evaluation from e to e0
e ⇒∗ e0 multiple small step evaluations from e to e0
let x = 2 and y = 4 (∗ Initializes both ∗)
State theory and IH; do base case
(∗ (’a ∗ ’b −> ’c) −> ’a −> ’b −> ’c = <fun> ∗) let rec even parity = function
let cur = fun f −> fun x −> fun y −> f (x,y) | [] −> false
| true::xs −> not (even parity xs)
(∗ ’a list list −> ’a list = <fun> ∗) | false :: xs −> even parity xs
let first lst = match lst with
| [] −> [] | x :: xs −> x let even parity tr l = let rec parity p = function
| [] −> p | p’::xs −> parity (p<>p’) xs in
(∗ val is zero : int −> string = <fun> ∗) parity false l
let is zero = function | 0 −> ”zero” | −> ”not zero”
(∗ IH: For all l , even parity l = even parity tr l ∗)
(∗ Variable bindings are overshadowed; (∗ Case for true: ∗)
bindings are valid in their respective scopes ∗) even parity tr true::xs
let m = 2;; let m = m ∗ m in m (∗ is 4 ∗);; = parity false true::xs (∗ Def of even parity tr ∗)
m (∗ is 2 ∗) ;; let f () = m;; let m = 3;; f () (∗ is 2 ∗) ;; = parity (false <> true) xs (∗ Def of parity ∗)
= parity true xs (∗ Def of <> ∗)
List Ops = not (parity false xs) (∗ Prove? ∗)
= not (even parity tr xs) (∗ Def of even parity tr ∗)
elem :: list list1 @ list2
= not (even parity xs) (∗ IH ∗)
val length : ’a list −> int
= even parity true::xs (∗ Def of even parity ∗)
val find opt : (’ a −> bool) −> ’a list −> ’a option
val filter : (’ a −> bool) −> ’a list −> ’a list
val map : (’a −> ’b) −> ’a list −> ’b list
val fold right : (’ a −> ’b −> ’b) −> ’a list −> ’b −> ’b References
val for all : (’ a −> bool) −> ’a list −> bool mutable type type t = { mutable i : int }
val exists : (’ a −> bool) −> ’a list −> bool init let x = ref 0 let y = i = 5
val rev : ’a list −> ’a list retrieval let val1 = !x let val2 = y.i
val init : int −> (int −> ’a) −> ’a list (∗ by index ∗) assignment x := 9 y.i <–1
module type STACK = (∗ Coin ∗)
sig
type stack exception BackTrack
type t
val empty : unit −> stack (∗ val change : int list −> int −> int list = <fun> ∗)
val push : t −> stack −> stack let rec change coins amt = if amt = 0 then []
val size : stack −> int else (match coins with
val pop : stack −> stack option | [] −> raise BackTrack
val peek : stack −> t option | coin :: cs −>
end if coin > amt then change cs amt
else try coin :: (change coins (amt − coin))
module IntStack : (STACK with type t = int) = with BackTrack −> change cs amt)
struct
type stack = int list (∗ val change : int list −> int −>
type t = int (int list −> ’a) −> (unit −> ’a) −> ’a = <fun> ∗)
let empty () = [] let rec change coins amt success failure =
let push i s = i :: s if amt = 0 then success []
let size = List.length else match coins with
let pop = function | [] −> None | :: t −> Some t | [] −> failure ()
let peek = function | [] −> None | h :: −> Some h | coin :: cs −>
end if coin > amt then change cs amt success failure
else change coins (amt − coin)
(∗ Susp ∗) (fun list −> success (coin :: list ))
(fun () −> change cs amt success failure)
type ’a susp = Susp of (unit −> ’a)
type ’a str = {hd: ’a; tl : (’ a str ) susp} Syntax & Semantics
let delay f = Susp f (∗ (unit −> ’a) −> ’a susp ∗)
let force (Susp f) = f() (∗ ’a susp −> ’a ∗) • Definition
F V ((e1 , e2 )) = F V (e1 ) ∪ F V (e2 )
(∗ (’a −> ’b −> ’c) −> ’a str −> ’b str −> ’c str ∗) • Substitution
let rec zip f s1 s2 = {hd = f s1.hd s2.hd ; [e0 /x0 ](let pair (x, y) = e1 in e2 end) = let pair (x, y) =
tl = delay (fun () −> zip f (force s1. tl ) ( force s2. tl )) } [e0 /x0 ]e1 in [e0 /x0 ]e2 end
Provided x0 6= x && x0 6= y && (x, y 6= F V (e0 ))
(∗ Sieve of Eratosthenes ∗) • Type
Types t ::= int | bool | T1 → T2 | T1 × T2 | α
Γ ` (x, y) : T × S Γ ∪ {(x : T ), (y : S)} ` e2 : U
let rec filter str (p : ’a −> bool) (s : ’a str ) =
let h, t = find hd p s in {hd = h; Γ ` let pair (x, y) = e1 in e2 : U
T-LET
tl = delay (fun () −> filter str p ( force t))}
Provided x0 6= x, x0 6= y, & x, y ∈ / F V (e0 )
and find hd p s = if p s .hd then (s.hd, s. tl )
else find hd p ( force s . tl )
My Solution (they don’t account for e1 )
Γ ` e1 : T1 × T2 Γ, x : T1 , y : T2 , ` e2 : T
let no divider m n = not (n mod m = 0)
Γ ` let (x, y) = e1 in e2 end : T
let rec sieve s = { hd = s.hd; T-LET-MATCH
tl = delay (fun () −> • Operation
sieve ( filter str (no divider s .hd) (force s . tl ) ))} e1 ⇓ (v1 , v2 ) [v1 /x][v2 /y]e3 ⇓ v
B-LET
let pair (x, y) = e1 in e2 ⇓ v3
(∗ val double : (’a −> ’a) −> ’a −> ’a = <fun> ∗) • References
let double = fun f −> fun x −> f(f(x)) Γ ` e1 : T ref Γ ` e2 : T Γ ` e : T ref
Γ ` e1 := e2 : unit Γ `!e : T
Γ`e:T
Γ ` ref e : T ref Γ ` () : unit
• Preservation: If e ⇓ v and e : T then v : T

Γ ` e ⇒ T /C : Infer type T for expression e in the typing

Misc x:T ∈Γ
environment Γ module the constraints C B-VAR
Γ ` x ⇒ T /∅
Γ `⇒ T /C Γ ` e1 ⇒ T1 /C1 Γ ` e2 ⇒ T2 /C2
An effect is an action resulting from evaluation of an Γ ` if e then e1 else e2 ⇒ T1 /C ∪ C1 ∪ C2 ∪ {T = bool, T1 = T2 }
expression other than returning a value. B-IF