# Dependently Typed Binary Lambda Calculus

Paradigm(s) functional Anthony Hart 2017 Turing complete Original Binary Lambda Calculus `.dblc`

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 `0110` AST `*` Rep `*`
 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`