Dependable Types 3: Reductio Sine Absurdum

Welcome back! This time, we’re going to write that evaluate function we mentioned in the last article… Strictly, this function will be better named reduce, as it will perform an operation called beta reduction (or β-reduction, if you’re so inclined). What this means is that, any time we see an Abstraction on the left-hand side of an Application, we can simplify by taking the abstraction’s body, and replacing any mention of its parameter with the argument.

For example:

(λx.x)y

We can reduce this down to y simply by substituting y for all occurrences of x inside the x abstraction. Woo!

As a more complicated example:

(λx.(λy.(λz.z)y)x)a

Here, we have a few nested functions, so we handle them one at a time. First, we substitute a in place of x:

(λy.(λz.z)y)a

Now, we’ve eliminated the abstraction for x (and so the context no longer has an x), but we see that a is now applied to the y abstraction. Let’s do the same thing for y as we did for x:

(λz.z)a

This is exactly the same as the body of the y abstraction, but all the mentions of y have been replaced by a, and so y has been totally eliminated! Finally, we substitute a in place of z:

a

Boom. This, reader mine, is what we’re going to do today. Before we go any further, think about why this might be a bit trickier with De Bruijn indices. Buckle up, friends: we’re gonna need to write some proofs.

Before we get to code, let’s think about the type signature. If we get everything right, the context of the reduced expression won’t change, and nor will the type. As our Expression type is indexed by both of these things, this helps us to refine the set of possible implementations, and hence produce fewer bugs!

reduce
   : Expression ctx ptype
  -> Expression ctx ptype

As usual, to make this code fit on a mobile screen, a lot of the variables have been abbreviated. If you’d prefer to read a more verbose form, the code for this post is a good place to start!

Apart from an Application in an Abstraction, there’s not anything we can do to reduce our expression. So, with that one exception, all this is going to look pretty uninteresting, and just like any other recursive function you might imagine for this type:

reduce
   : Expression ctx ptype
  -> Expression ctx ptype

reduce (Abstraction param body)
  = Abstraction param (reduce body)

reduce (Variable ref)
  = Variable ref

reduce (Application fn arg)
  with (reduce fn, reduce arg)
    | (Abstraction param body, arg')
        = substitute Here body arg'
    | (fn', arg')
        = Application fn' arg'

We can see that, when we encounter the magical situation we’re looking for, we do some kind of substitution of arg' in place of Here inside the body. There’s a catch, though: we’re using Here and There as De Bruijn indices.

Take the following:

(λx.λy.(λz.x)x)

When we use this format, we can identify all the references to x simply because they’re written as x. However, let’s look at the same expression when written with De Bruijn indices:

λλ(λ3)2

The variable three lambdas ago and the variable two lambdas ago are actually the same variable! De Bruijn indices change depending on the level of abstraction-nesting, which means that we’ll also have to keep track of that!

Once again, let’s think about the type for substitute before we write any code. The body is in a different context to the arg': it has an extra variable that isn’t present in the arg'. However, once we finish substitution, we will have eliminated that variable entirely, so it is also missing from the result!

substitute
   : (ref : Elem atype ctx)
  -> Expression
       ctx
       ptype
  -> Expression
       (dropElem ctx ref)
       atype
  -> Expression
       (dropElem ctx ref)
       ptype

Let’s start with the simplest case: Application. In this instance, we recurse down through both sides, and we’re done. We’ll find that Application is very much the simple case in this process, as it is the only one of the three constructors that doesn’t touch the context.

substitute ref (Application fn x) arg
  = Application (substitute ref fn arg)
                (substitute ref x  arg)

Now, let’s have a little look at the case of Abstraction. We probably want to increment the index we’re looking for, so we’ll stick a There on it:

substitute ref (Abstraction param body) arg
  = Abstraction
      param
      (substitute (There ref) body arg)

… Not quite.

Type mismatch between
  Expression
    (dropElem ctx ref)
    atype

    (Type of arg)
and
  Expression
    (dropElem (param :: ctx) (There ref))
    atype

    (Expected type)

This type error rightly tells us that arg is the problem here, and specifically that it is in the wrong context: inside the Abstraction, there is an extra parameter in our context to worry about, so we need to update the arg context accordingly. Luckily, we know that the arg works in the ctx context, so param doesn’t get a mention inside. All we need to do is increment the references.

… Ish. If a variable is introduced within that body, we should not bump the reference - we only care about those that come from outside the body, which we call the free variables of the body expression. Symmetrically, those that come from inside the body will be referred to as bound variables.

expandContext
   : (bound : Context)
  -> Expr (bound ++      free) t
  -> Expr (bound ++ a :: free) t

This type describes what we want: expand the context by one more bound variable. Consequently, we’ll need to increment all free references, but none of the bound references. Sorry if these last few paragraphs take a few readthroughs…

expandContext ctx (Application fn x)
  = Application (expandContext ctx fn)
                (expandContext ctx x)

expandContext ctx (Abstraction param body)
  = Abstraction
      param
      (expandContext (param :: ctx) body)

expandContext ctx (Variable ref)
  = Variable (expandElemContext ctx ref)

As before, Application is nice and easy. Abstraction is a bit ugly, but as expected: we add this new param to the bound list, and recurse. The fun happens in the Variable case: we want to update the ref when it’s a reference to a free variable. Let’s have a look at that function:

expandElemContext
   : (bound : Context)
  -> Elem t (bound ++      free)
  -> Elem t (bound ++ a :: free)

expandElemContext [] ref
  = There ref

expandElemContext (_ :: _) Here
  = Here

expandElemContext (_ :: xs) (There later)
  = There (expandElemContext xs later)

When we have an empty context, all references must be free. If we have a Here reference to a non-empty context, we know it must be bound! In any other case, we can just drop the most recent bound variable, and a layer of the reference, and recurse! This function isn’t too scary, really: we ignore a reference within the context, and increment a reference beyond. Don’t panic!

Now we have all that out the way, we can rewrite our substitute statement:

substitute ref (Abstraction param body) arg
  = Abstraction
      param
      ( substitute
          (There ref)
          body
          (expandContext [] arg)
      )

Magnifique.

The only case we haven’t considered for substitute yet is Variable. I’ve deliberately left this one until last because, well, it’s quite scary. To people unfamiliar with Idris, this is going to look… well, unfamiliar. Nevertheless, let’s crack on!

When we encounter a Variable within an expression, one of two things may be true:

• The Variable’s reference is not the one we’re looking to eliminate, so we just update it if necessary.

• The Variable’s reference is the one we’re looking for, and we want to replace this Variable with the given arg.

Now, if the variable is the one we’re looking for, we’re going to have to prove a couple things to Idris. First of all, atype and ptype are going to have to be equivalent. If we can’t prove this, Idris won’t let us unify atype and ptype, as they could be different. Secondly, we have to prove that the context references are indeed the same! The order isn’t especially important, but both are required to satisfy the compiler.

Enough stalling for time; let’s see the beast:

substitute {atype} {ptype} ref (Variable ref') arg
    with (decEq ptype atype)
  substitute {atype = ptype} ref (Variable ref') arg
    | (Yes Refl)
          with (decEq ref' ref)
        substitute ref' (Variable ref') arg
          | (Yes Refl)
          | (Yes Refl)
          = arg
        substitute ref (Variable ref') arg
          | (Yes Refl)
          | (No contra)
          = Variable (independentRefs ref' ref contra)
  substitute ref (Variable ref') arg
    | (No contra)
    = Variable (independentValues ref' ref contra)

Warned you, right? There are a couple things going on here. Firstly, we’re pulling terms out of the type. This is another bit of “dependently-typed magic”: we can reflect things down from the type-level, such as atype and ptype (the ProgramType indices for the expression and the substitution), and then use them within our function! Types are terms are types are terms. It really is magical.

Now we have access to those values, we can use decEq (decidable equality) to compare them. The result of doing so is either Yes prf or No contra, where prf and contra are proofs of one way or the other. We’ll see more of these in a moment.

I’m omitting the accompanying DecEq ProgramType implementation because it’s quite mechanical, and doesn’t contain anything we’re not about to see. However, if you’re enjoying this, I’d encourage you to go take a look!

If we successfully prove both, the result is simply arg: we know that we’re safe to make the substitution, so we replace the Variable with the arg we’ve been carrying. Job done! If that isn’t, the case, however, we have a little more work to do. Specifically, we need to update the Variable index to account for the now-eliminated parameter. To avoid a Maybe, let’s have a go at proving that our reference can be adjusted safely. You’ll notice that the above code had two proofs: independentRefs and independentValues are the holes that we’re going to have to fill.

Don’t think there was any magic in the selection of proofs. Most of this code was written with a lot of help from Idris’ editor plugin. Most of the time with proofs, the obvious proof search will do most (if not all) the work for you!

Firstly, let’s look at the type of independentRefs:

independentRefs
   : (l : Elem x xs)
  -> (r : Elem x xs)
  -> Not (l = r)
  -> Elem x (dropElem xs r)

Here, we have to prove that, if the l and r values are not equal, x will exist in the list without the element to which r refers. In other, simpler words: if l and r are both references to a value of some type, and they’re not the same, that type must be in there at least twice, and we can remove one and provide a reference to another!

independentRefs Here Here prf
  = absurd (prf Refl)

We first deal with the case in which the two references are the same. However, we already have a proof that this can’t be the case, so this is… absurd! The proof is Refl (we can think of this as “obvious” for now), given the proof that Not (l = r).

I won’t go into too much detail, but absurd is a function from Void to anything. In other words, there’s no way this can happen!

independentRefs Here (There later) prf
  = Here

If l points to the first element, and r to any other, then we know that dropping r will make no difference - the element will be in first place!

independentRefs (There later) Here prf
  = later

Similarly, if r points to the first, and l to something later, the element is simply one place closer to the start than before.

independentRefs (There this) (There that) prf
  = There (independentRefs this that (prf . cong))

Here’s our recursive step. If both references are later on, we recurse. Notice the cong function here:

cong : a = b -> f a = f b

“If a and b are the same, applying f to both will give the same answer”. The f here is There: if we can remove a There from each and still prove that they’re the same, we’re good! Now, what about that independentValues function? Well, it’s almost identical to the above. The only reason it has to exist is that, this time, we want to prove that, if the referenced values are different, removing one won’t remove the other:

independentValues
   : (l : Elem x xs)
  -> (r : Elem y xs)
  -> Not (x = y)
  -> Elem x (dropElem xs r)

This one is even simpler, as we don’t have to carry the cong proof: we only care about the proof at the point that it fails. Voila:

independentValues Here Here prf
  = absurd (prf Refl)

independentValues (There later) Here prf
  = later

independentValues Here (There later) prf
  = Here

independentValues (There x) (There later) prf
  = There (independentValues x later prf)

Now, we have everything we need. We’ve made it, friends: the above is almost everything from this article’s code. Still, while we’re here, why don’t we try one last party trick?

Earlier, we had this expression:

(λx.(λy.(λz.z)y)x)a

If we convert this to our format, we get something rather more ugly:

Test : Expression (x :: context) x
Test {x} -- x is just a type!
  = Application
      ( Abstraction
          x
          ( Application
              ( Abstraction
                  x
                  ( Application
                      ( Abstraction
                          x
                          ( Variable Here
                          )
                      )
                      ( Variable Here
                      )
                  )
              )
              ( Variable Here
              )
          )
      )
      ( Variable Here
      )

Here, we’re saying that Test is an expression in any context with an x at the head, and it has a return type of x. Given that we already know the result of reducing this expression is just Variable Here, why don’t we write a test?

Dependent types to the rescue once more. Thanks to the magic of Idris, where terms are types and types are terms, we can write our tests at the type-level, and have them checked whenever we compile! On top of that, the compiler will recognise them as dead code after type-checking, so they won’t appear in the output binary! Here’s how we’d write the type of our test:

allClear
  : reduce (Test {context = []} {x = PInt})
  = Variable Here

We’re giving the compiler a couple hints here: to avoid polymorphism confusion, we specialise our context and x values to make it easier for the type-checker. In actual fact, this is required for the next step. What this type says is that reducing our expression is equivalent to the reduced form we expect. What do we write for our body, though?

allClear
  = Refl

The most beautiful line in this whole post. The type-checker will do the reduction, arrive at the result of Variable Here, and then the proof of this test becomes obvious. Now, whenever we change our code, this reduction will be carried out, and the result will be checked. If the result does not match the intended output, compilation will fail.

Failing tests are now type errors. How awesome is that?

Ok, this has been the longest post I’ve written by quite a way, but there was a lot to cover! I hope this has given you some sort of idea about how we write proofs for the type system, and how they allow us to expand contexts, update variable references, and all sorts of things we haven’t covered here!

Next time, we’ll be looking at some serious dependently-typed magic. We’ll be turning our Expression values into actual Idris functions that we can call with arguments and receive results, all while remaining totally type-safe. Until then, feel free to contact me on Twitter with any suggestions, questions, criticisms, and so on. I’d love to hear from you, and see what you’ve been concocting!

Until next time, take care ♥

As always, a huge thanks to Liam for teaching me everything I know about Idris. Thanks also to Gabe for proofreading this article (among many)!