http://okmij.org/ftp/Computation/lambda-calc.html#haskell-type-level

This is the first message in a series on arbitrary type/kind-level computations in the present-day Haskell, and on using of so computed types to give signatures to terms and to drive the selection of overloaded functions. We can define the type TD N to be the type of a tree fib(N)-level deep, and instantiate the read function for the tree of that type. The type computations are largely expressed in a functional language not too unlike Haskell itself.

In this message we implement call-by-value lambda-calculus with booleans, naturals and case-discrimination. The distinct feature of our implementation, besides its simplicity, is the primary role of type application rather than that of abstraction. Yet we trivially represent closures and higher-order functions. We use proper names for function arguments (rather than deBruijn indices), and yet we avoid the need for fresh name generation, name comparison, and alpha-conversion. We have no explicit environment and no need to propagate and search it, and yet we can partially apply functions.

Our implementation fundamentally relies on the connection between polymorphism and abstraction, and takes the full advantage of the type-lambda implicitly present in Haskell. The reason for the triviality of our code is the typechecker's already doing most of the work need for an implementation of lambda-calculus.

Our code is indeed quite simple: its general part has only three lines:

instance E (F x) (F x) instance (E y y', A (F x) y' r) => E ((F x) :< y) r instance (E (x :< y) r', E (r' :< z) r) => E ((x :< y) :< z) r

The first line says that abstractions evaluate to themselves, the second line executes the redex, and the third recurses to find it. Still, we may (and did) write partial applications, the fixpoint combinator, Fibonacci function, and S and K combinators. Incidentally, the realization of the S combinator again takes three lines, two of which build the closures (partial applications) and the third line executes the familiar S-rule.

instance A (F CombS) f (F (CombS,f)) instance A (F (CombS,f)) g (F (CombS,f,g)) instance E (f :< x :< (g :< x)) r => A (F (CombS,f,g)) x r

Incidentally, the present code constitutes what seems to be the shortest proof that the type system of Haskell with the undecidable instances extension is indeed Turing-complete. That extension is needed for the fixpoint combinator -- which is present in the system described in Luca Cardelli's 1988 manuscript:

http://lucacardelli.name/Papers/PhaseDistinctions.pdf

As he wrote, ``Here we have generalized the language of constant expressions to include typed lambda abstraction, application and recursion (because of the latter we do not require compile-time computations to terminate).'' [p9]

This message is all the code, which runs in GHC 6.4.1 - 6.8.2 (it could well run in Hugs; alas, Hugs did not like infix type constructors like :<).

- data HTrue = HTrue
- data HFalse = HFalse
- data Zero = Zero
- data Su a = Su a
- data F x
- class A l a b | l a -> b
- data FNot
- data FAnd
- data f :< x
- class E a b | a -> b
- type Testb x = E ((F FAnd :< (F FNot :< x)) :< (F FNot :< (F FNot :< x))) r => r
- data Rec l
- data FSum'
- type FSum = Rec (F FSum')
- type N0 = Zero
- type N1 = Su N0
- type N2 = Su N1
- type N3 = Su N2
- test_sum :: E ((F FSum :< x) :< y) r => x -> y -> r
- data Fib'
- type Fib = Rec (F Fib')
- test_fib :: E (F Fib :< n) r => n -> r
- data CombK
- data CombS
- type Test_skk x = E (((F CombS :< F CombK) :< F CombK) :< x) r => r
- type CombZ = F CombS :< F CombK
- type CombSu = F CombS :< ((F CombS :< (F CombK :< F CombS)) :< F CombK)
- type CombTwo = CombSu :< (CombSu :< CombZ)
- test_ctwo :: E ((CombTwo :< (F FSum :< Su Zero)) :< Zero) r => r
- class Nat a where

# Documentation

First we define some constants

Show HTrue | We define the instances of Show to be able to show things. We define the instances in a way that the value is not required. |

E HTrue HTrue | Constants evaluate to themselves |

A (F (FAnd, HTrue)) a a | When we receive the second argument, we are in the position to produce the result. Again, we use the case analysis. |

A (F FNot) HFalse HTrue | |

A (F FNot) HTrue HFalse | by case analysis: |

Su a |

Nat x => Show (Su x) | |

Nat x => Nat (Su x) | |

A (F (Fib', self)) Zero (Su Zero) | |

E (:< (:< self n) m) r => A (F (FSum', self, Su n)) m (Su r) | |

E x x' => E (Su x) (Su x') | Other particular rules |

E (:< (:< (F FSum) (:< self n)) (:< self (Su n))) r => A (F (Fib', self)) (Su (Su n)) r | |

E (:< (:< (:< (F Ntimes) f) (:< f x)) n) r => A (F (Ntimes, f, x)) (Su n) r | |

A (F (Fib', self)) (Su Zero) (Su Zero) | |

E (:< f m) r => A (F (Prop', f)) (Su m) (Bool -> r) |

Indicator for functions, or applicable things:

A (F (CombK, a)) b a | |

A (F (FAnd, HFalse)) a HFalse | |

A (F (FAnd, HTrue)) a a | When we receive the second argument, we are in the position to produce the result. Again, we use the case analysis. |

A (F (Prop', f)) Zero Bool | |

E (:< (:< f x) (:< g x)) r => A (F (CombS, f, g)) x r | |

A (F (FSum', self, Zero)) m m | |

E (:< (:< f y) x) r => A (F (Flip, f, x)) y r | |

A (F (Ntimes, f, x)) Zero x | |

E (:< (:< l (F (Rec l))) x) r => A (F (Rec l)) x r | |

A (F FNot) HFalse HTrue | |

A (F FNot) HTrue HFalse | by case analysis: |

E (:< (F Prop) (:< (F Fib) n)) r => A (F StrangeProp) n r | |

A (F (CombS, f)) g (F (CombS, f, g)) | |

A (F (Fib', self)) Zero (Su Zero) | |

A (F (FSum', self)) n (F (FSum', self, n)) | |

A (F (Flip, f)) x (F (Flip, f, x)) | |

A (F (Ntimes, f)) x (F (Ntimes, f, x)) | |

E (:< (:< self n) m) r => A (F (FSum', self, Su n)) m (Su r) | |

A (F CombS) f (F (CombS, f)) | |

A (F CombK) a (F (CombK, a)) | |

A (F Fib') self (F (Fib', self)) | |

A (F FSum') self (F (FSum', self)) | |

A (F FAnd) x (F (FAnd, x)) | Applying And to an argument makes a closure, waiting for the second argument. |

A (F Flip) f (F (Flip, f)) | |

A (F (ATC2 c)) x (F (ATC1 (c x))) | |

A (F (ATC1 c)) x (c x) | |

A (F Ntimes) f (F (Ntimes, f)) | |

A (F Prop') f (F (Prop', f)) | |

E (F x) (F x) | Abstractions are values and so evaluate to themselves |

E (:< (:< (F FSum) (:< self n)) (:< self (Su n))) r => A (F (Fib', self)) (Su (Su n)) r | |

E (:< (:< (:< (F Ntimes) f) (:< f x)) n) r => A (F (Ntimes, f, x)) (Su n) r | |

A (F (Fib', self)) (Su Zero) (Su Zero) | |

E (:< f m) r => A (F (Prop', f)) (Su m) (Bool -> r) | |

(E y y', A (F x) y' r) => E (:< (F x) y) r | Familiar rules for applications |

class A l a b | l a -> bSource

A (F (CombK, a)) b a | |

A (F (FAnd, HFalse)) a HFalse | |

A (F (FAnd, HTrue)) a a | When we receive the second argument, we are in the position to produce the result. Again, we use the case analysis. |

A (F (Prop', f)) Zero Bool | |

E (:< (:< f x) (:< g x)) r => A (F (CombS, f, g)) x r | |

A (F (FSum', self, Zero)) m m | |

E (:< (:< f y) x) r => A (F (Flip, f, x)) y r | |

A (F (Ntimes, f, x)) Zero x | |

E (:< (:< l (F (Rec l))) x) r => A (F (Rec l)) x r | |

A (F FNot) HFalse HTrue | |

A (F FNot) HTrue HFalse | by case analysis: |

E (:< (F Prop) (:< (F Fib) n)) r => A (F StrangeProp) n r | |

A (F (CombS, f)) g (F (CombS, f, g)) | |

A (F (Fib', self)) Zero (Su Zero) | |

A (F (FSum', self)) n (F (FSum', self, n)) | |

A (F (Flip, f)) x (F (Flip, f, x)) | |

A (F (Ntimes, f)) x (F (Ntimes, f, x)) | |

E (:< (:< self n) m) r => A (F (FSum', self, Su n)) m (Su r) | |

A (F CombS) f (F (CombS, f)) | |

A (F CombK) a (F (CombK, a)) | |

A (F Fib') self (F (Fib', self)) | |

A (F FSum') self (F (FSum', self)) | |

A (F FAnd) x (F (FAnd, x)) | Applying And to an argument makes a closure, waiting for the second argument. |

A (F Flip) f (F (Flip, f)) | |

A (F (ATC2 c)) x (F (ATC1 (c x))) | |

A (F (ATC1 c)) x (c x) | |

A (F Ntimes) f (F (Ntimes, f)) | |

A (F Prop') f (F (Prop', f)) | |

E (:< (:< (F FSum) (:< self n)) (:< self (Su n))) r => A (F (Fib', self)) (Su (Su n)) r | |

E (:< (:< (:< (F Ntimes) f) (:< f x)) n) r => A (F (Ntimes, f, x)) (Su n) r | |

A (F (Fib', self)) (Su Zero) (Su Zero) | |

E (:< f m) r => A (F (Prop', f)) (Su m) (Bool -> r) |

The meaning of |A l a b| is that the application to |a| of an applicable thing denoted by |l| yields |b|.

Surprisingly, this already works. Let us define the boolean Not function

The next function is the boolean And. It takes two arguments, so we have to handle currying now.

Commonly, abstraction is held to be `more fundamental', which is reflected in the popular phrase `Lambda-the-Ultimate'. In our system, application is fundamental. An abstraction is a not-yet-applied application -- which is in itself a first-class value. The class A defines the meaning of a function, and an instance of A becomes the definition of a function (clause).

We have dealt with simple expressions and applicative things. We now build sequences of applications, and define the corresponding big step semantics. We introduce the syntax for applications:

and the big-step evaluation function:

E Bool Bool | We can do better, with the help of higher-order type functions. First we declare a few standard Haskell type constants as constants in our calculus, with trivial evaluation rules |

E Int Int | |

E String String | |

E Zero Zero | |

E HFalse HFalse | |

E HTrue HTrue | Constants evaluate to themselves |

E (F x) (F x) | Abstractions are values and so evaluate to themselves |

E x x' => E (Su x) (Su x') | Other particular rules |

(E (:< x y) r', E (:< r' z) r) => E (:< (:< x y) z) r | |

(E y y', A (F x) y' r) => E (:< (F x) y) r | Familiar rules for applications |

E (a -> b) (a -> b) | |

E (a, b) (a, b) | |

E (Node v els) (Node v els) |

type Testb x = E ((F FAnd :< (F FNot :< x)) :< (F FNot :< (F FNot :< x))) r => rSource

That is all. The rest of the message are the tests. The first one is the type-level equivalent of the following function:

testb x = and (not x) (not (not x))

At the type level, it looks not much differently:

We introduce the applicative fixpoint combinator

and define the sum of two numerals

At the type level, this looks as follows

Finally, the standard test -- Fibonacci

Finally, we demonstrate that our calculus is combinatorially complete, by writing the S and K combinators

type Test_skk x = E (((F CombS :< F CombK) :< F CombK) :< x) r => rSource

A few examples: SKK as the identity