The reducer normalizes terms by successive rewriting -- finding a redex and reducing it -- until it either gets stuck or produces a value. The reducer is instrumented to count the number of reduction steps. The reducer is written to be as close as possible to the familiar big-step or structural operational semantics of the calculus. Therefore, its count of reduction steps can be trusted to represent the complexity of term reduction.
The tagless-final style is designed around a compositional mapping of
terms of the embedded DSL to the values in some repr domain -- i.e.,
denotational semantics. Operational semantics in the tagless-final
style did not seem possible all. After all, to find a redex we have to
pattern-match on a term. Performing an application, i.e.,
substituting into abstraction's body, calls for more pattern-matching.
Tagless-final terms are not represented by a data type (AST); how do
we pattern-match on them? This article demonstrates, explaining
how to search for
a redex and substitute in the tagless-final style. Operational semantics
turns out not only possible but also relatively straightforward and
even profitable (e.g., letting us short-circuit the substitution when
the variable in question does not appear in the term).
module type Lambda = sig
type repr
val vz : repr (* variable of the De Bruijn index 0 *)
val vs : repr -> repr (* next De Bruijn index (weakening) *)
val lam : repr -> repr (* abstraction *)
val (/) : repr -> repr -> repr (* application *)
(* Constants *)
val int : int -> repr (* integer literal *)
val inc : repr -> repr (* successor *)
val ifz : repr * repr * repr -> repr (* branch on zero *)
end
The calculus is an instance of a lambda calculus over an algebraic
signature, which in our case contains zero-arity function symbol
(constant) for each natural number; the arity one constant for the
successor inc, and the arity three constant ifz. Incidentally, the
full Lambda signature is also algebraic.
The signature Lambda can be read as the context-free grammar of the language:
repr is the start symbol and lam, inc, etc. are the
terminals. In the conventional CFG notation it would look as:
repr -> "vz"
repr -> "vs" repr
repr -> "lam" repr
...
This grammar derives, for example, lam vz -- the identity combinator.
OCaml programmers might look at Lambda as defining a set of OCaml
functions to construct terms of the embedded calculus. All such terms
are represented as OCaml values of the abstract type repr. Thus vz
is the term for the 0-index free variable,
and lam is the OCaml function that constructs the lambda-abstraction
term given the term for the abstraction's body. Thus lam vz
is the OCaml expression that evaluates to the value of the type repr that
represents the identity combinator.
Since we use OCaml expressions to construct lambda-calculus terms, we
follow OCaml syntactic conventions regarding fixity, parentheses,
application operation associativity and precedence,
etc. For example, lam (lam (vs vz)) represents
the K combinator. We can write this expression without
parentheses, using @@ -- the right-associative OCaml application operator of
low precedence -- as lam @@ lam @@ vs vz. The second Church numeral
looks as lam @@ lam @@ vs vz / (vs vz / vz) (in OCaml, slash is
the infix operator, of a higher precedence compared to @@).
To specify the meaning of the vz, lam, etc. operations, is to
implement the Lambda signature. An implementation, such as
NativeEval below, tells what repr is, concretely --
and how exactly vz, lam etc. operations construct the
repr values that represent the free-variable, the abstraction,
etc. terms. In other words, an implementation of Lambda tells how
to compute the meaning, or, the repr value, of each term from the
repr values of its immediate subterms. An
implementation of Lambda thus specifies a denotational semantics
of the calculus.
Specifically, NativeEval maps closed lambda-terms either to
OCaml integers or OCaml
functions. The calculus is untyped; the semantics domain is
therefore the
disjoint union v below. We also have to account for open terms, and
hence introduce the environment: a list of v values that are assumed
as meanings for free variables. The list is ordered by the De Bruijn
index. Thus the term meaning repr is a partial
function from the environment to v (if the environment does not tell
the meaning of all free variables in a term, we cannot make any sense
of the term):
module NativeEval = struct
[@@@warning "-8"] (* annotation: partial pattern-match is intentional, don't warn *)
type v = (* the value domain *)
| I of int
| A of (v->v) (* generally, a partial function *)
type repr = v list -> v (* also a partial function *)
let vz = fun (h::_) -> h
let vs e = fun (_::t) -> e t
let lam e = fun env -> A (fun x -> e (x::env))
let (/) e1 e2 = fun env ->
match e1 env with A f -> f (e2 env)
let int x = fun _ -> I x
let inc e = fun env -> match e env with I x -> I (x+1) (* partial *)
let ifz (e1,e2,e3) = fun env -> match e1 env with (* partial *)
| I 0 -> (e2 / (int 0)) env
| I n when n > 0 -> (e3 / (int (n-1))) env
end
It should now be clear what ifz(n,v1,v2) means exactly: n is
supposed to be an integer; v1 and v2 are functions.
If n means 0, ifz(n,v1,v2) amounts to the application
of v1 to 0; otherwise,
ifz(n,v1,v2) means the same as the application of v2 to the predecessor of
n. In other words, ifz is the pattern-matcher (deconstructor) on
integers.
NativeEval is but one implementation of Lambda. Another
implementation, called Show, maps each term to a string, the
pretty-printed representation of the term. The reader may want
to write this implementation on their own (and then compare to the one
in the accompanying code).
lam vz, in the NativeEval interpretation means
the identity function on NativeEval.v. According to the Show
implementation, however, the same term means the string
"Lx1. x1". One may ask: what does the term lam vz mean by itself?
A glib answer is that a term embedded in the tagless-final style means
whatever its interpretation makes it to mean. Technically, an embedded
term may be regarded as a function that takes an
interpretation of its syntactic forms (i.e.,
an implementation of its signature) and
returns the repr value produced by that implementation. To say it in
OCaml:
type lambda = {e: 'a. (module Lambda with type repr = 'a) -> 'a}
Different implementations of Lambda generally choose different
concrete types for repr -- therefore the type lambda stands for a
polymorphic function: there is a implicit forall before 'a.,
quantifying that type variable. Moreover, lambda is the first-class
polymorphic function: we do want to pass terms as arguments to other
functions. In OCaml, first-class polymorphic values have to be
embedded in a record (in our case, the record with the field e).
Since we chose modules for tagless-final signatures and
implementations, lambda's argument is a value of the
module type: OCaml has first-class modules. We could just as well
have used OCaml records or objects -- and we
will use something like that in the follow-up article.
The modules are more convenient and we use them for now.
Although lambda is the glib technical answer to the question about
the inherent meaning of embedded terms, it could be taken
seriously. In fact, we may define a denotational semantics in which
our lambda-calculus terms indeed mean lambda.
It is the most banal -- one may say, `syntactic' -- implementation
of Lambda. We
show only the representative part; the reader may want to finish as
an exercise.
module LambdaSelf : (Lambda with type repr = lambda) = struct
type repr = lambda
let vz = {e = fun (type a) (module L : Lambda with type repr = a) ->
L.vz}
let vs e = {e = fun (type a) ((module L : Lambda with type repr = a) as l)->
L.vs (e.e l)}
let lam e = {e = fun (type a) ((module L : Lambda with type repr = a) as l)->
L.lam (e.e l)}
...
end
One can now say what lam vz means `by itself': it tells how to
interpret itself, using whatever interpreter the user may provide.
That is, lam vz takes an interpreter as an argument and directs it to
find the meanings of vz and use the interpretation of lam
to build the complete denotation. The `intrinsic' meaning of an embedded
term is, hence, the guiding of its interpretation according to its
structure. This is what syntax means, doesn't it?
(The reason the above implementation is called LambdaSelf will
become clear in the follow-up article).
One may say above more `mathematically': we have already mentioned
that Lambda is an algebraic signature. Its implementations --
NativeEval, Show, LambdaSelf and many more below -- are
hence Lambda-algebras. Each algebra has its own set of repr values (the
carrier set), which supports vz, vs, etc. operations.
Of all Lambda-algebras, LambdaSelf is special: it is so-called
`word' algebra, which is an initial algebra. For any
Lambda-algebra L, there is a unique total function
Lambda.repr -> L.repr that `respects' the operations: the unique
homomorphism. In fact, any
implementation of a Lambda-signature is exactly the definition of
that homomorphism. For example, passing the NativeEval interpreter, as the
first-class--module argument, to a
LambdaSelf term obtains the NativeEval's interpretation of the
term, as we shall see momentarily.
Banal as it may be, LambdaSelf is insightful, and also practically
useful. First of all, it lets us easily write terms and have them
interpreted. Here a few sample terms:
open LambdaSelf
let ci = lam vz
let ck = lam @@ lam @@ vs vz (* the K combinator *)
let c2 = lam @@ lam @@ vs vz / (vs vz / vz) (* second Church numeral *)
let et3 = lam @@ inc(inc(vz / int 1)) (* higher-order, numeric *)
let et3a = et3 / (lam @@ inc(inc(inc vz)))
let delta : lambda = lam @@ vz / vz
let lomega : lambda = lam @@ delta / delta
They all have the type lambda, which is inferred in all cases
(although we often prefer to write the type explicitly as an
annotation, to make sure we define a proper embedded term). We use
OCaml definitions to give names to embedded terms; moreover, we can use
the names to incorporate already defined terms into new ones (see
et3a and lomega).
A bit more complex is the the applicative fixpoint combinator,
let fixa : lambda =
lam (vz /
(lam @@ delta / (lam @@ vs (vs vz) / (lam (delta / vs vz / vz))) / vz))
using which we define the recursive function to add two numbers, by
induction on the second summand:
let add : lambda =
lam @@ fixa / (lam @@ lam @@
let y = vz and self = vs vz and x = vs (vs vz) in
ifz(y, lam @@ vs x, lam @@ inc(vs self / vz)))
We take another advantage of OCaml let-bindings, to give meaningful
names to De Bruijn indices.
The lambda terms are also straightforward to evaluate, as we have
said earlier:
let eval : lambda -> NativeEval.v = fun {e} -> e (module NativeEval) []
The evaluator takes a (closed) lambda term, passes it the NativeEval
implementation as the first-class module, and applies the resulting
repr value to the empty environment. Thus we may try
eval Sample.et3a
(* NativeEval.I 6 : NativeEval.v *)
eval LambdaSelf.(add / int 1 / int 4)
(* NativeEval.I 5 : NativeEval.v *)
(The evaluation result is shown in the comments). Likewise, we
define show : lambda -> string, so
that show c2 gives "Lx1. Lx2. x1 (x1 x2)". When printing terms, we
use concrete variable names for readability.Tagless-final with objects
A simpler example of the tagless-final DSL embedding, using objects
(which are extensible records)
Lambda term
into the corresponding weak normal form -- or diverge
if it does not exist. The weak normal form -- also called value -- is a
closed term of the particular shape: either int x for some integer
x or lam e for some e.
The normalizers differ from the earlier eval : lambda -> NativeEval.v
and show : lambda -> string in that they map a lambda-term to
another lambda-term. Thus the two normalizers to be described below
both have the type lambda -> lambda. The identity function also has
this type; the normalizers, however, always return a lambda-term that is a
value.
Our first normalizer is `denotational' and hence easily coded in the
tagless-final style. In fact, we have already written most of its
code: NativeEval, which maps a lambda term to its
NativeEval.v meaning. If only we could
turn this meaning to a value lambda-term... Let's try:
let rec dyn : NativeEval.v -> lambda = function
| NativeEval.I x -> LambdaSelf.int x
| NativeEval.A f -> LambdaSelf.lam (dyn (f ???))
Since f above is a v -> v function, we have to apply it to
something, in such a way that the result is easily convertible to
lambda representing the body of the abstraction.
The easy solution is to extend the NativeEval.v data type
with another variant, for the term being reconstructed:
type v =
| I of int
| A of (v->v)
| T of lambda
Then
let rec dyn : v -> lambda = function
| I x -> LambdaSelf.int x
| T e -> e
| A f -> LambdaSelf.lam (dyn (f (T LambdaSelf.vz)))
hoping that the function f, upon receiving T LambdaSelf.vz,
will produce T e where e is the term that corresponds to the
abstraction's body. For example, lam vz naturally means the (tagged) OCaml
identity function: A (fun x -> x); applying dyn gives us
LambdaSelf.lam LambdaSelf.vz : lambda as desired.
We now have to adjust NativeEval to produce the hoped-for denotations.
There is a slight problem however: we naturally wish int 1 to be
interpreted as I 1 -- but not when it appears under lam, as in
lam (int 1). In the latter case, it ought to be interpreted as
LambdaSelf.int 1. Luckily, we already have the solution to this
context-sensitivity problem. To account for open terms,
the meaning repr in NativeEval is a function from the
environment to v. The environment is a list of v values to use when
substituting for free variables. Normally, these values are tagged either
with I or A. However, the dyn function above will also pass T LambdaSelf.vz to request the result as a T-tagged
lambda term (the `read-out'). We can, hence, easily tell if the
current context
is under lambda: the environment contains
at least one T-tagged value at the top. (A little exercise: can we
say that the environment is either a list of I and A values, or
entirely T-tagged values?)
module NBE = struct
[@@@warning "-8"] (* partial pattern-match is intentional *)
type v = (* the value domain *)
| I of int
| A of (v->v)
| T of lambda
type repr = v list -> v
let rec dyn : v -> lambda = function
| I x -> LambdaSelf.int x
| T e -> e
| A f -> LambdaSelf.(lam (dyn (f (T vz))))
let vz = fun (h::_) -> h (* Substitution under lam is OK *)
let vs e = fun (_::t) ->
match e t with
| T e -> T LambdaSelf.(vs e)
| e -> e
let lam e = function
| T _::_ as env -> (* readout in progress *)
T LambdaSelf.(lam (dyn (e (T vz::env))))
| env -> A (fun x -> e (x::env))
let (/) e1 e2 = function
| T _::_ as env -> T LambdaSelf.(dyn (e1 env) / dyn (e2 env))
| env -> match e1 env with A f -> f (e2 env)
let int x = function
| T _::_ -> T (LambdaSelf.int x) (* readout in progress *)
| _ -> I x
let inc e = function
| T _::_ as env -> T LambdaSelf.(inc (dyn @@ e env))
| env -> match e env with
| I x -> I (x+1)
| T e -> T LambdaSelf.(inc e)
let ifz = (* exercise *)
end
Most denotations have two cases: one for read-out (for building terms)
and the other as in NativeEval. Only vz has the single
interpretation: the substitution is performed uniformly in any context.
The denotational normalizer is thus:
let neval : lambda -> (NBE.v list -> NBE.v) = fun {e} -> e (module NBE)
let nbe : lambda -> lambda = fun e -> NBE.dyn @@ neval e []
let nbeshow : lambda -> string = fun e -> show @@ nbe e
(incidentally, neval is that unique homomorphism from LambdaSelf
to NBE -- do you see that?)
For example, nbeshow lomega produces the same string as
show lomega: lambda-abstractions always evaluate to themselves, even
if there are redices inside. Not surprisingly,
nbeshow (add / int 1 / int 4) yields "5", which is the
pretty-printed representation of int 5. Now, however, we can also
nbeshow (add / int 1). For sure, we could
eval (add / int 1) with NativeEval. The result, however, is
a (A-tagged) OCaml function, which is opaque. The new nbeshow lets us
see the resulting lambda-term:
"Lx1. ifz x1 (Lx2. 1) (Lx2. S ((Lx3. (Lx4. x4 x4) (Lx4. (Lx5. Lx6. ifz x6 (Lx7. 1) (Lx7. S (x5 x7))) (Lx5. (Lx6. x6 x6) x4 x5)) x3) x2))"Still, the result of
nbe (add / int 1) agrees with that of the
NativeEval, the definitional interpreter. To quickly check:
let e = LambdaSelf.(add / int 1) in
let A f1 = eval e in
let A f2 = eval (nbe e) in
List.for_all (fun n -> f1 (NativeEval.I n) = f2 (NativeEval.I n))
[0;1;2;3;4;100]
produces true: f1 and f2 agree, at least on the given sample inputs.
One may easily observe from the NBE code that, when restricted to v
values without T-tags, it behaves just like NativeEval.
In particular, for any closed term e, neval e [], if terminates, is
either I x for some integer x or A f for
some v->v function.
One may further observe, with a slightly bit more effort, that if
v is the result of neval e [] for some closed term e, then
neval (dyn v) [] is v, extensionally. (The extra effort is
generalizing this statement to open terms). That is, dyn is the
left-inverse for the NBE interpretation. The function like dyn is typically
called `reify' in the normalization-by-evaluation literature. Putting
these observations together we obtain that for any closed term e,
nbe e is a value term and
eval e === eval (nbe e)where
=== means that either two sides both diverge, or they are the
same integer or the same, as a mapping, OCaml function (that is, ===
is the extensional equality). That means nbe is
meaning-preserving and it does yield a value: it is the correct
normalizer.
Incidentally, normalization-by-evaluation is a technique for
normalizing terms, or partially evaluating them. A partial evaluator
can perform reductions even under lambda. Although this often improves
efficiency when the lambda-term is subsequently applied, in this
article we keep close to the operational semantics and avoid any extra
reductions. (It is also worth contemplating what may happen when partially
evaluating a term like lomega.)
------- (where v is a value: either lam e or int x)
v --> v
------------------------ (beta)
(lam e) / v --> e{vz:=v}
------------------------- (inc)
inc (int x) --> int (x+1)
-------------------------------- (if0) (v1,v2 are values)
ifz(int 0,v1,v2) --> v1 / int 0
------------------------------------- (ifn) (n>0)
ifz(int n,v1,v2) --> v2 / (int (n-1))
e1 --> e1'
-------------------- (e1 is not a value)
e1 / e2 --> e1' / e2
e2 --> e2'
------------------ (e2 is not a value)
v / e2 --> v / e2'
e1 --> e1'
------------------------- (e1 is not a value)
inc e1 --> inc e1'
e --> e'
------------------------------ (e is not a value)
ifz(e,e1,e2) --> ifz(e',e1,e2)
(the two more similar ifz compatibility rules are skipped)
where e{vz:=v} stands for the substitution of the value v for the
free variable vz in e, adjusting the other De Bruijn indices.
The rules are all disjoint; the last six
(including the two skipped ones)
are the compatibility rules, implicitly defining the evaluation
contexts. The reducer sos below applies the rules until it
either obtains a value, or no rule is applicable: it got stuck.
That is, sos computes the transitive closure of -->.
The operational semantics treats inc e and ifz(e,e1,e2) terms
essentially like
applications: in either case, if the arguments are not values,
compatibility rules are applied. If the arguments are values,
the reduction looks at what sort of value it is, and does something
meaningful (performs substitution or the increment). Our reducer below
indeed treats the terms with inc and ifz as applications.
Incidentally, the operational semantics may also be specified in the
big-step, `natural' style, as the ==> relation of a term and the
corresponding value:
-------
v ==> v
e1 ==> lam e1' e2 ==> v2 e1'{vz:=v2} ==> v
-----------------------------------------------
e1 / e2 ==> v
(the rules for inc and ifz are left as an exercise).
repr below. The kind tells if the term
is an application (and if so, its applicands) or a
value. In the latter case, is it an integer value or a functional
value, that is, something that takes an argument and either
substitutes it or does something fancier. Since repr
denotations are built bottom-up, one has to account for another
possibility: if a term is open. The classification of an open term
depends on what its free variables mean. An open term
is a term with free variables to substitute. We also
keep track of the depth of an open term, the largest De Bruijn index
of its free variables (which is the length of the needed environment).
module Classifier = struct
[@@@warning "-8"] (* partial pattern-match is intentional *)
type repr = {term: lambda; (* term as it is *)
kind: kind} (* and its kind *)
and kind =
| App of repr * repr (* subject to reductions *)
(* Expressions of the kind Int and Applicable are values *)
| Int of int
| Applicable of (repr -> repr) (* can be applied to an argument,
which must be a value
*)
(* The three kinds above are closed. The remaining kind is
for open expressions. The first argument is the depth:
the number of lambdas needed to close the expression
*)
| Open of int * (repr list -> repr)
let vz = {term = LambdaSelf.vz;
kind = Open (1,fun (h::_) -> h)}
let rec vs e = match e.kind with
| Open (n,e') ->
{term = LambdaSelf.vs e.term;
kind = Open (n+1,fun (_::t) -> vs (e' t))}
(* vs may end up being applied to a closed value after the substitution.
In that case, it does nothing.
*)
| _ -> e
let rec lam e =
{term = LambdaSelf.lam e.term;
kind = match e.kind with
| Open (1,t) -> Applicable (fun x -> t [x])
| Open (n,t) when n > 1 ->
Open (n-1,fun env -> lam (t (vz::env)))
| _ -> Applicable (fun _ -> e) (* constant function *)
}
let rec (/) e1 e2 = (* exercise *)
let int x = {term = LambdaSelf.int x;
kind = Int x}
(* introducing delta-redices *)
let delta_inc =
{term = LambdaSelf.(lam @@ inc vz);
kind = Applicable (function {kind = Int n} -> int (n+1))}
let rec inc e =
{term = LambdaSelf.(inc e.term);
kind = match e.kind with
| Open(n,t) -> Open(n,fun env -> inc (t env))
| _ -> App (delta_inc,e)
}
let ifz = (* exercise *)
end
One may notice that as we build repr bottom-up, we also build the
function to substitute for the term's free variables.
The substitution function is a bit smart: it avoids rebuilding or even
looking into subterms that are known to be closed and hence have nothing
to substitute for.
It is worth pointing out how kind differs from the familiar
abstract syntax tree for the lambda-calculus. First, we do not
distinguish inc and ifz: either is treated as applications.
However, we do distinguish open terms.
inc e and ifz(e,e1,e2) terms are treated
as applications.
let sos : lambda -> lambda = fun {e} ->
let open Classifier in
let rec step : repr -> repr = (* the --> reduction of SOS *)
fun e -> match e.kind with
| Applicable _ | Int _ -> e (* value *)
| Open _ -> assert false (* cannot happen *)
| App (e1,e2) -> match (e1.kind,e2.kind) with
| (Applicable f,Int _) | (Applicable f,Applicable _) ->
f e2 (* redex *)
| (App _,_) -> step e1 / e2 (* compatibility rules *)
| (_,App _) -> e1 / step e2
| _ -> failwith "stuck"
in
let rec loop : repr -> repr = (* transitive closure of step *)
fun e -> match e.kind with
| Applicable _ | Int _ -> e (* value *)
| _ -> loop (step e) (* keep stepping *)
in (loop (e (module Classifier))).term
let sosshow : lambda -> string = fun e -> show @@ sos e
The sos reducer can be used just like the earlier nbe
normalizer. They do produce identical results (see the accompanying
code for that test, among many others).
The naively implemented SOS reducer is inefficient: too many pattern-matches on the shape of the term. (Do you see that?) A simple modification turns it into the efficient, natural, big-step reducer -- which we suggest as an exercise. The accompanying code also makes the big-step reducer count the number of reductions.
The normalizers are written in the host language, OCaml. Next we lower normalizers to (into) the embedded language itself, showing off our calculus serving as a metalanguage to embed itself and evaluate the self-embedded expressions.