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