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 present 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 (it could well run in Hugs; alas, Hugs does not like infix type constructors like :<).

{-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-}

module TypeLC where

First we define some constants

data HTrue = HTrue data HFalse = HFalse

data Zero = Zero data Su a = Su a

Indicator for functions, or applicable things:

data F x

and the applicator

class A l a b | l a -> b

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

data FNot

by case analysis:

instance A (F FNot) HTrue HFalse instance A (F FNot) HFalse HTrue

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

data FAnd

Applying And to an argument makes a closure, waiting for the second argument.

instance A (F FAnd) x (F (FAnd,x))

When we receive the second argument, we are in the position to produce the result. Again, we use the case analysis.

instance A (F (FAnd,HTrue)) a a instance A (F (FAnd,HFalse)) a HFalse

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:

data f :< x infixl 1 :<

and the big-step evaluation function:

class E a b | a -> b

Constants evaluate to themselves

instance E HTrue HTrue instance E HFalse HFalse instance E Zero Zero

Abstractions are values and so evaluate to themselves

instance E (F x) (F x)

Familiar rules for applications

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

Other particular rules

instance E x x' => E (Su x) (Su x')

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:

type Testb x = E (F FAnd :< (F FNot :< x) :< (F FNot :< (F FNot :< x))) r => r testb1_t = undefined :: Testb HTrue testb1_f = undefined :: Testb HFalse

We introduce the applicative fixpoint combinator

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

and define the sum of two numerals

fix f = f (fix f) vsum = fix (\self n m -> case n of 0 -> m (n+1) -> 1 + (self n m))

At the type level, this looks as follows

data FSum' -- first define the non-recursive function

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

type FSum = Rec (F FSum') -- now we tie up the knot

After we define a few sample numerals, we can add them

type N0 = Zero; type N1 = Su N0; type N2 = Su N1; type N3 = Su N2 (n0 :: N0, n1::N1, n2::N2, n3::N3) = undefined

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

test_sum_2_3 = test_sum n2 n3

*TypeLC> :t test_sum_2_3 test_sum_2_3 :: Su (Su (Su (Su (Su Zero)))) Finally, the standard test -- Fibonacci

vfib = fix(\self n -> case n of 0 -> 1 1 -> 1 (n+2) -> (self n) + (self (n+1)))

data Fib'

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

type Fib = Rec (F Fib') test_fib :: E (F Fib :< n) r => n -> r test_fib = undefined

test_fib_5 = test_fib (test_sum n3 n2)

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

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

data CombS 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

A few examples: SKK as the identity

type Test_skk x = E (F CombS :< F CombK :< F CombK :< x) r => r test_skk1 = undefined:: Test_skk HTrue

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 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 test_ctwo = undefined

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.

instance Show HTrue where show _ = "HTrue" instance Show HFalse where show _ = "HFalse" instance Show Zero where show _ = "N0" instance Show x => Show (Su x) where show _ = "N" ++ (show (x+1)) where ('N':xs) = show (undefined::x) x = (read xs)