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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe