Expressions: e ::= c (* constants *) | id (* variables *) | (fn (id:t) => e) (* anonymous functions *) | e1(e2) (* function applications *) | u e (* unary operations, ~, not, etc. *) | e1 b e2 (* binary operations, +,*,etc. *) | (e1,...,en) (* tuples *) | #i e (* field projection for tuples *) | {lab1=e1,...,lab=en} (* records *) | #lab e (* field projection for records *) | Id | Id(e) (* data constructors *) | (case e of p1 => e1 | ... | pn => en) (* case expressions *) | let d in e end (* let expressions *) | (fun id(id1:t1):t2 = e) (* recursive functions *)
Declarations: d ::= val p = e (* value declarations *) | fun id(id1:t1):t2 = e (* function declarations *)
Patterns: p ::= _ (* wildcard *) | c (* constant pattern *) | id (* variable pattern *) | (p1,...,pn) (* tuple patterns *) | {lab1=p1,...,labn=pn} (* record pattern *) | Id | Id(p) (* data constructor pattern *)
Values: v ::=
c (* constant values *)
| (fn (id:t):t' => e) (* anonymous functions *)
| (v1,...,vn) (* tuples of values *)
| {lab1=v1,...,labn=vn} (* records of values *)
| Id | Id(v) (* data constructors *)
Rule #E1 [constants]: constants evaluate to themselves
eval(c) = c
Rule #E2 [functions]: anonymous functions evaluate to themselves
eval(fn (id:t) => e) = (fn (id:t) => e)
Rule #E3 [function calls]: to evaluate e1(e2), evaluate e1 to a function (fn (id:t) => e), then evaluate e2 to a value v, then substitute v for the formal parameter id within the body of the function e to yield an expression e'. Finally, evaluate e' to a value v'. The result is v'.
eval(e1(e2)) = v' where (0) eval(e1) = (fn (id:t) => e) (1) eval(e2) = v (2) substitute([(id,v)],e) = e' (3) eval(e') = v'
Rule #E4 [unary ops]: to evaluate u e where u is a unary operation such as not or ~, evaluate e to a value v', then perform the appropriate unary operation on the value v' to get the result v.
eval(u e) = v where (0) eval(e) = v' (1) v = apply_unop(u,v')
Rule #E5 [binary ops]: to evaluate e1 b e2 where b is a binary operation such as +, *, -, etc. evaluate e1 to a value v1, then evaluate e2 to a value v2, then perform the appropriate operation on the values v1 and v2 to get the result v.
eval(e1 b e2) = v where (0) eval(e1) = v1 (1) eval(e2) = v2 (2) v = apply_binop(b,v1,v2)
Rule #E6 [tuples]: to evaluate a tuple expression (e1,e2,...,en), evaluate the sub-expressions left-to-right and collect the results into a tuple value..
eval((e1,e2,...,en)) = (v1,v2,...,vn) where vi = eval(ei)
Rule #E7 [tuple projection]: to evaluate #i e, evaluate e to a tuple value (v1,v2,...,vn) and then return vi.
eval(#i e) = vi where eval(e) = (v1,v2,...,vn)
Rule #E8 [records]: to evaluate a record expression {lab1=e1,lab2=e2,...,labn=en}, evaluate the sub-expressions left to right and collect the results into a record value. Then sort the fields of the record by label (in ascending lexicographic order.)
eval({lab1=e1,lab2=e2,...,labn=en}) = sort_fields({lab1=v1,...,labn=vn})
where eval(ei) = vi
Rule #E9 [record projection]: to evaluate #lab e, evaluate e to a record value {lab1=v1,lab2=v2,...,labn=vn} and return the value vi such that lab = labi.
eval(#lab e) = vi where
(0) eval(e) = {lab1=v1,lab2=v2,...,labn=vn}
(1) lab = labi
Rule #E10 [simple data constructors]: non-value carrying data constructor Id (such as nil, NONE, etc.) evaluate to themselves.
eval(Id) = Id
Rule #E11[value-carrying data constructors]: To evaluate a data constructor applied to an argument Id(e), evaluate the argument e and then return the data constructor value Id(v).
eval(Id(e)) = Id(v) where eval(e) = v
Rule #E12[case]: to evaluate (case e of p1 => e1 | p2 => e2 | ... | pn => en), evaluate e to a value v. Then try to match v against the pattern p1 (see below for the definition of match). If the match succeeds, we get a substitution S1 which maps variables in the pattern to values. Perform the substitution S1 on e1 to yield the expression e1' and then evaluate e1' to get the result. If v fails to match the pattern p1, then try to match v against the pattern p2. If the match succeeds, we get a substitution S2. Perform the substitution S2 on e2, evaluate the resulting expression to get the final answer. If the match fails, we move on to the third pattern and so forth.
eval(case e of p1 => e1 | p2 => e2 | ... | pn => en) = v' where
(0) eval(e) = v
(1) if match(v,p1) = S1:
(*) substitute(S1,e1) = e1'
(*) eval(e1') = v'
(2) if match(v,p1) FAILS and match(v,p2) = S2:
(*) substitute(S2,e2) = e2'
(*) eval(e2') = v'
(3) if match(v,p1) and match(v,p2) FAIL and match(v,p3) = S3:
(*) substitute(S3,e3) = e3'
(*) eval(e3') = v'
...
(n) if match (v,pi) FAILS for 1<=i<n, and match(v,pn) = Sn:
(*) substitute(Sn,en) = en'
(*) eval(en') to get v'
Rule #E13[let]: to evaluate let d in e end, evaluate the declaration d to get a substitution S. Perform the substitution S on e yielding a new expression e'. Then evaluate e' to get the final answer.
eval(let d in e end) = v where (0) eval_decl(d) = S (1) substitute(S,e) = e' (2) eval(e') = v
Rule #E14[fun expressions]: to evaluate a recursive function expression (fun f(x:t):t' = e), we "unroll" the function once. In other words, we return the anonymous function (fn (x:t) => e') where e' is the result of substituting (fun f(x:t):t' = e) for the identifier f within the body e.
eval(fun f(x:t):t' = e) = (fn (x:t):t' => e') where substitute([f,(fun f(x:t):t' = e)],e) = e'.
Rule #D1[val declarations]: to evaluate a declaration val p = e, evaluate e to a value v and match v against the pattern p to yield a substitution S. The substitution S is the result of the declaration.
eval_decl(val p = e) = S where (0) eval(e) = v (1) match(v,p) = S
Rule #D2[fun declarations]: to evaluate a function declaration fun f(x:t):t' =e, return the substitution that maps f to the function expression fun f(x:t):t'=e.
eval_decl(fun f(x:t):t' = e) = [(f,fun f(x:t):t'=e)]
Rule #P1[wildcard patterns]: a value v matches the pattern _ with an empty substitution as the result.
match(v,_) = []
Rule #P2[constant patterns]: the constant value c matches the constant pattern c with an empty substitution as the result. All other values fail to match a constant pattern.
(0) match(c1,c2) = [] when c1 = c2 (1) match(v,c2) = FAIL when v <> c2
Rule #P3[variable patterns]: a value v matches the pattern id (where id is not a data constructor) and returns the substitution that maps id to v.
match(v,id) = [(id,v)]
Rule #P4[tuple patterns]: the tuple value (v1,v2,...,vn) matches the tuple pattern (p1,p2,...,pn) if v1 matches p1 with substitution S1, v2 matches p2 with substitution S2,...,and vn matches pn with substitution Sn. The result of the match is the compound substitution S1 @ S2 @ ... @ Sn (i.e., append all of the substitutions together.) No other values match the tuple pattern.
match((v1,v2,...,vn),(p1,p2,...,pn)) = S where (0) match(v1,p1) = S1 (1) match(v2,p2) = S2 ... (n-1) match(vn,pn) = Sn (n) S = S1 @ S2 @ ... @ Sn
match(v,(p1,p2,...,pn)) FAILS otherwise
Rule #P5[record patterns]: the record value {lab1=v1,...,labn=vn} matches the record pattern {lab1'=p1',...,labn'=pn'} if, when we sort the pattern by field, we get {lab1=p1,...,labn=pn} (i.e., the labels match up after sorting), and v1 matches p1 with S1, v2 matches p2 with S2, ..., and vn matches pn with Sn. The result is the compound substitution S1 @ S2 @ ... @ Sn (i.e., append all the substitutions together.) No other values match the record pattern.
match({lab1=v1,...,labn=vn},{lab1'=p1',...,labn'=pn'}) = S where
(0) sort_fields({lab1'=p1',...,labn'=pn'}) = {lab1=p1,...,labn=pn}
(1) match(v1,p1) = S1
...
(n) match(vn,pn) = Sn
(n+1) S = S1 @ ... @ Sn
match(v,{lab1'=p1',...,labn'=pn'}) FAILS otherwise
Rule #P6[simple data constructor patterns]: The simple data constructor value Id matches the simple data constructor pattern Id with the empty substitution as the result. No other values match the simple data constructor pattern Id.
match(Id,Id) = []
match(v,Id) FAILS otherwise.
Rule #P7[value-carrying constructor patterns]: The value Id(v) matches the pattern Id(p) with substitution S if the value v matches the pattern p with substitution S. No other values match the pattern Id(p).
match(Id(v),Id(p)) = S when match(v,p) = S
match(v,Id) FAILS otherwise.
Substitution:
Recall that a substitution is a finite map from identifiers (variables) to expressions. We represent the substitution as a list of identifiers and expressions (i.e., [(x1,e1),(x2,e2),...,(xn,en)]). We can perform a substitution S = [(x1,e1),(x2,e2),...,(xn,en)] on an expression or declaration by first substituting e1 for x1, then e2 for x2, ..., then xn for en. That is, substitute([],e) = e and substitute((x,e')::rest,e) = substitute(rest, subst(x,e',e)), where we define subst as below. The definition of subst needs an auxiliary function vars(p) which returns the set of variables that occur in a pattern.
subst(x,e,c) = c
subst(x,e,y) = e when x = y
subst(x,e,y) = y when x <> y
subst(x,e,(fn (y:t) => e')) = (fn (y:t) => subst(x,e,e')) when x <> y
subst(x,e,(fn (y:t) => e')) = (fn (y:t) => e') when x = y
subst(x,e,e1(e2)) = (subst(x,e,e1))(subst(x,e,e2))
subst(x,e,u e') = u (subst(x,e,e'))
subst(x,e,e1 b e2) = (subst(x,e,e1)) b (subst(x,e,e2))
subst(x,e,(e1,...,en)) = (subst(x,e,e1),...,subst(x,e,en))
subst(x,e,#i e') = #i (subst(x,e,e'))
subst(x,e,{lab1=e1,...,labn=en}) = {lab1=subst(x,e,e1),...,labn=subst(x,e,en)}
subst(x,e,#lab e') = #lab (subst(x,e,e'))
subst(x,e,Id) = Id
subst(x,e,Id(e')) = Id(subst(x,e,e')
subst(x,e,case e' of p1 => e1 | ... | pn => en) =
case (subst(x,e,e')) of p1 => e1' | ... | pn => en'
where ei' = ei if x is in vars(pi)
otherwise ei' = subst(x,e,ei)
subst(x,e,let val p = e1 in e2 end) =
let val p = subst(x,e,e1) in e2' end
where e2' = e2 if x is in vars(p)
otherwise e2' = subst(x,e,e2)
subst(x,e,let fun f(y:t):t'=e1 in e2 end) =
let fun f(y:t):t'= e1' in e2' end
where e1' = e1 if x = f or x = y
otherwise e1' = subst(x,e,e1) and
where e2' = e2 if x = f
otherwise e2' = subst(x,e,e2)
subst(x,e,fun f(y:t):t'=e1) = fun f(y:t):t'=e1'
where e1' = e1 if x = f or x = y
otherwise e1' = subst(x,e,e1)
Intuitively we push the substitution down, replacing all free occurrences of x (i.e., uses of x) with the new expression e. Note that we stop pushing the substitution down when we encounter a binding occurrence of the same variable (i.e., a new definition of x that shadows the old one that we're substituting for.) For instance, in (fn (x:t) => e'), x is a binding occurrence and shadows all older definitions of x. Similarly, in (fun f(x:t):t' = e), both f and x are binding occurrences, and in a pattern, a variable is a binding occurrence. All other occurrences of variables are said to be free occurrences.
In general, we evaluate expressions in a left-to-right, inner-most to outer-most fashion.
eval takes an expression and yields a value.
eval_decl takes a declaration and yields a substitution.
match takes a value and a pattern and possibly yields a substitution -- it can also FAIL.
A substitution is a mapping from identifiers to expressions. We represent the substitution as a list of identifiers and expressions here.
SML doesn't really have recursive function expressions, only recursive function declarations. We need recursive function expressions to explain how things evaluate (not to write code.)
Most of the other SML expression forms are derived forms. For instance:
if e1 then e2 else e3 ::=
(case e1 of true => e2 | false => e3)
let d1 d2 ... dn in e end ::=
let d1 in let d2 in ... in let dn in e end ... end end
Thus, if-expressions can be treated as a special case of case-expressions, and let-expressions with more than one declaration can be treated as a sequence of nested let's with one declaration. Similarly, a function that pattern matches on its argument can always be written to do an explicit case expression. It's possible to also encode mutually-recursive functions, but we won't deal with this for now.
Indeed, we can simplify the description by treating tuples as a special case of records, simple data constructors as a special case of compound data constructors (applied to unit), and etc.
The substitution model presented here does not take into account:
However, it covers a relatively large portion of the language and is extremely simple.