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 Mul e = Mul e e deriving Show

instance Functor Val where
fmap f (Val x) = Val x
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
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

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.
--