Alice Project


________ Overview ____________________________________________________

Alice ML has an extended type language featuring:

________ Structural datatypes ________________________________________

Datatype declarations are not generative: all datatypes that have structurally equivalent definitions are compatible. For example, the following program will elaborate:

datatype 'a t = A | B of 'a | C of 'a t
val x = C (B 0)

datatype 'a u = B of 'a | C of 'a u | A
val y = B 20

datatype 'a v = B of 'a | C of 'a t | A
val z = A

val l = [x,y,z]

This relaxation is particularly interesting for distributed programming.

________ Extensible types ____________________________________________

Extensible types are a generalization of SML's exception type. In effect, the programmer can arbitrarily introduce new sum types similar to exn, which have a potentially unlimited set of constructors.

An extensible type is declared as follows:

exttype 'a message

Fresh constructors are introduced as follows:

constructor DoThis of int : 'a message
constructor DoThat of bool * 'a : 'a message
constructor StopIt : 'a message
constructor Abort = StopIt

Constructors can be added at any point. Like exceptions in SML, constructor declarations are dynamically generative, i.e., the following function returns a different constructor on each call:

fun genMsg() = let constructor C : 'a message in C end

Note that - like exceptions - extensible types do not admit equality, since it is unknown whether there will be any constructors prohibiting that.

Extensible types syntax

dec ::= ...
exttype extbind extensible datatype
constructor econbind generative constructor
extbind ::= tyvarseq tycon extensible datatype
econbind ::= <op> vid <of ty> : tyvarseq longtycon <and econbind> new constructor
<op> vid = <op> longvid <and econbind> synonym
spec ::= ...
exttype extdesc extensible datatype
constructor econdesc generative constructor
extdesc ::= tyvarseq tycon extensible datatype
econdesc ::= <op> vid <of ty> : tyvarseq longtycon <and econdesc> new constructor

Exception declarations and specifications are derived forms in Alice ML, e.g.

exception vid <of ty> constructor vid <of ty: exn
exception vid1 = vid2 constructor vid1 = vid2

________ Type wildcards ______________________________________________

Type annotations may contain underscores as unspecified subcomponents:

fun mapSnd (f : _ -> _ * _) l = (#2 o f) l

Unlike type variables, type wildcards do not enforce polymorphic typing. They are thus suitable to leave out any part of a type annotation:

(3,4,[]) : (_ * int * _ list)

Wildcard syntax

ty ::= ...
_ wildcard

As a restriction, wildcards may not appear in any ty which is part of a typbind, datbind, econbind, exbind or sigexp.

________ Dynamic typing ______________________________________________

The most fundamental extension with respect to the typing discipline of SML is the package type. Values of that type may encapsulate arbitrary values (or modules) along with their type (resp., signature), which is dynamically checked upon extraction of the value. Packages provide a rich form of dynamic typing within the statically typed framework of ML. See the section on packages.

last modified 2007/03/05 18:52