Controlled reduction
Making sense of IvoryScript values introduced
expressions as distinct values. It also used the prefix
#! without explaining its significance.
#! is the reduction
operator.
Reduction is the transformation of a value into a simpler form, which does not imply any particular computation or process for carrying out that transformation. Its meaning is given by a relatively small collection of transformation rules for each expression form, using two fundamental abstract functions: Valof & Reduce.
ValOf
ValOf e ρ - the value of an expression
e in a given environment ρ.
The term environment is used elsewhere in IvoryScript documentation for a broader mechanism spanning names, types, closures and pointers. Here it refers to the static binding of names to values within the scope of an expression.
Importantly, ValOf does not imply reduction. The
value denoted by e may be irreducible, such as an
integer or character, or it may itself be an expression
value.
Four rules cover every case.
Reduction
ValOf #!e ρ
=> Reduce (ValOf e ρ) ρ
The value of #!e involves reduction, discussed
fully in the sections that follow.
Name occurrence
ValOf x ρ
=> LookUp x ρ
LookUp x ρ is the value associated with
x in the environment ρ. If that value
is an expression, it remains an expression. ValOf
does not implicitly reduce it.
The same name may occur in different environments and denote different values. Environments are considered more fully later.
Literal
ValOf #k ρ
=> k
per Making Sense of Values, a literal constant value.
Identity
ValOf e ρ
=> e
For any e not covered by the three rules above,
ValOf e provides e
directly. All free variables (name occurrence values within, but
not defined in it) are captured; this will be described
separately.
Reduce
There is a separate rule for each expression form.
Constant as expression
A constant expression reduces to its corresponding value:
Reduce Exp k ρ => k
Thus for:
#!42
the integer value forty-two.
Lambda as expression
A lambda is itself an expression value. Its direct reduction gives the corresponding lambda value:
Reduce Exp λ v1 ... vn -> e ρ => λ v1 ... vn -> e
For example, a doubling function:
\i -> #!(addInt i i)
is an unreduced function value.
#!(\i -> #!(addInt i i))
makes it available for function application.
Function application
A function may be applied to one or more arguments:
f a1 ... an
Nested applications are combined:
Reduce (Reduce (f a)) b ρ
=> Reduce f a b ρ
Reduce (Reduce (f a b)) c ρ
=> Reduce f a b c ρ
...
The general application rule is:
Reduce (f a1 ... an) ρ
=> Reduce (ValOf f ρ) a1 ... an ρ
These rules also account directly for currying. Arguments may be supplied by nested applications rather than all at once.
For example, addInt 3 4 is parsed as
(addInt 3) 4. Collapsing gives the flat form:
Reduce (Reduce (addInt 3)) 4 ρ => Reduce addInt 3 4 ρ
and the general application rule then applies:
Reduce (addInt 3 4) ρ => Reduce (ValOf addInt ρ) 3 4 ρ
Lambda application
When the function value is a lambda, fully applied:
Reduce ((λ v1 ... vn e) a1 ... an) ρ
=> ValOf e ρ[vn = ValOf an; ...; v1 = ValOf a1]
Each parameter is bound to the value of its corresponding
argument in sequence in reverse order. The body e
in this extended environment is the value of this reduction.
If e denotes a function value (referred to as
higher-order), additional arguments for it may also be present.
From the perspective of the function application this is
transparent.
The number of arguments may also be less than required,
otherwise known as partial application. For
1 ≤ k < n (n ≥ 2):
Reduce ((λ v1 ... vn e) a1 ... ak) ρ
=> λ v(k+1) ... vn -> ValOf e ρ[vk = ValOf ak; ...; v1 = ValOf a1]
The arguments are bound, in the same reverse order as full application, and the result is a new lambda over the remaining parameters. Applying that lambda to the rest of the arguments has the same value as applying the original lambda to all of them directly.
For example:
(\i j -> #!(addInt i j)) 3
is the k = 1, n = 2 case:
Reduce ((\i j -> #!(addInt i j)) 3) ρ
=> \j -> ValOf #!(addInt i j) ρ[i = ValOf 3]
The result is a single argument function closure over
i = 3. Applying it to 4 has the same
value as (\i j -> #!(addInt i j)) 3 4.
Currying means that there is nothing to distinguish a two-parameter function from a single parameter one returning a further function; that distinction is examined in Data types: Strict and lazy. The rule above is stated as if the number of a lambda's formal parameters (referred to as its arity) was simply known regardless; ensuring a caller sees identical behaviour - whichever the callee actually turns out to be - is a matter for description elsewhere.
let
A let expression introduces a local binding:
Reduce (let x = e in eb) ρ => ValOf eb ρ[x = ValOf e]
The body eb is its value in an environment
extended by a binding of x to the value of
e for all occurrences of x within
eb.
For example:
let x = 42 in x
binds x to the expression value 42.
Neither the binding or any name occurrence implies
reduction.
For an ordinary let, the right-hand side
e is in the scope of ρ and
eb in the scope of the extended environment
ρ'.
let can introduce several bindings at once,
sequentially bound in order (unlike the reverse order of
function application arguments):
Reduce (let x1 = e1; ...; xn = en in eb) ρ
=> ValOf eb ρ[x1 = ValOf e1 ρ; ...; xn = ValOf en ρ]
Recursive bindings permit the scope of the bound expression
to be ρ'
ρ' = ρ[x1 = ValOf e1 ρ'; ...; xn = ValOf en ρ']
This allows for mutual recursion, where name occurrences in a
bound expression may refer to other names within the same
let (sometimes referred to as
letrec).
Fatbar
Fatbar provides choice:
Reduce e1 [] e2 ρ
=> Valof e1 ρ
or
=> Valof e2 ρ
(if Valof e1 ρ = FAIL)
The first alternative with any value other than
FAIL; otherwise the second alternative.
For example:
case pair of {
(0, y) -> a
otherwise -> b
}
compiles (in outline) to a single let. The
scrutinee value pair is bound once to
p, then the first component is unpacked and
compared. If equal to 0, y is bound to
the second component, resulting in a in the
extended environment. Otherwise [] falls back to
b:
let
p = pair
in
#!(COND #!(eqInt (x = #!(SELECT (Pair, 1) p)) 0)
#!(let y #!(SELECT (Pair, 2) p)) 0) in a
FAIL) [] b
This is the end point of a series of transformations. For
example, with an intermediate stage
let p = pair in #!(#!(\(0, y) -> a) p) [] b.
How an arbitrary set of patterns compiles to nested Fatbar and lambda applications — including the order in which components are unpacked and the guarantee that a component is reduced only once - is a matter for the general case transformation (described separately). Worth noting here only that pattern matching may result in explicit reduction just to preserve overall surface language case semantics.
Primitive and built-in functions
Most primitive and built-in functions need no specific rule,
e.g. addInt, reached via LookUp (see
Name occurrence), denotes an ordinary lambda value; applying it
goes through the same Lambda application rule as any other
function. A compiler may implement a fully applied application
as a single instruction, but this is simply an optimisation
detail, not of any semantic relevance.
COND, which denotes a conditional value, is
different in kind. Ordinary lambda application binds every
parameter uniformly through ValOf, but no rule
reduces one argument while leaving another untouched. For this
reason, there is a separate rule for an application of
COND.
Reduce (COND q a b) ρ => Valof q ρ
True => ValOf a ρ
False => ValOf b ρ
The value of q determines a value a
or b - note that no value is produced (using
Valof) unless selected.
The same reasoning applies to sequencing: a dedicated rule is required only where the effect cannot be reproduced by function application in the ordinary way.
Sequencing
A source language block { e1; e2 } is
transformed to SEQ e1 e2
Reduce (SEQ e1 e2) ρ => ValOf e1 ρ; ValOf e2 ρ
Note that ValOf e1 ρ has no value, but it will
require reduction to reach that point before the value of
e2 is determined.
Controlled
The distinction between ValOf and
Reduce is central. ValOf establishes
the value denoted by a form, and that value may itself be an
expression. It does not continue implicitly towards some more
fundamental value.
An expression may therefore remain an expression indefinitely. It may be:
associated with a name
passed as a function argument
returned as function result
copied
persisted
all without being reduced.
Reduction occurs only where it is explicitly denoted, and only according to the applicable transformation rule.