Keith Battocchi kbattocchi at gmail.com
Mon Apr 27 15:47:36 EDT 2009

```Matthew Brecknell <haskell <at> brecknell.org> writes:
> [...]
> 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