In this post we will consider *Hutton’s Razor*.

This post was derived from a literate Idris file so there will be some cruft related to Idris that will remain until I get round to ^{1} improving Idris’ literate mode support.

```
module Main
```

We will need some data structures, and helper functions, not defined in Idris’ prelude.

```
import Data.List
```

The following two imports are from my container’s library, we will need these in the final sections to keep our musing’s DRY.

```
import Data.DList
import Data.DeBruijn
```

Totality is a good thing here.

```
%default total
```

## The Original Razor

```
namespace Original
```

Let us first consider the original razor.
It is my understanding that *Hutton’s Razor* is *the* mininal expression language to help reason about programming language concepts.
That is operating on: Abstract Syntax.
The phase is a homage to *Occam’s Razor* to ensure that our problems are stated as /Minimally Viable Problems/ (MVPs).

Hutton’s Razor, first appeared in Fold and unfold for program semantics, and contains integer values and integer addition. Within Idris the language is defined as a simple datatype:

```
data Razor = I Int | Add Razor Razor
```

Although, the original definition is an indexed type to explore manipulation, we do not add the flexibility here.

With our definition, we can construct a simple evaluation function for `Razor`

that runs the computation.

```
eval : Razor -> Int
eval (I x) = x
eval (Add x y) = (+) (eval x) (eval y)
```

Using type-level equality `(=)`

we can also test to see if the evaluation function is correct:

```
Example : Razor
Example = Add (I 4) (I 5)
test : eval Example = 9
test = Refl
```

## A Razor with Variables

```
namespace WithVars
```

`Razor`

is a simple definition, and is useful for exploring fundamental program transformations.
However, it is not expressive enough to explore simple program transformations such as ’let-floating’ and ’normal forms'
To do so we need to include notions of variables and binding.
Fortunatly, we can extend `Razor`

to incorporate such notions.

```
data RazorV = I Int
| Var String
| Add RazorV RazorV
| Let String RazorV RazorV
```

We now have a minimal expression language to reason about programming language concepts and transformations relating to form ^{2}.
Here `Var`

represents a variable, and `Let`

is a binding site to bind an expression to a variable name.
As an example here is our previous example rewritten:

```
Example : RazorV
Example = Let "x" (I 4) (Add (Var "x") (I 5))
```

and here is an error handling evaluation function to run computations.

```
eval : (env : List (String, Int))
-> (expr : RazorV)
-> Maybe Int
```

Error handling is required in case we encounter a variable name that is not found.
We need to provide an environment (`env`

) to record variables and their evaluated expressions.

```
eval env (I value) = Just value
```

Constants return values.

```
eval env (Var x) = lookup x env
```

When encountering variables we need to search the environment for it’s value.
It is this evaluation step that *can* fail.

```
eval env (Add x y) =
do x' <- eval env x
y' <- eval env y
pure (x' + y')
```

For addition we can take advantage of `Maybe`

being a computation context and use ‘Do-Notation’ to pass failing cases around seemlessly.
For `Add`

, we evaluate each operand and perform the computation using the primitive operation `(+)`

.

```
eval env (Let this beThis inThis) =
do beThis' <- eval env beThis
eval ((this,beThis')::env) inThis
```

Our final case is binding site creation.
We evaluate `beThis`

and extend our environment to associate variables called `this`

with the evaluation result.
We then evaluate `inThis`

, the remaining computation, to operate the result.

We can run our test as before:

```
test : WithVars.eval Nil WithVars.Example = (Just 9)
test = Refl
```

We have disambiguated the function and values to ensure our test uses the required function and value.

## A Well Scoped Razor

```
namespace WellScoped
```

`RazorV`

requires an error handling evaluation function.
This is not ideal.
Within Dependently Typed Languages we can imporve`RazorV`

to better reason about variables such that our expressions will be *Well-Scoped* by default.
We do so using standard techniques.

Thus we now have:

```
data RazorS : (ctxt : List String) -> Type where
```

We paramterise the type of our language with a variable context to record used variable names.

```
I : (value : Int) -> RazorS ctxt
```

Values remain the same.

```
Var : (idx : Elem binder ctxt) -> RazorS ctxt
```

Variables are now proofs that the variable name exists within the context.

```
Add : (x : RazorS ctxt)
-> (y : RazorS ctxt)
-> RazorS ctxt
```

Addition is defined the same.

```
Let : (this : String)
-> (beThis : RazorS ctxt)
-> (inThis : RazorS (this::ctxt))
-> RazorS ctxt
```

Our binding site is the same at the value level, but at the type-level we extend the context for `inThis`

with the introduced variable name.

Much of the construction follows that of `RazorV`

but these suitable type-level differences are important.
Consider our running example:

```
Example : RazorS Nil
```

The type-level typing context is empty as we make no assumptions about exisit names.

```
Example = Let "x" (I 4) (Add (Var Here) (I 5))
```

The example is much the same as before except that `Var`

states that we are referring to the latest variable that was introduced at a binding site.

Like `RazorV`

, to evaluate `RazorS`

expressions we need an environment.

```
data Env : (ctxt : List String) -> Type where
```

We parameterise the the type of `Env`

with the variable context to ensure that our environment grows and shrinks in the same way as the variable-context.

```
Empty : Env Nil
```

Empty environments have empty contexts.

```
Extend : (value : Int)
-> (rest : Env ctxt)
-> Env (binder::ctxt)
```

Extending the environment adds a `value`

that has an associated `binder`

.

We can use our proof that a variable binder exists to safely index our environment to retrieve a value.

```
lookup : (env : Env ctxt)
-> (prf : Elem binder ctxt)
-> Int
lookup (Extend value rest) Here = value
lookup (Extend value rest) (There later) = lookup rest later
```

This function unrolls the `Elem`

proof *and* environment until it encouters `Here`

, and then returns the value at that position.

With `lookup`

and `Env`

we can construct a error handling free version of `eval`

.

```
eval : (env : Env ctxt)
-> (expr : RazorS ctxt)
-> Int
```

Notice how the context of the expression matches the context of the environment!

```
eval env (I value) = value
```

Values *still* return values.

```
eval env (Var idx) = lookup env idx
```

Variables now use the safe lookup function to return a value free of error handling.

```
eval env (Add x y) = (+) (eval env x) (eval env y)
```

We no longer need to use ‘Do-notation’ to take advantage of computation contexts, of which we are no longer in one.

```
eval env (Let binder beThis inThis) = eval (Extend (eval env beThis) env) inThis
```

Evaluation of binding sites also becomes ‘simplified.

Our tests run as expected.

```
test : eval Empty Example = 9
test = Refl
```

Of note: there was an Agda definition created by James Chapman for an FP Lunch ^{3} at the University of Nottingham that presents a similar construction but sans binding sites.

## The Well-Typed Razor

```
namespace WellTyped
```

We move on now to looking back at the original Razor in terms of program structure but to also include types. We shall do so in the style of the /Well-Typed Interpreter/.

Before, Hutton’s Razor was singularly typed: Untyped if you feel that way inclined. We will introduce two types of numbers: Integers and Reals.

```
data Ty = INT | REAL
```

We encode these types using an enumerated type.
As part of our implementation of `RazorT`

we need to map our types (`Ty`

) to concrete implementations.
We do so using `interpTy`

:

```
interpTy : Ty -> Type
interpTy INT = Int
interpTy REAL = Double
```

The mapping is straightforward.

However, we also need to construct a predicate to represent the same mapping. This will be useful when we write the evaluation function.

```
data InterpTy : Ty -> Type -> Type where
IsInt : InterpTy INT Int
IsDbl : InterpTy REAL Double
```

Here `InterpTy`

captures the same mapping as `interpTy`

but presents the mapping as evidence.

We can now construct our expression language.

```
data RazorT : Ty -> Type where
```

We now paramterise our type for expressions by `Ty`

to ensure that all expressions are /well-typed/.

```
V : interpTy type -> RazorT type
```

Values contain ‘real’ values computed from the type `type`

.

```
Add : (x : RazorT type)
-> (y : RazorT type)
-> RazorT type
```

Addition works on expressions of the same type.

Here are some examples of well-typed expressions.

```
ExampleI : RazorT INT
ExampleI = Add (V 5) (V 4)
ExampleF : RazorT REAL
ExampleF = Add (V 5.0) (V 4.0)
```

Should we try and make ill-typed expressions our examples will fail to type-check.

We can now transition to writing our evaluation function.

```
doEval : (prf : InterpTy ty type)
-> (expr : RazorT ty)
-> interpTy ty
```

Our evaluation function is a dependent function whose return type is dependent on the to-be-evaluated expression’s type. We also require a predicate to help inform the translation. We will see it’s usefulness in the next equation.

```
doEval prf (V x) = x
```

Values are returned as normal.

```
doEval prf (Add x y) with (prf)
doEval prf (Add x y) | IsInt = (+) (doEval IsInt x) (doEval IsInt y)
doEval prf (Add x y) | IsDbl = (+) (doEval IsDbl x) (doEval IsDbl y)
```

The addition operator `(+)`

is part of the `Num`

interface.
To enable use of the correct addition operation we need to tell Idris which addition operation we are using.
Dependent pattern matching on the proof supplies the compiler with the required evidence.
The Well-Typed Interpreter from Idris’ documentation doesn’t require this as it uses a more generic construction that supplies the required operation.
Here we strive for a Razor with *just* addition and not generic binary operations.

Before we can construct the evaluation function we present a simple function to construct proofs of type `InterpTy`

.

```
whichPath : (ty : Ty)
-> (type : Type ** InterpTy ty type)
whichPath INT = (_ ** IsInt)
whichPath REAL = (_ ** IsDbl)
```

Here `whichPath`

acts as a partial covering function in that we return a dependent pair to introduce (at the type-level) the concrete type each `ty`

is being mapped to.
We now present the final evaluation function:

```
eval : (expr : RazorT ty)
-> interpTy ty
eval expr {ty} with (whichPath ty)
eval expr {ty} | path = doEval (snd path) expr
```

Here `eval`

will calculate the required proof and pass it on to `doEval`

which performs the evaluation.

## The Well-Scoped-Well-Typed (Nameless) Razor

```
namespace WellScopedTyped
```

In our final example, we extend `RazorT`

to include variables such that it becomes a well-scoped and well-typed expression language.
This combines what we have seen with our previous examples.
We shall reuse our definition of `Ty`

from above.

First we reframe `InterpTy`

as a new predicate called:

```
data IsNum : (type : Ty) -> (real : Type) -> Type where
IsInt : IsNum INT Int
IsDbl : IsNum REAL Double
```

We can now write our expression language.

```
data RazorST : List Ty -> Ty -> Type where
```

We parameterise the type of expressions with a typing-context *and* a type.
Our typing context here is a nameless representation and we will use a positional proof (as we did with `RazorS`

) to ensure that we refer to variables with respect to their binding site.
This is the ‘DeBruijn’ representation often used in reasoning about names.
Fortunatly this is a common design pattern when reasoning about languages.
So much so, that I have a helper library (`Data.DeBruijn`

) as part of the containers package to help make things easier.

```
Val : (value : interpTy type) -> RazorST ctxt type
```

Values have the same representation as `RazorT`

.

```
Var : (idx : Index Ty ctxt ty) -> RazorST ctxt ty
```

Rather than use existenial quantification over lists memebership (i.e. `Elem`

) we will use `Index`

from `Data.DeBruijn`

.
Structurally, it is the same as `Elem`

but we make explicit the type of elements in the list.
It can be the case that when constructing environments or types there will be a slight difference in the element type you want to work with at the type-level, and the one contained in expressions.
Being explicit here helps.

```
Add : (prf : IsNum a type)
-> (x : RazorST ctxt a)
-> (y : RazorST ctxt a)
-> RazorST ctxt a
```

Another change we make is how to carry proof over which implementation of `Add`

we will need during evaluation.
Rather than externalise the proof as we did in `RazorT`

, we internalise it.
Here we the proof is: `IsNum`

.
One can think of this construct as similar in concept to an interface constraint in that `prf`

is the evidence that `a`

can be translated to something that can perform numeric.
If we were to add another type, `Booleans`

, then we can introduce other predicates that present evidence that a type can do logical things.

```
Let : RazorST ctxt a
-> RazorST (a::ctxt) b
-> RazorST ctxt b
```

The final constructor is `Let`

.
Let follows previous implementations but is nameless.
We do not need to provide a binder to address the variable.

We can now move onto constructing our evaluation function:

```
eval : (env : Env Ty interpTy ctxt)
-> (expr : RazorST ctxt ty)
-> interpTy ty
```

The function `eval`

is a dependent function that takes an environment and an expression, and returns a value.
Here the type `Env`

comes from `Data.DeBruijn`

and is a dependent list that allows one to collect evaluated values.
With use of `Env`

comes `read`

and `extend`

functions to interact with environments.

```
eval env (Val value) = value
```

Values are values.

```
eval env (Var idx) = read id x env
```

As `RazorST`

is well-scoped and well-typed variables can be read safely from the environment.

```
eval env (Add IsInt x y) = (+) (eval env x) (eval env y)
eval env (Add IsDbl x y) = (+) (eval env x) (eval env y)
```

Addition is straightforward, and now that we have internalised the proof, explicit dependent pattern matching is not required.

```
eval env (Let x y) = eval (extend env (eval env x)) y
```

Evaluation of binding sites defined by `Let`

follows.

## Coda

In this post we have considered implementing Hutton’s Razor, and two variants, in Idris:

- Razor with variables; and
- Razor with types;

and their combination as:

- Razor with variables and types.

I should follow up these posts with describing how to reason more about the languages using Idris, much like we see in PLFA and software foundations.

I like the idea of Hutton’s Razor not *being* the simplest expression language to reason about programs, but rather I think we should think of Hutton’s Razor as being:

the

Minimalist Viable Languagefor demonstrating your idea.

Much like we have notions of /Minimal Viable Product/ and /Minimal Failing Example/ simple examples help remove the cruft from presentation of your ideas. Sometimes starting with the STLC and it’s extensions is just too complicated, and that our Razors should always fall in between Hutton’s Original Razor and the many variants of the STLC. Thus allowing you to concentrate what you are doing and not corner cases you may not need.

When playing about with dependent types I have started to use these variants of Hutton’s Razor to explore new construction techniques, and explore let-floating and normal forms! Deploying a suitable Razor makes things that little bit easier.

So

Keep it Real; Keep it Simple; Keep it Small.