Introduction
------------
This directory contains a *prototype* implementation of the work
reported in my thesis:
1998, Claudio Russo, "Type For Modules",
Department of Computer Science, University of Edinburgh.
This is an interpreter for Standard ML-like Modules language built on
top of a very simple functional Core language, Core-ML. The
implementation supports both higher-order and first-class modules.
Requirements and Installation
-----------------------------
The implementation is written in Caml Light, which is available for a
wide variety of platforms. You will need to install Caml Light 0.7x
in order to compile and run the interpreter. Caml Light is available
on the web at:
http://pauillac.inria.fr/caml/
To *build* the interpreter, start up Caml Light in this directory and
type:
include "build.ml";;
at the prompt. This will compile the source files in
this distribution. It shouldn't take too long, and you can
safely ignore the warning messages.
After building the interpreter, it can be run by typing:
include "link.ml";;
at the Caml Light prompt. This loads in the object files and launches
the interpreter.
Send bug reports to cvr@dcs.ed.ac.uk.
Interacting with the interpreter
--------------------------------
The interpreter has the ability to read *.mod files from the current
directory using the command 'Use x;;' (reading file x.mod). Note that *.mod
files must contain sequences of top-level phrases terminated by
'Quit;;'. The command 'Ctxt;;' displays the current context.
The concrete grammar of the language closely follows the abstract syntax
given in the thesis, except for that Core lambda abstraction is written
using ASCII '\' for tex \lambda, '/\' for tex \Lambda, '!' for tex \forall.
Signature curtailment is written using '>' for tex \succeq,
signature abstraction is written using ASCII '\' for tex \backslash, eg.:
/\('a, 'b). 'a -> 'b (a parameterised simple type taken a 2-tuple of type arguments)
!'a,'b. 'a -> b (a universally quantified simple type)
\i.i (the Core ML identity function)
struct val x = 1 end > sig end (curtailment)
struct val x = 1 end \ sig end (abstraction)
Semantic objects (types) are printed using '/\' for tex \Lambda, '!'
for tex \forall and '?' for tex \exists. Binders binding empty sets of
variables are omitted.
Use uppercase identifiers for modules and signature, lowercase for
types, values and lambda-bound identifiers. Due to parsing
difficulties, module expressions and signatures should be
parenthesised using *curly* brackets '{' '}', while core type and
value expressions should be parenthesised using ordinary parenthesis
'('')'.
The interpreter goes beyond the thesis and supports signature
abbreviations and "with" constraints (see the file sigs.mod for
examples).
Example files
-------------
intro.mod simple examples from Thesis Section 2.1.
poly.mod examples of Higher-Order Modules from Thesis Chapter 5.
sieve.mod an example of First-Class Modules from Thesis Chapter 7.
array.mod another example of First-Class Modules from Thesis Chapter 7.
inference.mod tricky type inference examples from Thesis Chapter 8.
sigs.mod examples of signature abbreviations and 'with' constraints (see the grammar).
This goes beyond the Thesis.
Concrete Grammar
----------------
(when in doubt, parenthesise!)
t := t, u, ... type identifiers
(alpha-numeric identifiers starting with a *lowercase* letter)
x := x, y, ... value identifiers
(alpha-numeric identifiers starting with a *lowercase* letter)
X := X, Y, F, G ... module identifiers
(alpha-numeric identifiers starting with an *uppercase* letter)
I := S, T, ... signature identifiers
(alpha-numeric identifiers starting with an *uppercase* letter)
(* top-level phrases (terminated by ';;' (double semicolons) *)
p ::= type t = d;; type definition
| val x = e;; value definition
| module X = m;; module definition
| signature I = S;; signature abbreviation
| : S;; immediate signature
| m;; immediate module expression
| Use x;; textually include file named 'x.mod' from the current directory
(x is an alpha-numeric identifier starting
with a lower-case letter)
'x.mod' should contain a sequence of top level phrases
terminated by 'Quit;;'
| Ctxt;; displays the current context;;
| Set k;; set flag to show kinds on type variables
| Clear k;; clear flag to show kinds on type variables
| Quit;; exit the interpreter
(also used to terminate a file x.mod).
(* Modules *)
B ::= type t = d; B type definition
| type t : k; B type specification
| val x : v; B value specification
| module X : S; B module specification
| empty body
S ::= sig B end structure signature
| funsig(X:S)S functor signature
| I signature identifier
| S with C0 with constraint
| {S} parenthesised signature (USE CURLY BRACKETS)
CO ::= (X)C0 functor range constraint (functor parameter X)
| BC signature body constraint
C ::= (X)C0 functor range constraint (functor parameter X)
| .BC signature body constraint
BC ::= t = d type constraint
| X C subsignature constraint (on module component X)
do ::= t type identifier
| m.t type projection
b ::= type t = d; b type definition
| val x = e; b value definition
| module X = m; b module definition
| local X = m in b local module definition
| empty body
| signature I = S in b signature abbreviation
m ::= X module identifier
| m.X submodule projection (left associative)
| struct b end structure
| functor(X : S)m functor
| m m functor application (left associative)
| m > S signature curtailment
| m \ S signature abstraction
| {m} parenthesised module (USE CURLY BRACKETS)
vo ::= x value identifier
| m.x value projection
(* Core-ML *)
i ::= i, j, ... lambda-bound identifiers (alpha-numeric identifiers starting with a *lowercase* letter)
'a ::= 'a, 'b, ... simple type variables (alpha-numeric identifiers starting with a *prime*)
k ::= 0, 1, 2, ... kinds (arities)
u ::= 'a simple type variable
| u -> u function type (right associative)
| do (u,..., u_(k-1)) type occurrence applied to k-tuple of type arguments
| do u shorthand for type occurrence applied to 1-tuple of type arguments.
| do shorthand for type occurrence applied to 0-tuple of type arguments.
| ~~ package type
| int integers
| bool booleans
| unit the unit type
| u * u cross product (the type of paired values) (right associative)
| u + u disjoint union (the type of tagged values) (right associative)
| list u the list type
| (u) parenthesised simple type (USE ORDINARY PARENTHESES).
d ::= /\('a_0,...,'a_(k-1)).u parameterised simple type of kind k
| /\ 'a. u shorthand for parameterised simple type of kind 1
| u shorthand for parameterised simple type of kind 0
v ::= !'a_0,...,'a_(n-1).u quantified simple type with n quantified type variables.
| u shorthand quantified simple type with zero quantified type variables.
e ::= i identifier
| \i.e lambda-abstraction
| e e application (left associative)
| vo value occurrence
| pack m as S package introduction
| open e as X:S in e' package elimination
| fix takes the (call-by-value) fix point of a functional
| eq polymorphic equality (curried)
| let i = e in e' polymorphic let
| n for n an integer numeral ...,-1,0,1,...
| ifzero e e' e'' test if e evaluates to zero and evaluating e otherwise evaluate e'.
| - e negate the integer value of e
| * integer multiplication (curried)
| + integer addition (curried)
| divides divides e e' test that e divides e'
| div div e e' returns integral divisor of division of e by e'
! mod mod e e' returns integral remainder of division of e by e'
| true boolean true
| false boolean false
| if e then e' else e'' conditional evaluation
| one the sole value of type 'unit'.
| pair e e' pair the values of e and e'
| fst e projects the first component of the pair e
| snd e projects the second component of the pair e
| inl e injects the value of e into the left half of a sum type
| inr e injects the value of e into the right half of a sum type
| case e e' e'' discriminates on the tag (inl or inr) of the value of e
applying the function e' or e'' to the untagged value.
| nil the empty list
| cons e e' conses the value of e onto the value of the list e'
| listcase e e' e'' tests if e evaluates to the empty list, evaluates e' if it does,
otherwise applies the value of the function e'' to the head
and tail of e's value.
| (e) parenthesised expression (USE ORDINARY PARENTHESES).
Enjoy!
Claudio Russo
~~