[Haskell-cafe] Re: Typing efficient folds

[Matthew Brecknell]

Keith Battocchi wrote: 
> 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.

The unification matches type constructors from the outside towards the
inside. Since the polymorphic recursion adds a Pair constructor at the
outside, you're left with an l/z discrepancy on the inside.

I had a look at the paper you referred to, and I think there must be an
typographical error in the definition you are looking at (page 5). If
you look at the fold for the Collection data-type at the top of page 15,
you'll see how to correct it.

> 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

Ok, that makes sense. My main gripe with my example was having to write
what amounts to an identity function for g:

\(Id x, Id y) -> Id (x,y)

In your example, g actually does something interesting:

\(K m, K n) -> K (m + n)

Regards,
Matthew