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 ¹ 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 ². 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

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 ³ 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.