Wadler's Blog

I've posted a solution to your question here
 

Wouter Swierstra writes (posted with permission):

Regarding the question on your blog about "Data types a la carte": the reason its hard to get a symmetric definition of :<: is that the algorithm Haskell uses to infer which instance definition to use doesn't backtrack - it picks the first instance definition that fits and runs with it. As a result, writing a backtracking search on the type-level becomes a bit tricky. (I just saw an e-mail from Ryan Ingram on haskell-cafe that presents one solution.)

There is a real penalty for this asymmetry, by the way. With the asymmetric definition in the paper, you can't group together certain signatures and combine these pieces into even larger signatures. For example:

Add :<: (Val :+: Add :+: Sub :+: Mul :+: Div)

is fine, but:

Add :<: Val :+: (Add :+: Sub) :+: (Mul :+: Div)

isn't.
 

Oleg Kiselyov sends an alterantive solution, developed independently of Ryan Ingram's (posted with permission):

I'm including the code that solves the problem as described,
although not in a nice way. On the bright side, no overlapping
instances are required. How big the drawback of the solution is
depends on the exactly problem: is your universe of primitive data
types closed (or rarely extensible) or not. It is possible to greatly
improve the solution; for example, our HList paper described how to
define the total order on types (including type constructors). That
makes deciding `subjugation' and arithmetical problem... We can also
use the TypeEq predicates to compare any two types; alas that does
require overlapping instances. Again, given more details I can improve
the solution. The present solution, given all its obvious drawbacks,
has one advantage: simplicity. Hopefully it shows the underlying
ideas.

Cheers,
Oleg

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

module Main where

data (f :+: g) e = Inl (f e) | Inr (g e) deriving Show

newtype HJust a = HJust a
data HNothing a = HNothing

-- We now define predicate, which, given two types f and g, return
-- decides if f :<: g holds -- and if so, yields a witness

class IsSub f g result | f g -> result where
ginj :: result (f a -> g a)

instance IsSub f f HJust where
ginj = HJust id


instance (IsSub f g b, IsSub' b f g h result)
=> IsSub f (g :+: h) result where
ginj = ginj' (ginj :: b (f a -> g a))

class IsSub' b f g h result | b f g h -> result where
ginj' :: b (f a -> g a) -> result (f a -> (g :+: h) a)

instance IsSub' HJust f g h HJust where
ginj' (HJust tr) = HJust (Inl . tr)

instance (IsSub f h b, IsSub'' b f g h result)
=> IsSub' HNothing f g h result where
ginj' _ = ginj'' (ginj :: b (f a -> h a))

class IsSub'' b f g h result | b f g h -> result where
ginj'' :: b (f a -> h a) -> result (f a -> (g :+: h) a)

instance IsSub'' HJust f g h HJust where
ginj'' (HJust tr) = HJust (Inr . tr)

instance IsSub'' HNothing f g h HNothing where
ginj'' _ = HNothing

{- not ok, but what I want to do

instance (Functor f, Functor g, Functor h, (:<:) f g) => (:<:) f (g :+:
h) where
inj = Inl . inj

instance (Functor f, Functor g, Functor h, (:<:) f h) => (:<:) f (g :+:
h) where
inj = Inr . inj

-}

test1 = let (HJust (tr::[Char]->[Char])) = ginj in tr "a" -- "a"

data C a = C a deriving Show

-- need to define the disequalities
-- One may either use Template Haskell for that, or TypeEq from
-- the HList paper
instance IsSub [] Maybe HNothing where ginj = HNothing
instance IsSub Maybe [] HNothing where ginj = HNothing
instance IsSub C [] HNothing where ginj = HNothing
instance IsSub [] C HNothing where ginj = HNothing
instance IsSub C Maybe HNothing where ginj = HNothing
instance IsSub Maybe C HNothing where ginj = HNothing

type Sum1 = ([] :+: Maybe)
type Sum2 = (Sum1 :+: C)
type Sum3 = (C :+: Sum1)

test2 = let (HJust (tr::[Char]->Sum2 Char)) = ginj in tr "a"
-- Inl (Inl "a")
test3 = let (HJust (tr::[Char]->Sum3 Char)) = ginj in tr "a"
-- Inr (Inl "a")
test4 = let (HJust (tr::Maybe Char->Sum3 Char)) = ginj in tr (Just 'a')
-- Inr (Inr (Just 'a'))
 

Dear Philip

There is another solution to the Expression Problem which I find easier to use. I'm not sure it's common lore so I've decided to post some sample code. The idea of representing types as products of functions (rather than sums) is due to Bruno Oliveira. More on his paper "Generics as a Library" and on his PhD thesis. The code below is only a taster. Of course, errors or omissions are my own:

- GADT as a type class (or encode the type as it's fold):

class Exp e where
lit :: TyRange a => a -> e a
plus :: e Int -> e Int -> e Int
and :: e Bool -> e Bool -> e Bool

- We cannot construct an ill-typed expression, the Haskell type-checker complains.

- |TyRange| is the class of indices:

class TyRange a
instance TyRange Int
instance TyRange Bool

- The behaviour is given by instances:

newtype Eval a = Eval {eval :: a}

instance Exp Eval where
lit = Eval
plus x y = Eval (eval x + eval y)
and x y = Eval (eval x && eval y)

Extension is easy:

class Exp e => ExpIf e where
ifOp :: TyRange a => e Bool -> e a -> e a -> e a

instance ExpIf Eval where
ifOp c t e = Eval (if (eval c) then (eval t) else (eval e))

class Exp e => ExpMult e where
mult :: e Int -> e Int -> e Int

instance ExpMult Eval where
mult x y = Eval (eval x * eval y)

- Adding new indices is easy:

instance TyRange a => TyRange [a]
instance TyRange Char

class Exp e => ExpConcat e where
conc :: e [Char] -> e [Char] -> e [Char]

instance ExpConcat Eval where
conc x y = Eval (eval x ++ eval y)

- Closing expressions is also easy: wrap around a type and provide new functions:

data TyRange a => Wrap a = Wrap (forall e. (Exp e, ExpIf e, ExpMult e,
ExpConcat e) => e a)

> evalExp :: TyRange a => Wrap a -> a
> evalExp (Wrap x) = eval x

Compare:

exp1 :: Exp e => e Int
exp1 = plus (lit 3) (lit 3)
val1 = eval exp1

With:

exp1' :: Eval Int
exp1' = plus (lit 3) (lit 3)
va1' = eval exp1

We are limited here to writing only folds, but we can choose to encode expressions using another encoding.

Regards,
Pablo Nogueira
 

Exactly this issue is addressed by a new paper from J. Garrett Morris and Mark Jones, discussed here.