Dependently Typed Lambda Calculus
This is a simple, naive implementation of a lambda calculus with dependent types.
What are dependent types?
Dependent types are types that can depend on values.
In most programming languages, the distinction between a value and a type is sharp. Values are things like 0, 1, 2, "Hello world", [1, 2, 3], the function which sorts a list, etc. Types are things like Integer, List<String>, and functions that take an Integer and return an Integer. You can mix values together, such as function application: f(a). You can mix types together, such as Iterator<Integer>. But you can't mix values and types.
But with dependent types, you can!
In dependent type systems, values and types are on the same level. It is possible to write functions (values) which accept types as arguments or to write types which depend on values (hence the name).
This gives a TON of expressiveness to the language. The first, most basic example taught are the types Fin n and Vect A n.
Fin n is a datatype (defined for all integers n >= 0) which has exactly n values, 0, 1, 2, ..., (n-1). They are useful for when you want to accept a number that is less than n, or when you want to certify your return value will be less than n.
Vect A n is a datatype that contains a list of exactly n objects (all of type A). Unlike regular lists found in most languages, we know how many elements there are at compile time. This prevents us from making silly mistakes, like taking the first element from an empty list. Instead of indexing Vect A n's by an integer (which could lead to out of bounds exceptions), we can index them by Fin n's. Do you see the synergy between the two?
These types don't just sit there when you do stuff, either. The append method for Vect takes two Vects, one of length n and one of length m, and returns a third Vect of length m+n.
But that's not all there is to dependent types.
The phenomenon that makes dependent types so incredibly powerful is called the Curry-Howard correspondence. It's a big word (actually, two names and a word) with a big philosophical idea behind it.
Plain and simply, the Curry-Howard correspondence says that programming and logic are (at some level) the same darn thing. More precisely, it says something about the relation between an object and its type.
Suppose you viewed types as logical propositions. You could imagine all sorts of dependent types:
- Eq x y
- IsEven x
- LessThan x y
- IsPrime p
- IsMortal m
The Curry-Howard correspondence says that IF you can construct an object of that type, the proposition you viewed it as is true.
On the other hand, if it impossible to construct an object, the proposition is false.
So, in a dependently typed language, it's possible to have types that cannot be instantiated. Fin 0, Even 1, Prime 4, IsMortal zeus are all types, but are all empty types.
Having this distinction between empty and non-empty types gives rise to the interestingness in dependent type theory. While all of our usual programming types are non-empty (Integer, List, Bool, etc), many of our new special types are not guaranteed so.
In some cases, you can conditionally construct an object. In the case of IsMortal, for instance. We can't create an object of IsMoral m in all cases. If m is a man, then we have enough to show that IsMortal m, but without knowing anything more about m, we can't prove he is mortal. This conditional can be written as IsMan m -> IsMortal m. Now for the astounding part given by the Curry-Howard correspondence: "IsMan m -> IsMortal m" is just a regular function. Instead of taking an Integer or a List as a parameter, it takes *evidence* that m is a man (otherwise known as an object of type IsMan x). Using that evidence, it constructs an object of type (aka: evidence of) IsMortal m.
Terms come in the flavors:
- Star 0, Star 1, Star 2, ...
- Var 0, Var 1, Var 2, ...
- Lam type body
- Forall type body
- App func arg
There is also support for natural numbers:
And support for equality and absurdity:
The variables are DeBruijn indexes. Be careful, because in Forall terms, if a constant appears in both the premise and the conclusion, they will have different indexes (the conclusion's indexes will be one greater).
The basic calculus is modeled after Ivor. However, binders (and obviously names) do not appear in the contexts.
The normalization is pretty nice in the core, but the natural normalization (Rec terms) are a total kludge.
In theory, all typed terms should normalize. In practice, who knows. Factorial 5 seems to be all it takes to freeze my laptop. (Which is funny, because it is the test I always use when doing shit like this).
- Add real inductive types.
- Add List types.
- Write a pretty printer and parser.
- Write a proper tutorial.