Every so often I like to reread notable books on /Programming Language Theory/ (PLT). Namely, one should read:
- Programming Language Foundations in Agda
- Software Foundations
- Types and Programming Languages
- Practical Foundations for Programming Languages
With these books each presents a treatment of PLT either: mechanised using Agda or Coq; presented purely theoretically in LaTeX; or a mixture of theory and practice.
Of particular interest to myself is the presentation using Agda. Dependent types allow us to present formal descriptions of our programs together with their practical constructions.
I found the treatment in PLFA guilty of missing that last step: How to run one’s programming and obtain an result. This is no fault of the book’s authors. They seek to provide a foundational course towards PLT and they do that fine, unicode and mixfix operators aside. In fact, Agda programmers can run their programs but what would be more beneficial when presentating a programming language’s semantics would be the last step and linking this to its practicalities: producing values.
In this post I will show this by considering Hutton’s Razor in the dependently-typed language Idris
Statics
We can define the static semantics of Hutton’s Razor as:
data Term = Val Nat | Add Term Term
Terms are either values (natural numbers) or the addition of two terms.
This razor is mono-typed in that all terms have type Nat, so we need not be explicit with a term’s type:
They are all typed with the same type
Dynamics
Using these static semantics we can begin to provide straightforward progress and preservation proofs. If fact we will only look at progress as, given our mono-typed terms typing is preserved. To look at progress we must first define what it means for our terms to reduce.
Values
Values are our only values:
data Value : Term -> Type where
IsValue : {n : Nat} -> Value (Val n)
Reduction
We define reduction on terms using a simple small-step operational semantics. This can be encoded nicely in Idris using a dependent type as follows:
data Reduce : (this : Term) -> (that : Term) -> Type where
with reduction rules that are focused on the addition term.
Left Operands Reduce
Let us start our reduction by stating that left operands can reduce to something.
LeftEta : Reduce this that
-> Reduce (Add this y) (Add that y)
Right Operands Reduce
Once, the left operand is a value and we have proof that the right operand, then the addition will reduce the right operand.
RightEta : Value x
-> Reduce this that
-> Reduce (Add x this) (Add x that)
Addition Reduces
If both operands in our term are values then the term can be reduce to a single value.
AddBeta : Reduce (Add (Val x) (Val y)) (Val (plus x y))
Progress
With our reduction semantics we can then now look to define progress.
Definition
Rather straightforwardly, progress is when given a term t:
data Progress : (t : Term) -> Type where
we are done when t is a value:
Done : Value v -> Progress v
or we can step through the computation reducing t to another term n:
Step : {n : Term} -> Reduce t n -> Progress t
Proof
using our reduction rules we can describe this progress as given a term t:
progress : (t : Term) -> Progress t
Values
We are done when we have a value:
progress (Val k) = Done IsValue
Addition
Given the addition term we examine the left operand first:
progress (Add x y) with (progress x)
and then the right operand second:
progress (Add x y) | (Done z) with (progress y)
If both operands are values we can apply AddBeta to reduce this to a single value.
progress (Add (Val x) (Val y)) | (Done z) | (Done w) = Step AddBeta
If we have reduce the left operand but not the right operand we can only reduce using RightEta.
progress (Add x y) | (Done z) | (Step w) = Step (RightEta w z)
‘Last’ of all if we have just reduced the left operand then we apply LeftEta to move on to the right one.
progress (Add x y) | (Step z) = Step (LeftEta z)
Complete Reduction
We have shown the small step operational semantics with single reductions steps. To link them together we need to show that a term can reduce down until it can no longer reduce.
More formally speaking we can describe such a set of sequences as a term this that will reduce completly to that:
data Reduces : Term -> Term -> Type where
The reduction is reflexive if reduction doesn’t reduce any further:
Refl : Reduces t t
The reduction is transitive in that a term a will reduce completly to term c if when we know that a can take a single step towards term b, and that b will eventually reduce to term c.
Trans : Reduce a b -> Reduces b c -> Reduces a c
Finished Evaluation
Evaluation of a term t will finish under the following circumstances:
data Finished : Term -> Type where
If the term t has reduced to a value we know that the term has been fully normalised—i.e. computed.
Normalized : Value t -> Finished t
Otherwise, we have a term that is stuck and we can make no more progress.
OOF : Finished t
The Last Step(s)
With the definition of our razor and proofs of progress and preservation complete we need to look at evaluating terms.
For Squigglers.
If we were reading PLFA we will say that given a term t:
data Steps : (t : Term) -> Type where
evaluation is a series of steps describing the reduction of t to a term t' in which t' can no longer reduce.
MkSteps : Reduces t t' -> Finished t' -> Steps t
We can caputure the reduction of a term t as a finite set of steps that one must take to either get stuck or, even better, provide a value.
eval : Nat -> (t : Term) -> Steps t
The natural number here is the fuel to allow us to reduce our computation.
eval Z t = MkSteps Refl OOF
If we can no longer take a step we can no longer compute.
eval (S k) t with (progress t)
If not let us compute:
eval (S k) t | (Done x) = MkSteps Refl (Normalized x)
If we are done computing then great we are finished!
eval (S k) t | (Step x) {n} with (eval k n)
If not, and we have stepped through once, let us try again.
eval (S k) t | (Step x) | (MkSteps y z) = MkSteps (Trans x y) z
As we know we can take at least two steps then we are done!
Example:
With eval we can show that we can compute values from terms.
Arith> eval 100 (Add (Val 1) (Val 4))
MkSteps (Trans AddBeta Refl) (Normalized IsValue)
Arith> eval 100 (Add (Val 1) (Add (Val 3) (Val 4)))
MkSteps (Trans (RightEta AddBeta IsValue) (Trans AddBeta Refl)) (Normalized IsValue)
It is not clear, however, what this value is.
For Bodgers.
Let us take a different direction and perform a better last step. Our definition of evaluation is the same as before:
data Steps : Term -> Type where
MkSteps : Inf (Reduces t t') -> Finished t' -> Steps t
We now say, however, that our reduction could contain infinitly many steps and is possible an infinite data structure.
Rather than use Natural numbers as a source of fuel we can take a different representation, that of the fuel data type:
data Fuel = Empty | More (Inf Fuel)
In which we have no fuel, or infinitly more fuel.
This fuel could also potentialy last forever:
forever : Fuel
forever = More forever
Redefining our evaluation in terms of fuel is straightforward, we swap out Nats for fuel.
compute : Fuel -> (t : Term) -> Steps t
compute Empty t = MkSteps Refl OOF
compute (More f) t with (progress t)
compute (More f) t | (Done x) = MkSteps Refl (Normalized x)
compute (More f) t | (Step x) {n} with (compute f n)
compute (More f) t | (Step x) | (MkSteps y z) = MkSteps (Trans x y) z
With computation defined we can now say how to run a computation:
run : (t : Term) -> Maybe (n : Nat ** Reduces t (Val n))
Our definition of run states that a successful computation of t will tell us the value that is reduced and the set of steps required.
Further, even though we know that computation of t is total we nonetheless need to account for the fact that we might run out of fuel.
Thus we wrap the result in a maybe type.
With this we look at running the computation:
run t with (compute forever t)
We know that computations can take forever and will either:
run t | (MkSteps x (Normalized (IsValue {n}))) = Just (n ** x)
produce just a value; or
run t | (MkSteps x OOF) = Nothing
produce nothing.
With run we can now compute values and show how they reduce!
run (Add (Val 1) (Val 4))
Just (MkDPair 5 (Trans AddBeta Refl))
Arith> run (Add (Val 1) (Add (Val 3) (Val 4)))
Just (MkDPair 8 (Trans (RightEta AddBeta IsValue) (Trans AddBeta Refl)))
Coda.
In this post we have seen:
- A formal treatment of Hutton’s Razor
- How to write an evaluator for Razor terms that produce values and the steps required to obtain those values.
When using such programs, Idris’ erasure will remove the unncessary compile time only computations.
Personaly, I think the addendum of obtaining values and computation steps in the evaluation results makes practical application of PLT in languages such as Agda and Idris that little bit more compeling. It provides something that is a little bit more tangible that we see in PLFA.