Dependently Typed Binary Lambda Calculus

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
Category:Languages
Category:Turing complete
Category:Functional paradigm
Category:Implemented
Category:2017