Language.TypeLC

Description

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 :<).

Synopsis

Documentation

data HTrue Source

First we define some constants

Constructors

HTrue

Instances

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:

data HFalse Source

Constructors

HFalse

Instances

Show HFalse
E HFalse HFalse
A (F (FAnd, HFalse)) a HFalse
A (F FNot) HFalse HTrue
A (F FNot) HTrue HFalse	by case analysis:

data Zero Source

Constructors

Zero

Instances

Show Zero
Nat Zero
E Zero Zero
A (F (Prop', f)) Zero Bool
A (F (FSum', self, Zero)) m m
A (F (Ntimes, f, x)) Zero x
A (F (Fib', self)) Zero (Su Zero)
A (F (Fib', self)) (Su Zero) (Su Zero)

data Su a Source

Constructors

Su a

Instances

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)

data F x Source

Indicator for functions, or applicable things:

Instances

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

Instances

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)

data FNot Source

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

Instances

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

data FAnd Source

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

Instances

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 FAnd) x (F (FAnd, x))	Applying And to an argument makes a closure, waiting for the second argument.

data f :< x Source

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:

Instances

(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

class E a b | a -> bSource

and the big-step evaluation function:

Instances

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:

data Rec l Source

We introduce the applicative fixpoint combinator

Instances

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

data FSum' Source

and define the sum of two numerals

At the type level, this looks as follows

Instances

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

type FSum = Rec (F FSum')Source

now we tie up the knot

type N0 = Zero Source

type N1 = Su N0 Source

type N2 = Su N1 Source

type N3 = Su N2 Source

test_sum :: E ((F FSum :< x) :< y) r => x -> y -> rSource

data Fib' Source

Finally, the standard test -- Fibonacci

Instances

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

type Fib = Rec (F Fib')Source

test_fib :: E (F Fib :< n) r => n -> rSource

data CombK Source

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

Instances

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

data CombS Source

Instances

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

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

A few examples: SKK as the identity

type CombZ = F CombS :< F CombK Source

and the representation of numerals in the SK calculus. The expression (F FSum :< Su Zero) is a partial application of the function sum to 1.

type CombSu = F CombS :< ((F CombS :< (F CombK :< F CombS)) :< F CombK)Source

type CombTwo = CombSu :< (CombSu :< CombZ)Source

test_ctwo :: E ((CombTwo :< (F FSum :< Su Zero)) :< Zero) r => rSource

class Nat a whereSource

Methods

fromNat :: a -> Integer Source

Instances

Nat Zero
Nat x => Nat (Su x)