Up: New Features in LEGO Version 1.3
Previous: Relaxed Patterns and Inductive Types
LEGO Version 1.3's Computation and Rewrite Rules
Object level computation in the new version of LEGO behaves
differently than in older versions. To explain the new version, let's
consider the design goals of LEGO evaluation.
LEGO is a normal order programming language. There are two reasons
for this: to preserve "feasibility" and to be as "intensional" as
possible. Both of these points need explanation.
Keeping these design goals in mind, we now consider
- "feasibility" - It is usually said that languages like Haskell use
normal order evaluation to preserve termination, but LEGO's type
theories are strongly normalizing (as long as you don't add funny
rewrite rules), so why don't we use applicative order in LEGO? The
fact that LEGO's languages are strongly normalizing is irrelevant in
choosing an evaluation order, because one can surely write terms in
LEGO that will not terminate in practice. LEGO uses a normalizing
order so that terms that can be feasibly (weak head) normalized will
have (weak head) normal forms in LEGO.
- "intensionality" - Using Haskell you don't see arbitrary terms,
only values, i.e. built-in data (e.g. booleans) or data type
constructors (e.g. Cons and Nil). Using LEGO you do see terms, and
you may well care about actual terms, not just their values. For this
reason, LEGO does not update shared parts of terms during computation.
For example when LEGO computes the whnf of (\x.xx)((\y.y)z) it stops
at z((\y.y)z) instead of z(z) as would be the result of using the
sharing introduced by \x.xx, as Haskell does. This may be a bad
decision, but no version of LEGO, including the new one, has this kind
Last modified: Tue Jun 23 16:48:14 BST 1998