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 http://www.okmij.org/ftp/Haskell/types.html#HList 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