[Haskell-cafe] Re: Typing efficient folds

[Keith Battocchi]

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

Thanks again for your help.

Regards,
Keith