Matthew Brecknell
[...] Nest ((,) (l b) (l b)) ~ Nest (l' b') l' ~ (,) (l b) b' ~ (l b) -- (5)
Unifying (2) and the result type from (3):
n ((,) (z b) (z b)) ~ n (z' b') z' ~ (,) (z b) b' ~ (z b) -- (6)
From (5) and (6), you require: l b ~ z b, and therefore l ~ z, but the "forall l z" in the type signature requires l and z to be independent.
Thanks for explicitly writing out the unification steps; this makes it perfectly clear where things are going wrong. I was hoping to be able to have b' ~ b, l' b' ~ (l b, l b), and z' b' ~ (z b, z b). I guess it makes sense that these types can't be inferred - is there any way to explicitly add signatures somewhere so that these alternate interpretations will be used instead? This would allow l and z to remain independent.
[...] efold :: (forall a. n a) -> (forall a. m a -> n (Pair a) -> n a) -> (forall a. Pair (m a) -> m (Pair a)) -> (a -> m a) -> (Nest a -> n a) efold e f g h Nil = e efold e f g h (Cons x xs) = f (h x) (efold e f g (g . pair h) xs)
For example, to flatten a Nest to a simple list, you can take m to be Id and n to be [], something like this:
nest = Cons 0 (Cons (1,2) (Cons ((3,4),(5,6)) Nil))
newtype Id a = Id a
-- [0,1,2,3,4,5,6] flat_nest = efold [] (\(Id xs) ys -> xs : concatMap (\(p,q) -> [p,q]) ys) (\(Id x, Id y) -> Id (x,y)) Id nest
It's a little unpleasant having to use the Id type like this, but I can't see a way around it. I'd be interested to see an example with a non-trivial m.
It may depend on your notion of trivial, but if you've got a Nest [a] and want to get the sum of the lengths of the lists, you'd want m a to be something like K Int a where K t a = K t Thanks again for your help. Regards, Keith