Syntax sugar

The core language defined in the body of the paper is quite sparse, but can be made quite readable with the addition of some simple syntax sugar, for terms such as infix functions and curried functions. This sugar has been used in all of the examples in the paper, and is implemented in the Java applet.

The syntax has been designed to resemble a C- or Pascal-like language, and is parsable (once some ambiguities are resolved) by an LL(1) grammar. The Java applet uses a JavaCC grammar, and is available electronically.

Infix constructors and functions:

M c N = c (M, N)
M x N = x (M, N)

Sequential composition of expressions (where T is the type of M and x is fresh):

(M; N) = (let x:T = M; N)

If the second expression is missing, it defaults to the empty tuple:

(M;) = (M; ())

For fans of C syntax, a return expression:

return M; = M

Syntax sugar for curried function types:

(C T0 ... Tn : T) = val T0 : (C T1 ... Tn : T)

for example the type of a fibonnaci function might be:

proc int int int : list = val int : val int : proc int : list

Note that all but the last function type is a val function, thus we have recorded in the type system the fact that applying the function to up to two arguments involves no significant computation, but applying it to a third argument begins a computation.

Syntax sugar for multiple curried arguments in anonymous functions, which matches the curried type:

(fn C P0 ... Pn {M}) = (fn val P0 { fn C P1 ... Pn {M} })

Again, note that it is only the last function which requires any computation.

Pascal-style declaration of named functions (where each Pi has type Ti):

C x P0...Pn : T {M} = let x : (C T0...Tn : T) = fn C P0...Pn {M};

for example:

local rec fibR;
proc fibR (x : int) (y : int) (n : int) : list {
  if (n == 0) { return nil; } { return x :: fib (y) (x + y) (n - 1); }
}
proc fib (n : int) : list {
  return fibR (0) (1) (n);
}

The return value of a function is optional, with default ():

fn C P1...Pn { } = fn C P1...Pn { () }

and similarly for named functions:

fn C x P1...Pn { } = fn C x P1...Pn { () }

Pascal-style type notation for functions in patterns and contexts:

C x T1 Tn : T' = x : C T1 Tn : T'

for example:

rec map;
proc map (proc f (int) : int) (xs : list) : list {
  if (isNil (xs)) { nil } { f (hd (xs)) :: map (f) (tl (xs)) }
}

Recursive function declarations (where x has type T in D and y is fresh):

rec x; D = local rec y; let x:T = y; D let y:T = x;

Multiple variables in recursive declarations:

rec x0,..., xn; D = rec x0; rec x1,..., xn; D

and in local recursive declarations:

local rec x0,..., xn; D = local rec x0; local rec x1,..., xn; D

Some handy syntax sugar for thunks:

{M} = fn proc () {M}
{ } = fn proc () { }

For example if we have an appropriately typed if function:

proc if (bool) (proc ()) (proc ())

then we can write if-statements as:

if (conditional) {true-case} {false-case}

For example, a while function can be written:

rec while; proc while (proc b () : bool) (proc p ()) {
  x : bool = b ();
  if (x) { } { p (); while (b) (p) }
}

For example:

while { !(x) > 0 } { x := (!(x) - 1); f (x) }

Previous | Next