### rm lec12-live from sp21

parent 99c83bcf
 (* CSE 341, Lecture 12 *) (*#utop_prompt_dummy let _ = UTop.set_show_box false *) (* examples for type inference *) (*** a couple examples "how a human would do it" before we walk through "how the type-checker does it" ***) let f x = if x > 3 then 42 else x * 2 (* let g x = if x > 3 then true else x * 2 *) (* 42 has type int so x has type int *) let x = 42 (* f : bool -> int -> 'a -> int*) let f y z w = if y then z + x else 0 (*** now walking through the constraint-based approach by which type inference is actually defined ***) (* f : T1 -> T2 x : T1 y : T3 z : T4 T1 = T3 * T4 -- because of pattern match T3 = int -- because of call to abs T4 = int -- because of second argument to + T2 = int -- because of result type of + int * int -> int *) let f x = let (y,z) = x in (abs y) + z (* sum : T1 -> T2 xs : T1 T1 = T3 list T2 = int x : T3 xs' : T3 list T3 = int T1 = T3 list = int list T2 = int sum : int list -> int *) let rec sum xs = match xs with | [] -> 0 | x::xs' -> x + (sum xs') (* broken_sum : T1 -> T2 xs : T1 T1 = T3 list T2 = int x : T3 xs' : T3 list T3 = int T3 = T1 T1 = T3 = T3 list *) (* let rec broken_sum xs = match xs with | [] -> 0 | x::xs' -> x + (broken_sum x) *) (* length : T1 -> T2 xs: T1 T1 = T3 list T2 = int x : T3 xs' : T3 list T3 list -> int 'a list -> int *) let rec length xs = match xs with | [] -> 0 | x::xs' -> 1 + (length xs') (* f : T1 -> T2 x : T3 y : T4 z : T5 T1 = T3 * T4 * T5 T2 = T3 * T4 * T5 T2 = T4 * T3 * T5 T3 = T4 T4 * T4 * T5 -> T4 * T4 * T5 'a * 'a * 'a -> 'a * 'a * 'a WRONG 'a * 'b * 'c -> 'a * 'b * 'c WRONG 'a * 'a * 'b -> 'a * 'a * 'b *) let f (x,y,z) = if true then (x,y,z) else (y,x,z) (* compose : T1 -> T2 -> T3 f : T1 g : T2 x : T4 T3 = T4 -> T5 from g being passed x, T2 = T4 -> T6 for some T6 from f being passed the result of g, T1 = T6 -> T7 for some T7 from a call to f being the result of the anonymous function, we need T5=T7 T3 = T4 -> T5 T2 = T4 -> T6 T1 = T6 -> T5 (T6 -> T5) -> (T4 -> T6) -> (T4 -> T5) ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b *) let compose f g = fun x -> f (g x) (* % *) (**** the value restriction (important, but optional material) ****) (* this first line is not polymorphic so next two lines do not type-check *) let r = ref None (* let _ = r := SOME "hi" let i = 1 + valOf (!r) *) type 'a foo = 'a ref let f : 'a -> 'a foo = ref let r2 = f None (* also need value restriction here *) (* where the value restriction arises despite no mutation *) let pairWithOne = List.map (fun x -> (x,1)) (* a workaround *) let pairWithOne2 xs = List.map (fun x -> (x,1)) xs
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment