Wadler's Blog

I've posted a solution to your question here
 

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.
 

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