alice
manual.


Alice Project

packages


________ 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 longstrid :> longsigid

This expression creates a package containing the module denoted by longstrid. The module must (statically) match the given signature longsigid. 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.

Example

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.

Sharing

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 package signature compatible with Word8, it has to be specified more specifically:

val p = pack Word8 :> (WORD where type word = Word8.t)

Now the package can be unpacked similarly as

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

enabling

Word8'.toString (Word8.fromInt 255)

Due to subtyping, it is still valid to unpack it abstractly:

structure Word' = unpack p : WORD

but of course, Word'.word is again statically different from Word8.word.

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

fun g(p1, p2) =
    let
	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)
    in
	X2.f X1.x
    end

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.


________ 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 type from the package itself (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.

Packing performs sealing to ensure consistency between the package signature and dynamic types contained in the packaged module. If no sealing took place, anomalies would be possible, like successful evaluation of the following program:

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

val p1 = pack X :> S
structure X1 = unpack p1 : S

val p2 = pack X1 :> (S where type t = X1.t)
structure X2 = unpack p2 : (S where type t = int)

Here, X has a transparent type t = int, but the package signature makes it abstract. Consequently, unpacking it under the constraint t = int would be unsuccessful. However, if packing would not perform sealing, X1.t indeed was int dynamically, so that an additional packing/unpacking step sufficed to reveal the implementation type. A package could leak information that was not appearent from its signature.

On the other hand, unpacking is transparent. The following program evaluates successfully:

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

val p1 = pack X :> (S where type t = int)
structure X1 = unpack p1 : S

val p2 = pack X1 :> (S where type t = X1.t)
structure X2 = unpack p2 : S where type t = int

In this case, the second pack expression makes the signature of p2 transparent relative to p1, without knowing the actual type t contained in p1. Note that it is not possible to specify t = int at this point, because statically, X1.t is abstract since it has been unpacked abstractly.

Transparent semantics of unpacking are necessary to allow expressing sharing.

Implementation limitations

The dynamic semantics of sealing is currently not implemented faithfully for polymorphic signatures: if the signature is not statically known because it is a functor parameter, no runtime sealing will be performed. A simple example is:

functor Abs(signature S structure X : S) = X :> S

structure M  = struct type t = int val x = 13 end
structure M' = Abs(signature S = sig type t val x : t end
                   structure X = M)

In this example, the runtime representation of M'.t will still be int and not an abstract type. However, since the static semantics work correctly, this can only be observed by going through a package:

structure P = Package.PackVal(type t = M'.t val x = M'.x)
structure X = Package.UnpackVal(val package = P.package type t = int)

val y = X.x + 1    (* Ah! *)

Unpacking should fail in this example, but currently does not.


________ Value packages ______________________________________________

Often it is not necessary to package whole modules. For convenience, the Package module thus provides functors that allow packaging of simple core values. Essentially, this provides a type dynamic, as available in a few other statically-typed languages.


________ Syntax summary ______________________________________________

exp ::= ...
pack atstrexp :> atsigexp packing
strexp ::= ...
unpack infexp : sigexp unpacking


last modified 2004/04/13 11:29