Dependable Types 1: Full-STλC Development09 Jan 2018
Hello again! Been a while, right? Sorry for being AWOL the best part of six months; I got my dream job writing Haskell and PureScript with some brilliant minds over at Habito, and I’ve had a lot to learn! Anyway, one such mind is Liam, (who’ll be a familiar face to anyone getting stuck in with PureScript), and we have been spending our lunch times on various little projects. So, I thought it’d be cool to share one of these projects with you!
Spoiler: the project we’ll be going through is up on GitHub, and you can download the code for this series if you want to play about with it. Head over to the Idris site if you need any help getting set up.
This “series” is probably going to end up as four-or-five posts, easing into GADTs, dependent types, and beyond, so buckle up! Before we get into that, though, let’s make sure we’re all on the same page, and have a quick refresher on the lambda calculus. If you’re already familiar with the lambda calculus (untyped and simply-typed), this post isn’t going to be super interesting for you, but I’ll hopefully see you later on!
The Untyped Lambda Calculus
The lambda calculus is a Turing-complete language made up of only 3 constructs: variables, abstractions, and applications. First, a cheat sheet:
Application. Given some expression
Mthat evaluates to a function, and some expression
Nthat evaluates to a value, apply
Mto get some result.
Abstraction. We can define a function that takes an argument,
x, and returns the result of running
Mcan be an expression that refers to
x, just as functions in any other language can use the value we provide.
Variable. This is how we refer to variables introduced in abstractions. We can’t talk about variables that haven’t been introduced (think of these as undefined variables in other languages), so every variable must refer to an argument supplied in an abstraction.
Hopefully, that made some sense. Just in case, though, let’s run through a few examples of some functions written using our calculus.
Probably the simplest program we could write,
id just takes the argument we
give it and hands it back to us. We have an abstraction,
λx.__, with a
Here, we take two arguments, and just return the first one (effectively ignoring the second). Nothing too complicated, and still looks a lot like the languages we’re familiar with. Notice that, when we want multiple arguments, we nest abstractions and get the arguments once at a time.
This time, we take a function and two arguments, but apply the arguments in the opposite order. More nesting, but still hopefully not doing anything too unfamiliar!
Hopefully, this gives us some idea about how this language works, and how we’d use these three constructs together to build up programs. There’s one last thing I wanted to talk about in this post, though: De Bruijn Indices.
Our syntax is great and all, but there is room for error. We could give two abstraction parameters the same name, which would add confusion, especially when we come to substitution in later posts. Ideally, we want a way to refer to abstraction parameters unambiguously, and that’s where our man Nicolaas comes in. In every abstraction, a new variable is introduced. De Bruijn indices count the number of nested abstractions between a variable’s introduction and its use.
Let’s start with
id, which is
λx.x. This variable is used immediately
inside the abstraction that introduces it, so we can rewrite this as
read this as, “Return the variable introduced in the latest abstraction”.
const? Well, with
x is again the variable in use, but
this time, there is a new variable introduced between the
x and its original
mention. Because of this, we use
2 to mean, “The variable from the
last-but-one abstraction”, and hence rewrite
As a last example, we can rewrite
λλλ312. This is because we apply
the last-but-two variable,
f, to the last variable,
x, and then
apply the result to the last-but-one variable,
Confusing, right? Don’t worry: I promise there’s a point to this. When we come to building the data type for lambda calculus expressions, using a form of De Bruijn indices will make it much easier for us to guarantee correctness. It’s all very exciting. If you want a little exercise to try out, see if you can encode the following with De Bruijn indices:
It’s a bit of a tricky one, but hopefully manageable. If you’re curious, this
function is called
on in Haskell’s
and is useful for all sorts of things!
All Together Now
One last note: the Idris project we’ll be going through is an implementation of
the simply-typed lambda calculus. What’s the difference between that and
what we’ve already seen? Simply that the variables, applications, and
abstractions all have types (like
Int -> Int - that sort of
thing). In practice, this is the same thing as any other programming language
with a simple type system, and we’ll track these through our program to make
sure that non-functions don’t end up being used as functions, or to avoid
invalid parameter usage.
Anyway, that’s all for now! It’s been lovely to talk to you again, and I hope I’ll be seeing you some time next week. Until then, take care ♥