Commit 99c83bcf authored by Dan Grossman's avatar Dan Grossman
Browse files

unit4 code, merged with some bug fixes from au21

parent 9c48a7b7
(* CSE 341, Lecture 11 *)
(*#utop_prompt_dummy
let _ = UTop.set_show_box false
*)
(* modules *)
module type MATHLIB = sig
val fact : int -> int
val half_pi : float
(*val doubler : float -> float*)
end
(* if MATHLIB is "hiding nothing", we could leave it
off and OCaml will do-the-same-thing,
but with doubler commented out above, it does hide
things from outside the module. *)
module MyMathLib : MATHLIB = struct
let rec fact x =
if x = 0 then
1
else
x * fact (x - 1)
let half_pi = Float.pi /. 2.0
let doubler x = x *. 2.0
let pi = doubler half_pi
end
let pi = MyMathLib.half_pi +. MyMathLib.half_pi
(* simply an undefined variable if doubler is not
in the module type*)
(*let twenty_eight = MyMathLib.doubler 14.0 *)
(* ---------------------------------------- *)
(* this signature hides gcd and reduce (and whole). That way
clients cannot assume they exist and cannot call them with
unexpected inputs. *)
module type RATIONAL_A = sig
type rational =
| Whole of int
| Frac of int * int
exception BadFrac
(* tupled looks more like a fraction perhaps*)
val make_frac : int * int -> rational
val add : rational -> rational -> rational
val string_of_rational : rational -> string
end
(* the previous signature lets clients build
any value of type rational they
want by exposing the Frac and Whole constructors.
This makes it impossible to maintain invariants
about rationals, so we might have negative denominators,
which some functions do not handle,
and print_rat may print a non-reduced fraction.
We fix this by making rational abstract. *)
module type RATIONAL_B = sig
type rational (* type is now abstract *)
exception BadFrac
val make_frac : int * int -> rational
val add : rational -> rational -> rational
val string_of_rational : rational -> string
end
(* it turns out while RATIONAL_B is fully powerful, it
doesn't "break anything" to expose the whole function.
*)
module type RATIONAL_C = sig
type rational
exception BadFrac
val whole : int -> rational (* can expose Whole via function *)
val make_frac : int * int -> rational
val add : rational -> rational -> rational
val string_of_rational : rational -> string
end
(* ---------------------------------------- *)
(* can ascribe any of the three module types above *)
module Rational1 : RATIONAL_C = struct
(*
Invariant 1: all denominators > 0
Invariant 2: rationals kept in reduced form
*)
type rational =
| Whole of int
| Frac of int * int
exception BadFrac
let rec gcd x y =
if x = y then
x
else if x > y then
gcd y x
else
gcd x (y - x)
let reduce r =
match r with
| Whole _ -> r
| Frac (0, _) -> Whole 0
| Frac (n, d) ->
let g = gcd (abs n) d in
if g = d then
Whole (n / d)
else
Frac (n / g, d / g)
(* when making a frac we ban zero denominators and
reduce the fraction
*)
let rec make_frac (n,d) =
if d = 0 then
raise BadFrac
else if d < 0 then
reduce (Frac (-n, -d))
else
reduce (Frac (n, d))
let whole x = Whole x
(* using math properties, both invariants hold of the result
assuming they hold of the arguments *)
let rec add r1 r2 =
match r1, r2 with
| Whole i1, Whole i2 -> Whole (i1 + i2)
| Whole i1, Frac (n2, d2) -> Frac ((i1 * d2) + n2, d2)
| Frac _, Whole _ -> add r2 r1
| Frac(n1,d1), Frac (n2, d2) -> reduce (Frac ((n1 * d2) + (n2 * d1), d1 * d2))
(* given invariant, prints in reduced form *)
let string_of_rational r =
match r with
| Whole i -> string_of_int i
| Frac (n, d) -> string_of_int n ^ "/" ^ string_of_int d
end
(* can ascribe any of the three signatures above *)
(* and **if** we use B or C, this module is *equivalent* to Rational1 *)
(* we choose not to reduce fractions until printing *)
module Rational2 : RATIONAL_B = struct
type rational =
| Whole of int
| Frac of int * int
exception BadFrac
let whole n = Whole n
let rec make_frac (n, d) =
if d = 0 then
raise BadFrac
else if d < 0 then
Frac (-n, -d)
else
Frac (n, d)
(* no call to reduce! *)
let rec add r1 r2 =
match (r1, r2) with
| Whole i1, Whole i2 -> Whole (i1 + i2)
| Whole i1, Frac (n2,d2) -> Frac ((i1 * d2) + n2, d2)
| Frac _, Whole _ -> add r2 r1
| Frac (n1,d1), Frac (n2,d2) -> Frac ((n1 * d2) + (n2 * d1), d1 * d2)
let string_of_rational r =
let rec gcd x y =
if x = y then
x
else if x > y then
gcd y x
else
gcd x (y - x)
in
let reduce r =
match r with
| Whole _ -> r
| Frac (0, _) -> Whole 0
| Frac (n, d) ->
let g = gcd (abs n) d in
if g = d then
Whole (n / d)
else
Frac (n / g, d / g)
in
match reduce r with
| Whole i -> string_of_int i
| Frac (n, d) -> string_of_int n ^ "/" ^ string_of_int d
end
(* this structure uses a different abstract type.
It does not even have signature RATIONAL_A.
For RATIONAL_C, the function whole is availabe at a less
generaly type externally.
*)
module Rational3 : RATIONAL_B = struct
type rational = int * int
exception BadFrac
let rec make_frac (x, y) =
if y = 0 then
raise BadFrac
else if y < 0 then
(-x, -y)
else
(x, y) (* could even return an alias of the argument rather than a copy *)
let whole i = (i, 1)
let add (a, b) (c, d) = ((a * d) + (c * b), b * d)
let string_of_rational (n, d) =
if n = 0 then
"0"
else
let rec gcd x y =
if x = y then
x
else if x > y then
gcd y x
else
gcd x (y - x)
in
let g = gcd (abs n) d in
let num = n / g in
let denom = d / g in
string_of_int num
^
if denom = 1 then
""
else
"/" ^ string_of_int denom
end
(* Note we used explicit modules and module types to show the
concepts, but more common in OCaml is implicit modules:
* foo.ml defines a module Foo
* if foo.mli is present, it is the signature for Foo, else
nothing-is-hidden from other modules (still write Foo.bar)
*)
\ No newline at end of file
(* 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
(* 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 = (* infer val f : int -> int *)
if x > 3
then 42
else x * 2
(*
let g x = (* report type error *)
if x > 3
then true
else x * 2
*)
let x = 42 (* val x : int *)
let f y z w =
if y (* y must be bool *)
then z + x (* z must be int *)
else 0 (* both branches have same type *)
(* f must return an int
f must take a bool, int, and ANYTHING
so val f : bool -> int -> 'a -> int
*)
(*
f : T1 -> T2 [must be a function; all functions take one argument]
x : T1 [must have type of f's argument]
y : T3
z : T4
T1 = T3 * T4 [else pattern-match in let-binding doesn't type-check]
T3 = int [because (abs y) where abs : int -> int]
T4 = int [because add z to an int]
So T1 = int * int
So (abs y) + z : int, so let-expression : int, so body : int, so T2=int
So f : int * int -> int
*)
let f x =
let (y,z) = x in
(abs y) + z
(*
sum : T1 -> T2 [must be a function; all functions take one argument]
xs : T1 [must have type of f's argument]
x : T3 [pattern match against T3 list]
xs' : T3 list [pattern match against T3 list]
T1 = T3 list [else pattern-match on xs doesn't type-check]
0 : int, so case-expresssion : int, so body : int, so T2=int
T3 = int [because x : T3 and is argument to addition]
T2 = int [because result of recursive call is argument to addition]
sum xs' type-checks because xs' has type T3 list and T1 = T3 list
case-expression type-checks because both branches have type int
from T1 = T3 list and T3 = int, we know T1 = int list
from that and T2 = int, we know f : int list -> int
*)
let rec sum xs =
match xs with
| [] -> 0
| x::xs' -> x + (sum xs')
(*
type inference proceeds exactly like for sum for most of it:
broken_sum : T1 -> T2 [must be a function; all functions take one argument]
xs : T1 [must have type of f's argument]
x : T3 [pattern match against T3 list]
xs' : T3 list [pattern match against T3 list]
T1 = T3 list [else pattern-match on xs doesn't type-check]
0 : int, so case-expresssion : int, so body : int, so T2=int
T3 = int [because x : T3 and is argument to addition]
T2 = int [because result of recursive call is argument to addition]
but now to type-check (broken_sum x) we need T3 = T1 and T1 = T3 list,
so we need T3 = T3 list, which is impossible for any T3.
Note: The actual type-checker might gather facts in a different order and
therefore report a different error, but it will report an error.
*)
(*let rec broken_sum xs =
match xs with
| [] -> 0
| x::xs' -> x + (broken_sum x)
*)
(*
First several steps are just like with sum:
length : T1 -> T2 [must be a function; all functions take one argument]
xs : T1 [must have type of f's argument]
x : T3 [pattern match against T3 list]
xs' : T3 list [pattern match against T3 list]
T1 = T3 list [else pattern-match on xs doesn't type-check]
0 : int, so case-expresssion : int, so body : int, so T2=int
recursive call type-checks because xs' has type T3 list, which = T1
and T2=int, so fine argument to addition
so with all our constraints, length : T3 list -> int
so 'a list -> int
*)
let rec length xs =
match xs with
| [] -> 0
| x::xs' -> 1 + (length xs')
(*
f : T1 * T2 * T3 -> T4
x : T1
y : T2
z : T3
both conditional branches must have type T4 (the type of the function body),
so T1 * T2 * T3 = T4 and T2 * T1 * T3 = T4, which means T1 = T2
putting it all together, f : T1 * T1 * T3 -> T1 * T1 * T3
now replace unconstrained types /consistently/ with type variables:
'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
from body of compose being a function, T3 = T4->T5 for some T4 and T5
from g being passed x, T2 = T4->T6 for some T6
from f being passed result of g, T1 = T6->T7 for some T7
from call to f being body of anonymous function, T7=T5
putting it all together:
T1=T6->T5, T2=T4->T6, and T3=T4->T5
so compose: (T6->T5) * (T4->T6) -> (T4->T5)
now replace unconstrained types /consistently/ with type variables:
('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 + Option.get (!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
(* 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 =