[Haskell-cafe] Wadler's blog post on the expression problem

Ryan Ingram ryani.spam at gmail.com
Thu Feb 28 19:54:21 EST 2008

I was reading Philip Wadler's post regarding the expression problem
and Wouter Swierstra's paper, "Data Types a la Carte".

Philip asks: The instances of the injection function for subtypes are
assymmetric.  Is there a symmetric solution in Haskell?

Here is a solution which works under GHC 6.8.2, heavily inspired by
the HList type computation work, available from

There are three keys to this trick, each of which builds on the previous.
1) TypEq: for any two types a, b, there is an instance for TypEq a b
HTrue if and only if a == b, and there is an instance for TypEq a b
HFalse otherwise.
2) This allows the definition of IsTreeMember which gives HTrue if a
type occurs somewhere within a tree and otherwise HFalse.
3) We can then use IsTreeMember as a predicate to determine whether to
use the left branch or right branch of a (:+:) constructor.

Source code follows:

{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances
-fallow-overlapping-instances #-}
module Expr where

newtype Expr f = In (f (Expr f))

instance Show (f (Expr f)) => Show (Expr f) where
    showsPrec _ (In x) = showParen True (showString "In " . showsPrec 11 x)

out :: Expr f -> f (Expr f)
out (In x) = x

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

instance (Functor f, Functor g) => Functor (f :+: g) where
   fmap h (Inl f) = Inl (fmap h f)
   fmap h (Inr g) = Inr (fmap h g)

class (Functor sub, Functor sup) => (:<:) sub sup where
   inj :: sub a -> sup a

instance TypTree sub sup => (:<:) sub sup where inj = treeInj

data Val e = Val Int deriving Show
data Add e = Add e e deriving Show
data Mul e = Mul e e deriving Show

instance Functor Val where
    fmap f (Val x) = Val x
instance Functor Add where
    fmap f (Add l r) = Add (f l) (f r)
instance Functor Mul where
    fmap f (Mul l r) = Mul (f l) (f r)

foldExpr :: Functor f => (f a -> a) -> Expr f -> a
foldExpr f (In t) = f (fmap (foldExpr f) t)

class Functor f => Eval f where
    evalA :: f Int -> Int

instance Eval Val where
    evalA (Val x) = x
instance Eval Add where
    evalA (Add x y) = x + y
instance Eval Mul where
    evalA (Mul x y) = x * y

instance (Eval f, Eval g) => Eval (f :+: g) where
    evalA (Inl f) = evalA f
    evalA (Inr g) = evalA g

eval :: Eval f => Expr f -> Int
eval expr = foldExpr evalA expr

val :: (Val :<: e) => Int -> Expr e
val x = In $ inj $ Val x

add :: (Add :<: e) => Expr e -> Expr e -> Expr e
add x y = In $ inj $ Add x y

mul :: (Mul :<: e) => Expr e -> Expr e -> Expr e
mul x y = In $ inj $ Mul x y

test :: Expr (Val :+: Add)
test = In (Inr (Add (val 118) (val 1219)))

test2 :: Expr (Add :+: Val)
test2 = val 1

test3 :: Expr ((Add :+: Val) :+: Mul)
test3 = add (mul (val 1) (val 2)) (val 3)

test4 :: Expr (Add :+: (Val :+: Mul))
test4 = add (mul (val 1) (val 2)) (val 3)

-- our typtree selection prefers left injection
test5 :: Expr ((Val :+: Val) :+: (Val :+: Val))
test5 = val 1

-- TypTree.  This is basically the same as (:<:).
-- I kept it a separate class during development.  This also allows the use of
-- additional constraints on (:<:) which improve the error messages
when you try,
-- for example:
--   testBroken :: Expr (Mul :+: Add)
--   testBroken = val 3
class (Functor sub, Functor sup) => TypTree sub sup where
    treeInj :: sub a -> sup a
instance Functor x => TypTree x x where
    treeInj = id

-- The magic all happens here
-- We use "IsTreeMember" to determine if a type is part of a tree with leaves
-- of various types and internal nodes of type (l :+: r).
class IsTreeMember (sub :: * -> *) (sup :: * -> *) b | sub sup -> b

instance TypEq x y b => IsTreeMember x y b
instance (IsTreeMember x l bl, IsTreeMember x r br, TypOr bl br b) =>
IsTreeMember x (l :+: r) b

class (Functor sub, Functor l, Functor r) => TypTree' b sub l r where
    treeInj' :: b -> sub a -> (l :+: r) a

-- We can then use this result to decide whether to select from the
left or the right.
instance (TypTree x l, Functor r) => TypTree' HTrue x l r where
    treeInj' _ = Inl . treeInj
instance (TypTree x r, Functor l) => TypTree' HFalse x l r where
    treeInj' _ = Inr . treeInj

-- Finally, this allows us to select which treeInj' to use based on the
-- type passed in.
instance (IsTreeMember x l b, TypTree' b x l r) => TypTree x (l :+: r) where
    treeInj = treeInj' (undefined :: b)

class TypOr b1 b2 res | b1 b2 -> res
instance TypOr HFalse HFalse HFalse
instance TypOr HFalse HTrue  HTrue
instance TypOr HTrue  HFalse HTrue
instance TypOr HTrue  HTrue  HTrue

-- Type equality, semi-lifted from the hlist paper; this only works in GHC.
-- You can avoid the reliance on GHC6.8 type equality constraints
-- by using TypeCast from the HList library instead.
-- see http://www.okmij.org/ftp/Haskell/types.html#HList
-- for the source of this idea.

data HFalse
data HTrue

class TypEq (x :: * -> *) (y :: * -> *) b | x y -> b
instance TypEq x x HTrue
instance (b ~ HFalse) => TypEq x y b

More information about the Haskell-Cafe mailing list