[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
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
More information about the Haskell-Cafe
mailing list