### 28.2.08

## Data Types a la Carte

Wouter Swierstra. Data Type a la Carte. Functional Pearl, accepted to Journal of functional programming.

Presents the best solution to the Expression Problem that I've seen in Haskell (well, Haskell with -fglasgow-exts).

There is one unfortunate feature. The instances of the injection function for subtypes are assymmetric:

It would be better to replace the left instance by one symmetric with the right:

But Haskell, alas, cannot support this (even with -fglasgow-exts). Is there a symmetric solution in Haskell?

Presents the best solution to the Expression Problem that I've seen in Haskell (well, Haskell with -fglasgow-exts).

There is one unfortunate feature. The instances of the injection function for subtypes are assymmetric:

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

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

inj :: sub a -> sup a

instance Functor f => (:<:) f f where

inj = id

instance (Functor f, Functor g) => (:<:) f (f :+: g) where

inj = Inl

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

inj = Inr . inj

It would be better to replace the left instance by one symmetric with the right:

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

inj = Inl . inj

But Haskell, alas, cannot support this (even with -fglasgow-exts). Is there a symmetric solution in Haskell?

Comments:

<< Home

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.

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'))

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

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.

Post a Comment
<< Home