[Haskell-cafe] Data Types a la Carte - automatic injections (help!)
Kenn Knowles
kenn at kenn.frap.net
Mon Jul 28 23:23:34 EDT 2008
I have a question about Data Types a la Carte
(http://www.cs.nott.ac.uk/~wss/Publications/DataTypesALaCarte.pdf) and
more generally hacking smart coproduct injections into Haskell (all
extensions are fair game).
> {-# LANGUAGE MultiParamTypeClasses,TypeOperators,UndecidableInstances,IncoherentInstances,FlexibleInstances,FlexibleContexts #-}
Here are the definitions from Wouter's paper, which cleverly manage
the instances of (:<:)
> data (f :+: g) a = Inl (f a) | Inr (g a)
> infixr 6 :+:
> instance (Functor f, Functor g) => Functor (f :+: g) where
> fmap f (Inl x) = Inl (fmap f x)
> fmap f (Inr x) = Inr (fmap f x)
> 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 :<: g)) => (:<:) f (h :+: g) where
> inj = Inr . inj
Now in my case, I want to be able to inject an arbitrary coproduct
into a larger one, assuming the components are in the same order, so
it is a subsequence of the larger sum, for example:
> coprodInject1 :: (Functor f, Functor g, Functor h, Functor i) => (f :+: g :+: h) a -> (f :+: g :+: h :+: i) a
> coprodInject1 = inj
> coprodInject2 :: (Functor f, Functor g, Functor h, Functor i) => (f :+: g :+: i) a -> (f :+: g :+: h :+: i) a
> coprodInject2 = inj
> instance (Functor f, Functor g, Functor h, (g :<: h)) => (:<:) (f :+: g) (f :+: h) where
> inj (Inl x) = Inl x
> inj (Inr x) = Inr (inj x)
The above works fine, and maybe I could manipulate my code to only
have injections
of those forms, but I want this next one to work too:
> coprodInject3 :: (Functor f, Functor g, Functor h, Functor i) => (f :+: g :+: i :+: j) a -> (f :+: g :+: h :+: i :+: j) a
> coprodInject3 = inj
It fails because after "passing up" the h in the search, it can either
use the reflexivity rule or decompose the sum on (i :+: j). The full
error is:
Overlapping instances for (i :+: j) :<: (i :+: j)
arising from a use of `inj'
...
Matching instances:
instance [incoherent] (Functor f) => f :<: f
-- Defined at ...
instance [incoherent] (Functor f, Functor g, Functor h, g :<: h) =>
(f :+: g) :<: (f :+: h)
-- Defined at ...
In the expression: inj
In the definition of `coprodInject3': coprodInject3 = inj
What confuses me is that IncoherentInstances is on, but it is still
rejected by GHC 6.8.3 seemingly for being incoherent. I haven't tried
it with any other version. Am I missing something? Any suggestions
or pointers?
More information about the Haskell-Cafe
mailing list