[Haskell-cafe] Data types a la carte

Victor Nazarov asviraspossible at gmail.com
Wed Jul 21 05:25:51 EDT 2010


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


More information about the Haskell-Cafe mailing list