# Hutton's Razor(s)

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
| 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 imporveRazorV 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


    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 Language for 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.

1. By round too I mean I have been planning on doing it for half a decade or there about… ↩︎