Alice Project


________ Overview ____________________________________________________

For particular programming tasks - especially when transferring data between different processes - it is desirable to relax the strict static rules of ML and shift some of the type checking to runtime. For this purpose, Alice ML provides runtime typing through the concept of packages.

A package is a value of abstract type package that encapsulates some value, along with its (runtime) type. Accessing the value inside a package is only possible via an explicit unpack operation, which requires giving the expected type. A dynamic type check verifies that the actual and the expected type match.

Instead of just values of the core language, packages may actually contain arbitrary higher-order modules, paired with their signature. This way, modules can be passed and stored as first-class values.

________ Packages ____________________________________________________

Creating packages

A package is created using the pack expression:

pack strexp : sigexp

This expression creates a package containing the module denoted by strexp. The module must (statically) match the given signature sigexp. This signature will be the package signature.

Unpacking packages

A module can be projected out of a package using the inverse unpack form:

unpack exp : sigexp

Dynamically, if the package signature of the package returned by expression exp matches the signature sigexp, this structure expression evaluates to the module encapsulated in the package. Otherwise, it raises the exception Package.Mismatch. Since Alice ML supports local modules, the exception may be handled in the usual way.

Statically, the expression has the signature type denoted by sigexp, as it can only be evaluated successfully if it delivers a suitable module. Any use of the unpacked module will be statically type-safe.


We can inject the library module Word8 into a package:

val p = pack Word8 : WORD

This package may then be passed to some client that may unpack it as follows:

structure Word' = unpack p : WORD

The package signature matches the expected signature, so that unpacking succeeds. The client may thus access the Word' structure as usual:

print (Word'.toString (Word'.fromInt 255))

The package can also be unpacked using a more general signature that contains fewer items:

structure WordFromInt = unpack p : sig type word  val fromInt : int -> word end

The full module subtyping rules apply to the unpack type check, so that unpacking is quite robust with respect to extensions to interfaces of modules packed elsewhere. In particular, arbitrary items may be added.


The package signature of p is WORD. That signature does not specify anything about the identity of the contained word type. Consequently, it will be abstract and incompatible with the original type after unpacking:

Word'.toString (Word8.fromInt 255)   (* static type error! *)

In order to make the unpacked structure statically compatible with Word8, it has to be unpacked with a more specific signature:

structure Word8' = unpack p : WORD where type word = Word8.t

In the scope of this declaration, the above expression is legal.

Type constraints can also be used to specify sharing between different packages:

fun g(p1, p2) =
	signature S  = sig type t  val x : t  val f : t -> int end
	structure X1 = unpack p1 : S
	structure X2 = unpack p2 : S where type t = X1.t
	X2.f X1.x

In this example, the types t in both packages are unknown. However, they might be known to be equal. The second unpack expression enforces this requirement dynamically, by specifying the necessary type equivalence.

Sometimes it is desirable to make a package fully opaque. The derived syntax

pack strexp :> sigexp

enables this. When Word8 is packed like

val p = pack Word8 :> WORD

The attempt to unpack it transparently,

structure Word8' = unpack p : WORD where type word = Word8.t

will fail.

________ First-class modules _________________________________________

The main application for first-class modules in the form of packages is in combination with pickling, where they allow to make implementations of abstract types or whole programs persistent, and with distributed programming, where they enable transfer of program components to remote locations.

Packages can also be used for encoding more traditional idioms requiring first-class modules. For example, the implementation of a map module may be chosen dependent on some condition, assuming the alternative implementations satisfy a common signature:

structure Map = unpack (if maxElems < 100
                        then pack BinTreeMap : MAP)
			else pack HashTableMap : MAP) : MAP

________ Dynamic typing ______________________________________________

Packages rely on dynamic typing, thus types (and signatures) have a dynamic semantics. An important property of the semantics is that it does not undermine any properties of the static type system. In particular, all abstraction guarantees carry over from static to dynamic typing: no type abstraction can be broken by use of the dynamic typing implied by packages. For example, the following declarations will not evaluate successfully:

signature S      = sig    type t       val x : t end
structure X :> S = struct type t = int val x = 9 end

val p = pack X : S

structure X' = unpack p : S where type t = int

The unpacking as shown here will always fail, since the type X.t is dynamically abstract. The only possible type that t can be specified equal to is the abstract type itself:

structure X' = unpack p : S where type t = X.t

The following also works (see sharing):

structure X1 = unpack p : S
structure X2 = unpack p : S where type t = X1.t

The dynamic semantics of types is as follows:

Note that polymorphic functions are still parametric and thus can be interpreted in a type erasure semantics. To pass type information, a function has to be lifted to the functor level. Due to local modules this is possible in most cases.

________ Syntax summary ______________________________________________

Derived forms have been marked with (*).

exp ::= ...
pack atstrexp : atsigexp transparent packing
pack atstrexp :> atsigexp opaque packing (*)
strexp ::= ...
unpack infexp : sigexp unpacking

Derived forms

pack atstrexp :> atsigexp pack (atstrexp :> atsigexp) : atsigexp

last modified 2005/10/05 20:29