Dependently Typed Binary Lambda Calculus

From Esolang
Jump to navigation Jump to search
Paradigm(s) functional
Designed by Anthony Hart
Appeared in 2017
Computational class Turing complete
Reference implementation Original
Influenced by Binary Lambda Calculus
File extension(s) .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;


Example: 1 + 1 = 2

We start by defining the church encoded natural numbers on line 1.

Raw 0110
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;