You probably have a particular idea of what a "constructor" is from C++. Forget what you know. In general, for any language, a "constructor" is an expression that creates a fresh value of a particular type. Languages commonly support two kinds of types:
ML has built-in constructor functions corresponding to each of the built-in compound types:
x :: xs (* List constructor: 2 components (head, tail) *)
(x, y, z) (* Tuple constructor: 3 components (#1, #2, #3) *)
{x=p, y=q} (* Record constructor: 2 components (#x, #y) *)
The square bracket constructor [a,b,c] is just
"syntactic sugar" for the :: constructor form.
_ pattern),Patterns are used on the "left-hand side" whenever a binding occurs. So far, we know of two places where bindings may occur:
val bindingsFor function arguments, the "left-hand side" is the formal parameter, and the "right-hand side" is the actual parameter.
Intuitively, "matching" allows us to perform an implicit computation when we bind a value. The computation attempts to answer the question: "Does the thing on the right hand side have a shape and value like the thing on the left-hand side?" (As an incidental bonus, we can bind designated pieces of the right-hand side to identifiers, for later use.)
If you think about this intuition for a while, you will see why
it makes sense that constructors, and not arbitrary expressions,
are allowed in a pattern: constructors unambiguously describe
"shapes" of data. By contrast, operators like addition (op
+) and list append (@) do not
unambiguously describe the shape of their arguments. For example,
if you have the list
[1, 2, 3, 4]
that was constructed by appending two other lists
x and y, you cannot precisely deduce the
identity of x and y! On the other hand,
if you know that the list above was constructed using
::, then you can unambiguously deduce the
identity of the parts.
Random historical trivia: the idea of pattern-matching as a style of describing computation comes from Prolog and the family of logic programming languages.
Notice that patterns are recursive (case (iv) from the previous page). In determining whether two patterns "match", we can therefore use a recursive algorithm, in pseudocode:
fun matches(left, right) =
if left is a constant then
if left = right then true else false
else if left is a variable then true
else if left is a wildcard then true
else if left is a compound constructor then
if right has the same top-level constructor then
if each component of left matches each component of right then
true
else
false
else
false
else (* left may not appear in a pattern! *)
raise some kind of error
Trace the execution of the pattern-matching algorithm over the following value bindings:
val 3 = 3;
val 3 = 4;
val _ = "walrus";
val (3+5, x) = (8, 9);
val x :: _ :: xs = [2,3,4];
val ({baz="hi", foo=seal}, fish::nil) = ({foo="bar", baz="hi"}, [827]);
In this type system, it is impossible to perform any illegal operation on any value. Furthermore, it is impossible to mingle values of inappropriate type.
Obviously, this type system is useless, because it is not permissive enough. That is, we cannot express any interesting programs. Here is another type system:
This type system is useless as well, but for a different reason: a programmer can write anything, including ridiculously incorrect programs. The type system is not restrictive enough to express any useful properties. (Some people wouldn't even call this a type system.)
A good type system is expressive: it allows the programmer to write interesting legal programs, but also to check interesting properties and restrictions for these programs.
At a very high level, here is the informal algorithm for determining types:
Note that the second definition implies that "how values are used" produces constraints on the types of values. This statement, by itself, is fairly intuitive. The way that type constraints are produced can be called the inference rules of the system. Inference rules are commonly written in the following format:
"If it rains, I will get wet." "It rains."
----------------------------------------------------
"I will get wet."
The "premises" of the rule are stated above the line, and the "conclusion" of the rule is below the line. We say that if the premises are true, then the conclusion is true. Here's a simple type inference rule:
p:t0 x:t1 y:t2 t = t1 = t2 t0 = bool
---------------------------------------------
(if p then x else y):t
This means that "if x is of type t1, and y is of type t2, then, when you see the expression (if p then x else y), assign it the type t, where t = t1 = t2. Also, unify the condition p with bool." In other words, we must unify the types of the two branches of the if/then/else, and the entire expression should in turn be unified with the resulting type.
The complete ML type system has many inference rules (and, actually, real type theorists use a rather different format for the rules). However, here are a few more in the same style as the above:
x:t1 xs:t2 list t1 = t2
--------------------------------
(x::xs):t2 list f:t0 -> t1 x:t2 t = t1 t0 = t2
----------------------------------------
f(x):t
x:t1 y:t2
------------------------
(x, y):t1 * t2
x:t1 y:t2 t1 = t2 = int
----------------------------------
(x mod y):int
x:t1 y:t2 t1 = t2 = bool
-----------------------------
(x andalso y): bool
Essentially, every time you see an = sign for types, you should perform unification. Individually, the rules for unification are pretty simple. Using them in a deterministic algorithm that actually computes all the types for every expression in the program takes some effort; the algorithm for ML's type inference is due to Robin Milner. We'll never ask you to use Milner's algorithm, but you should be able to systematically construct an argument for the typing of a function.
What is unification? Actually, unification over types is a lot
like pattern matching over values. There are various type
constructors, like the tuple type constructor *, the
function type constructor -> and the list type
constructor list (which is a unary constructor,
i.e. a constructor with only one argument: the list element
type).
I won't go into unification in detail, but here are some sample unifications (note: this is NOT ML code, this is a series of examples of how types unify). Technically, the result of unification is a type variable substitution and a "unified type" for the entire expression; however, to save space, I'll write only the substitutions you need to perform to make the resulting types unify:
unify('a -> 'b, 'c) => 'c = 'a -> 'b
unify('a * 'b, 'c list) => ERROR, * type constructor cannot match list
unify(('a * 'b) list, ('c * ('d * 'e -> 'f)) list)
=> 'b = ('d * 'e -> 'f)
unify(('a -> 'b) * 'c, 'd * ('e list * 'f))
=> 'd = 'a -> 'b
'c = 'e list * 'f
If you draw the type trees for these expressions, you'll see it looks a lot like the pattern matching algorithm---they're both just tree matching.
fun myIf(x, y, z) = if x then y else z;
fun squid(a, b, c) =
let val d = [2.0,3.0];
val e:(int * (int * string)) = (3, c);
in
if a > hd(d) then [hd(b), #2(c)] else tl(b)
end;
Like most languages, ML allows you to define your own named types. There are two principal mechanisms for doing this: type synonyms, and datatypes (actually there are some elaborations on these themes, but we'll stick to these two).
Type synonyms simply allow you to say that a given name means the same thing as some other type name:
(* A long and basically pointless type synonym *)
type StringIntTuple = (int * string);
(* Notice the syntax for declaring polymorphic synonyms *)
type 'a chain = 'a list;
type ('a, 'b) pair = ('a * 'b);
(* Function types are some of the best candidates for synonyms. *)
type MyWeirdType = (int * real * string list) -> (string * real);
Type synonyms are useful when you want to use the
x:t notation for explicitly declaring types. They're
also a form of documentation, and they have other uses when
defining structures and signatures (which you'll learn about in
the next few lectures).
More interesting, perhaps, are datatypes. A datatype declaration creates a brand new, fresh type, and a set of constructors for that type:
(* General form of a datatype declaration *)
datatype TypeName = Constructor1 of (type1 * type2 * ... * typeN)
| Constructor2 of (type1' * type2' * ... * typeN')
| ... ;
(* A color datatype... 3 real-valued components, for red/green/blue *)
datatype Color = RGB of real * real * real;
(* A Color value *)
val red = RGB(1.0, 0.0, 0.0);
(* A "union" datatype... can wrap either an int or a string. *)
datatype IntegerOrString = Int of int | Str of string;
(* Two values of the above type... *)
val x = Int(0);
val y = Str("hi");
(* A string tree datatype: either the empty tree, or a node with a
string and two subtrees. *)
datatype StringTree = Empty
| Node of string * StringTree * StringTree;
val t = Node("hi", Empty, Node("bye", Empty, Empty));
(* Datatypes also fill the role that "enums" fill in C... *)
datatype States = Yes | No | Maybe;
Recall that constructors can be used in patterns. Datatype constructors behave exactly like the built-in constructors, except for a bit of syntax:
(* Extracts the left subchild of a tree. *)
fun leftChild(Empty) = raise Fail("Tried to get child of Empty.")
| leftChild(Node(_, L, _)) = L;
Each datatype declaration is distinct; if you have to datatypes with identical cases, they are not the same type. Type theorists say that datatypes have "by-name type equivalence", whereas type synonyms have "structural type equivalence".
Suppose you had a Color datatype defined as above. Define a
function that, given a point in the real plane---i.e., a record of
type {x:real, y:real}---returns a color that is black
(i.e., RGB(0.0, 0.0, 0.0)) if the point is less than
2.0 units from the origin, and white (RGB(1.0, 1.0,
1.0)) otherwise.
This is a functional image: it is a function that defines the black circle centered at 0, with radius 2. Your ML project will employ functional images, so if you start to wrap your head around this idea now, you'll find the homework easier.
Now, define a function that takes two parameters: a foreground color, and a radius; and that returns a circle function with the given color and radius. This is a generator for functional images.