In defining types we have essentially three ways. We can either define types explicitly, more or less as type abbreviations, or recursively: here is the definition of the type of trees. You see it is a type with one parameter and in a sense it is a polymorphic type. This is the general pattern of a tree over a given data type of leaves. It has three constructures: empty, which constructs the empty tree, leaf, which is a operator that builds essentially a leaf of type A, and node which combines two trees to a root. And then here we have an example of an abstract data type. Here we define the abstract data type of streams. As you see, we are packaging up a stream. You might know that an A stream is a pair consisting of an element of A, whose first component is an element of A and whose second component is again a stream. And here you see, since we are working in a call-by-value environment, we want to prevent infinite evaluations. We have to freeze the computation packaging it up as a function. And of course since really the argument of the function does not matter we decide that the function has as domain just the unit type. It has two constructors next: given a stream, it gives you the next element of the stream together with the next stream and the function make stream which allows to build a new stream. As you can see the interface of such an abstract data type just lets you build streams and access next components of a stream. It does not really care what sort of implementation we have used. Then we shall discuss raising and handling of exceptions, possibly with parameters. We shall discuss imperative features. We will see that in fact although we have a very expressive polymorphic type discipline, when it comes to discussing functions which have non-functional features, as is the case where functions have exceptions, or imperative features. It is no longer the case that we can be so flexible in having polymorphic expressions. And in fact the compiler makes a distinction, a syntactic distinction between expansive and non expansive expressions. And only non-expansive expressions can have polymorphic types. Expansive expressions, that is expressions which create new references or new exceptions, have to be monomorphic otherwise we can break the type safety. Finally in discussing modules we will structures, signatures, functors and discuss the notion of sharing.

---