Dependently Typed Binary Lambda Calculus is a modification of Binary Lambda Calculus which adds type dependency, as well as features useful for code reuse.
Language overview
Every program in the language is made up of a single string of binary digits. There are four key patterns.
| Constructor
|
Meaning
|
00
|
Function application
|
010
|
Lambda abstraction/Pi type
|
11...0
|
Signifies a number
|
011
|
Calls a predefined function within a context
|
Application is ordinary function application, and expects two arguments. 010 is used both for lambda abstractions and pi types. As a consequence, it expects two arguments, the first being the input type, and the second either being the output program or type, depending on whether it's being used as a lambda abstraction or a pi type. Numbers are precisely a count of the number of 1s in an expression. For example 10 is 1, 1110 is 3, etc. 011 expects to be followed by a number. That number then signifies a "line" in the program. Because of how this operator is encoded, it can be followed directly by 0, in which case it signifies the type of types.
Expressions in the language are tokenized left-to-right, then a syntax tree is built up right-to-left using a stack parser. A typical program will end with a stack that has several expressions in it. Each expression in the final stack is considered independent, as a proxy for a new line. For example 01100100110010101100111001001100101010 will be tokenized into something along the lines of * λ * λ 1 2 ln{1} λ * λ 1 1, which is then parsed into four "lines", purely by virtue of the parser not being able to interpret it as a single tree.
* λ(*, λ(1, 2)) ln{1} λ(*, λ(1, 1))
in those expressions, the numbers that don't correspond to a line number are de Bruijn indices.
A correct program should consist of a sequence of pairs of expressions, corresponding to type-term pairs. In the previous example, the first pair is * and λ(*, λ(1, 2)), representing a program of type *, the type of types. So that first line defines a new type (in this case, the church encoded unit type) and stores it in the first "line". The second pair is ln{1} and λ(*, λ(1, 1)), signifying a program of type (whatever's on line 1). Since the unit type is on line 1, this second pair defines a term of the unit type.
Running a program primarily involves type checking. If a program successfully checks, then the normal form of the final term in the program is outputted.
Example: Lists
The list type will be a function from types to types;
| Raw
|
01001100110
|
| AST
|
λ(*, *)
|
| Rep
|
* → *
|
defined as;
| Raw
|
0100110010011001010010010111100101110111101110
|
| AST
|
λ(*, λ(*, λ(1, λ(λ(3, λ(3, 4)), 3))))
|
| Rep
|
λ(A : *) . Π(X : *) . X → (A → X → X) → X
|
In this example, 010 is used both as a pi type and lambda expression, but its usage is disambiguated by the provided type.
We can proceed to define the nil list. Its type signifies that we're taking a type and making a list of that type.
| Raw
|
0100110000111010
|
| AST
|
λ(*, ln{1}(1))
|
| Rep
|
Π(X : *) . List(X)
|
The nil list is then implemented as
| Raw
|
01001100100110010100100101110010111011110110
|
| AST
|
λ(*, λ(*, λ(1, λ(λ(3, λ(3, 4)), 2))))
|
| Rep
|
λ(X Y : *)(n : Y)(s : X → Y → Y) . n
|
Cons becomes;
| Raw
|
010011001010010000111011000011101110
|
| AST
|
λ(*, λ(1, λ(ln{1}(2), ln{1}(3))))
|
| Rep
|
Π(X : *) . X → List(X) → List(X)
|
| Raw
|
010011001010010000111011001001100101001001011111001011101111000001011111000000011110111011010
|
| AST
|
λ(*, λ(1, λ(ln{1}(2), λ(*, λ(1, λ(λ(5, λ(3, 4)), 1(5)(4(3)(2)(1)) ))))))
|
| Rep
|
λ(X : *)(x : X)(l : List(X))(Y : *)(n : Y)(s : X → Y → Y) . s(x)(l(Y)(n)(s))
|
and concatenation becomes;
| Raw
|
0100110010000111010010000111011000011101110
|
| AST
|
λ(*, λ(ln{1}(1), λ(ln{1}(2), ln{1}(3))))
|
| Rep
|
Π(X : *) . List(X) → List(X) → List(X)
|
| Raw
|
0100110010000111010010000111011001001100101001001011111001011101111000000011111011100000001111011101101010
|
| AST
|
λ(*, λ(ln{1}(1), λ(ln{1}(2), λ(*, λ(1, λ(λ(5, λ(3, 4)), 5(3)(4(3)(2)(1))(1) ))))))
|
| Rep
|
λ(X : *)(l1 : List(X))(l2 : List(X))(Y : *)(n : Y)(s : X → Y → Y) . l1(Y)(l2(Y)(n)(s))(s)
|
So, our full list implementation is;
0100110011001001100100110010100100101110010111011110111001001100001110100100110010011001010010010111001011101111011001001100101001000011101100001110111001001100101001000011101100100110010100100101111100101110111100000101111100000001111011101101001001100100001110100100001110110000111011100100110010000111010010000111011001001100101001001011111001011101111000000011111011100000001111011101101010
Example: 1 + 1 = 2
We start by defining the church encoded natural numbers on line 1.
| Raw
|
01001100101001001011011101110
|
| AST
|
λ(*, λ(1, λ(λ(2, 3), 3)))
|
| Rep
|
Π(X : *) . X → (X → X) → X
|
We then define 1 and 2 for later on lines 2 and 3;
| Raw
|
01110
|
| AST
|
ln{1}
|
| Rep
|
Nat
|
| Raw
|
01001100101001001011011100010110
|
| AST
|
λ(*, λ(1, λ(λ(2, 3), 1(2) )))
|
| Rep
|
λ(X : *)(z : X)(s : X → X) . s(z)
|
| Raw
|
01110
|
| AST
|
ln{1}
|
| Rep
|
Nat
|
| Raw
|
010011001010010010110111000100010110
|
| AST
|
λ(*, λ(1, λ(λ(2, 3), 1(1(2)) )))
|
| Rep
|
λ(X : *)(z : X)(s : X → X) . s(s(z))
|
We define addition on line 4;
| Raw
|
010011100100111001110
|
| AST
|
λ(ln{1}, λ(ln{1}, ln{1}))
|
| Rep
|
Nat → Nat → Nat
|
| Raw
|
0100111001001110010011001010010010110111000000011111011100000001111011101101010
|
| AST
|
λ(ln{1}, λ(ln{1}, λ(*, λ(1, λ(λ(2, 3), 5(3)(4(3)(2)(1))(1) )))))
|
| Rep
|
λ(n1 n2 : Nat)(X : *)(z : X)(s : X → X) . n1(X)(n2(X)(z)(s))(s)
|
For reasoning about equality, we can define the ordinary Leibniz equality on line 5;
| Raw
|
0100110010100101100110
|
| AST
|
λ(*, λ(1, λ(2, *)))
|
| Rep
|
Π(X : U) . X → X → *
|
| Raw
|
0100110010100101100100101110011001000101110001101110
|
| AST
|
λ(*, λ(1, λ(2, λ(λ(3, *), λ(1(3), 2(3)) ))))
|
| Rep
|
λ(X : U)(x y : X) . Π(P : X → U) . P(x) → P(y)
|
We can then define proof by reflexivity on line 6;
| Raw
|
0100110010100000000111111101101010
|
| AST
|
λ(*, λ(1, ln{5}(2)(1)(1) ))
|
| Rep
|
Π(X : U)(x : X) . Id(X)(x)(x)
|
| Raw
|
0100110010100100101100110010001011010
|
| AST
|
λ(*, λ(1, λ(λ(2, *), λ(1(2), 1))))
|
| Rep
|
λ(X : *)(x : X)(P : X → *)(px : P(x)) . px
|
And we are finally ready for our conclusion, that 1 + 1 = 2,
| Raw
|
000000011111110011100000011111100111100111100111110
|
| AST
|
ln{5}(ln{1})(ln{4}(ln{2})(ln{2}))(ln{3})
|
| Rep
|
Id(Nat)(Plus(1)(1))(2)
|
| Raw
|
00000111111110011100111110
|
| AST
|
ln{6}(ln{1})(ln{3})
|
| Rep
|
Refl(Nat)(2)
|
Our complete proof is then;
0110010011001010010010110111011100111001001100101001001011011100010110011100100110010100100101101110001000101100100111001001110011100100111001001110010011001010010010110111000000011111011100000001111011101101010010011001010010110011001001100101001011001001011100110010001011100011011100100110010100000000111111101101010010011001010010010110011001000101101000000001111111001110000001111110011110011110011111000000111111110011100111110