env :: n || n
env :: e1 + e2 || n
if env :: e1 || n1 and env :: e2 || n2
and n is the result of applying
primitive operation + to n1 and n2
env :: (e1, e2) || (v1, v2)
if env :: e1 || v1 and env :: e2 || v2
env :: fst e || v1
if env :: e || (v1,v2)
env :: Left e || Left v
if env :: e || v
env :: match e with Left x -> e1
| Right y -> e2 || v1
if env :: e || Left v and
env+{x=v} :: e1 || v1
env :: let x = e1 in e2 || v2
if env :: e1 || v1 and
env+{x=v1} :: e2 || v2
env :: (fun x -> e) || <<fun x -> e, env>>
env :: e1 e2 || v
if env :: e1 || <<fun x -> e, env'>>
and env :: e2 || v2
and env' + {x=v2} :: e || v
env :: let rec f x = e1 in e2 || v
if env + {f = <<f, fun x -> e1, env>>}
:: e2 || v
env :: e1 e2 || v
if env :: e1 || <<f, fun x -> e, env'>>
and env :: e2 || v2
and env' + {x=v2,f=<<f, fun x -> e, env'>>}
:: e || v
1. Write a recursive fold function that takes in one argument for each variant of the datatype.
2. That fold function matches against the datatype variants, calling itself recursively on any instance of the datatype that it encounters.
3. When a variant carries data of a type other than the datatype being folded, use the appropriate argument to fold to incorporate that data.
4. When a variant carries no data, use the appropriate argument to fold to produce an accumulator.
let rec fold_left (f : 'a -> 'b ->'a) (acc : 'a) (lst : 'b list): 'a =
match lst with
[] -> acc
| x :: xs -> fold_left f (f acc x) xs
fold_left : 'a -> 'b -> 'a -> 'a -> 'b list -> 'a
let rec fold_right (f : 'a -> 'b -> 'b) (l : 'a list) (acc : 'b) : 'b =
match l with
[] -> acc
| x :: xs -> f x (List.fold_right f xs acc)
fold_right: 'a -> 'b -> 'b -> 'a list -> 'b ->'b
Example of Generalized fold:
type
'a exprTree =
| Val of 'a
| Unop of ('a -> 'a) * 'a exprTree
| Binop of ('a -> 'a -> 'a) * 'a exprTree * 'a exprTree
let rec exprTree_fold (foldVal) (foldUnop) (foldBinop) = function
| Val x -> foldVal x
| Unop (f, t) -> foldUnop f (exprTree_fold foldVal foldUnop foldBinop t) | Binop (f, t1, t2) -> foldBinop f (exprTree_fold foldVal foldUnop foldBinop t1) (exprTree_fold foldVal foldUnop foldBinop t2)
;;
e1 + e2 --> e1' + e2
if e1 --> e1'
v1 + e2 --> v1 + e2'
if e2 --> e2'
n1 + n2 --> n3
where n3 is the result of applying primitive operation +
to n1 and n2
(e1, e2) --> (e1', e2)
if e1 --> e1'
(v1, e2) --> (v1, e2')
if e2 --> e2'
fst (v1,v2) --> v1
Left e --> Left e'
if e --> e'
match e with Left x -> e1 | Right y -> e2
--> match e' with Left x -> e1 | Right y -> e2
if e --> e'
match Left v with Left x -> e1 | Right y -> e2
--> e1{v/x}
match Right v with Left x -> e1 | Right y -> e2
--> e2{v/y}
let x = e1 in e2 --> let x = e1' in e2
if e1 --> e1'
let x = v in e2 --> e2{v/x}
e1 e2 --> e1' e2
if e1 --> e1'
v e2 --> v e2'
if e2 --> e2'
Capture Avoiding Substitution
(fun x -> e) v2 --> e{v2/x}
(Left e'){e/x} = Left e'{e/x}
(Right e'){e/x} = Right e'{e/x}
(match e' with Left y -> e1 | Right z -> e2){e/x}
= match e'{e/x} with Left y -> e1{e/x} | Right z -> e2{e/x}
(match e' with Left x -> e1 | Right z -> e2){e/x}
= match e'{e/x} with Left x -> e1 | Right z -> e2{e/x}
(match e' with Left y -> e1 | Right x -> e2){e/x}
= match e'{e/x} with Left y -> e1{e/x} | Right x -> e2
(match e' with Left x -> e1 | Right x -> e2){e/x}
= match e'{e/x} with Left x -> e1 | Right x -> e2
(let x = e1 in e2){v/x} = let x = e1{v/x} in e2
(let y = e1 in e2){v/x} = let y = e1{v/x} in e2{v/x}
(e1,e2){e/x} = (e1{e/x}, e2{e/x})
(fst e'){e/x} = fst e'{e/x}
Start off with this functor for Intervals.
module Make_interval :
functor (Endpoint : Comparable) ->
sig
type t = Interval of Endpoint.t * Endpoint.t | Empty
val create : Endpoint.t -> Endpoint.t -> t
val is_empty : t -> bool
val contains : t -> Endpoint.t -> bool
val intersect : t -> t -> t
end
Now, the functor does not have an abstract type. Because, the user can see the type in the functor. So, we have to hid that type t impelementation. There's a problem with Make_interval. The invariant is enforced by the create function, but because Interval.t is not abstract, we can bypass the create function. So you do something like this with sharing constraints: :
module Make_interval(Endpoint : Comparable) : Interval_intf with type endpoint = int struct
type endpoint = Endpoint.t
type t = | Interval of Endpoint.t * Endpoint.t
| Empty
Syntax:
e1 + e2
Type-checking:
If e1 and e2 have type int, then e1 + e2 has type int
Syntax: e1 < e2
Type-checking: if e1 has type int and e2 has type
int then e1<e2 has type bool
Syntax: if e1 then e2 else e3
Type-checking: if e1 has type bool and, for some type t, both e2 and e3 have type t, then if e1 then e2 else e3 has type t
Simplified syntax:
let x = e1 in e2
Type-checking:
If e1:t1, and if e2:t2 under the assumption that
x:t1, then let x = e1 in e2 : t2
Syntax: e0 (e1,...,en)
Type-checking:
If: e0 has some type (t1 * ... * tn) -> t
and e1 has type t1, ..., en has type tn
Then e0 (e1,...,en) has type t
Syntax: {f1=e1;...;fn=en}
Type-checking:
If e1:t1ande2:t2 and ... en:tn, and if t is a declared type of the form {f1:t1, ..., fn:tn} , then{f1 = e1; ...; fn = en}:t
Syntax: e.f
Type-checking:
If e:t1 and if t1 is a declared type of the form {f:t2, ...} , then e.f: t2
None has type ‘a option
– much like [] has type ‘a list – None is a value
Some e :t option ife:t
– much like e::[] has type t list if e:t – If e-->v then Some e-->Some v
Note- Datatype VS Records Table
|
Declare
|
Build/Construct
|
Access/ Destruct
|
|
|
DataType
|
type
|
Constructor name
|
Pattern matching with match
|
|
Record
|
type
|
Record expression with {...}
|
Pattern matching with let OR field selection with dot operator .
|
|
Tuple
|
N/A
|
Tuple expression with (...)
|
Pattern matching with let OR fst or snd
|
No comments yet.
Cheatography n. The art of mapping complex subjects into clear, instantly navigable reference guides.