I've been experimenting with type level programming and open recursion. My aim this far is to implement very modular interpreter for lambda calculi and combinatory logic powerful enough to demonstrate steps of some term's reduction to normal form. I'd like to be able to setup the set of combinators and reduction rules and to express the set in type signature. I'd like to achieve maximum modularity of the code by all possible means. Below is the beginning of this effort. Show instances are defined completely modular. Show instance for Lambda and show instance for Combinator reuse the very same code of Show instance of ApplicativeF. However, there are problems with this code, and I'd like to receive some suggestions to cope with them. 1) UndecidableInstances are required for this code to compile. Is it possible to avoid this language extension? What is the reason for it to be required? 2) app, var, abs functions. app function is defined differently for every example. Is it possible to perform some automatic lifting so that app will work for any combination of ApplicativeF? Can I use Functor class or should I define my own type-class for this purpose? Is it possible at all? 3) The code below uses technique similar to Data Type a la Carte. Is it possible to achieve the same modularity using Finally Tagless technique?
{-# LANGUAGE TypeOperators #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-}
Some type level combinators first
newtype (:.) f g a = O (unO :: f (g a)) newtype (:<*>) f g a = S {unS :: f a (g a)} newtype Flip f x y = Flip {unFlip :: f y x} newtype Mu f = Mu {unMu :: f (Mu f)}
Their show instances doesn't affect representation of underlying type
instance Show (f (Mu f)) => Show (Mu f) where showsPrec d (Mu f) = showsPrec d f instance Show (f (g a)) => Show ((f :. g) a) where showsPrec d (O f) = showsPrec d f instance Show (f a (g a)) => Show ((f :<*> g) a) where showsPrec d (S f) = showsPrec d f instance Show (f y x) => Show (Flip f x y) where showsPrec d (Flip f) = showsPrec d f
Applicative is some structure that permits application of some objects. We use open recursion here. ApplicativeF o is a functor that represent this structure. And Mu (Flip ApplicativeF o) is a fix-point of this functor.
data ApplicativeF a o = App a a | Obj o type Applicative o = Mu (Flip ApplicativeF o)
Pareses are left associative in applicative structure
instance (Show o, Show a) => Show (ApplicativeF o a) where showsPrec d (Obj o) = showsPrec d o showsPrec d (App a b) = showParen (d > 4) $ showsPrec 4 a . (' ':) . showsPrec 5 b
Here is an example of applicative structure of strings
test1 :: Applicative String test1 = obj "x" `app` obj "y" `app` obj "z" `app` (obj "w" `app` obj "v") where obj = Mu . Obj app a b = Mu $ App a b
Lambda calculi is a calculi of some objects with applicative structure. This object may represent a variable or an abstraction of variable. LambdaObjF encodes this fact. We use all combinators defined above to define objects of lambda calculi.
data LambdaObjF name a = Var Name | Abs Name a type Lambda name = Mu (ApplicativeF :<*> LambdaObjF name)
instance (Show a) => Show (LambdaObjF String a) where showsPrec d (Var s) = showParen (d > 5) (showString s) showsPrec d (Abs s a) = showParen (d > 3) $ ('\\':) . showString s . showString ". " . showsPrec 3 a
Lets try to build an object of lambda calculi
type Name = String
test2 :: Lambda Name -- test2 = (\x. \y. x) a b test2 = (abs "x" (abs "y" (var "x")) `app` var "a") `app` var "b" where var = Mu . S . Flip . Obj . Var abs x b = Mu . S . Flip . Obj $ Abs x b app a b = Mu . S . Flip $ App a b
Combinatory logic defines some basic combinators
data CombinatorObjF a = CK | CS type Cominator = Mu (ApplicativeF :<*> CombinatorObjF)
instance Show (CombinatorObjF a) where showsPrec d CK = showString "K" showsPrec d CS = showString "S"
test3 = s `app` k `app` k `app` (k `app` s) where s = Mu . S . Flip . Obj $ CS k = Mu . S . Flip . Obj $ CK app a b = Mu . S . Flip $ App a b
-- Victor Nazarov