-- -- | -- <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 :<). -- {-# LANGUAGE TypeOperators, ScopedTypeVariables, EmptyDataDecls, Rank2Types #-} {-# LANGUAGE FlexibleContexts, FlexibleInstances, ScopedTypeVariables #-} {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} module Language.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) -- | now we tie up the knot type FSum = Rec (F FSum') -- 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" class Nat a where fromNat :: a -> Integer instance Nat Zero where fromNat _ = 0 instance Nat x => Nat (Su x) where fromNat _ = succ (fromNat (undefined::x)) instance Show Zero where show _ = "N0" instance Nat x => Show (Su x) where show x = "N" ++ (show (fromNat x))