I'm trying to write some code to do folds on nested datatypes as in http://web.comlab.ox.ac.uk/people/Jeremy.Gibbons/publications/efolds.pdf but running into trouble getting things to typecheck. Given the types data Nest a = Nil | Cons(a, (Nest (Pair a))) type Pair a = (a,a) and the following function to map over pairs: pair f (a,b) = (f a, f b) the paper indicates that an efficient fold over a nest is defined as follows efold :: forall n m b. (forall a. n a) -> (forall a . (m a, n (Pair a)) -> n a) -> (forall a. Pair (m a) -> m (Pair a)) -> (forall l z. (l b -> m (z b)) -> Nest (l b) -> n (z b)) 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) However, when I try to compile this, I get the error "Couldn't match expected type `l' against inferred type `z'". I'm new to Haskell so I'm probably missing something obvious, but this code looks to me like it ought to work. Any thoughts on what I'm doing wrong? Thanks, Keith
On Fri, Apr 24, 2009 at 06:52:09PM +0000, Keith Battocchi wrote:
I'm trying to write some code to do folds on nested datatypes as in http://web.comlab.ox.ac.uk/people/Jeremy.Gibbons/publications/efolds.pdf but running into trouble getting things to typecheck.
Given the types
data Nest a = Nil | Cons(a, (Nest (Pair a))) type Pair a = (a,a)
and the following function to map over pairs:
pair f (a,b) = (f a, f b)
the paper indicates that an efficient fold over a nest is defined as follows
efold :: forall n m b. (forall a. n a) -> (forall a . (m a, n (Pair a)) -> n a) -> (forall a. Pair (m a) -> m (Pair a)) -> (forall l z. (l b -> m (z b)) -> Nest (l b) -> n (z b)) 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)
However, when I try to compile this, I get the error "Couldn't match expected type `l' against inferred type `z'". I'm new to Haskell so I'm probably missing something obvious, but this code looks to me like it ought to work. Any thoughts on what I'm doing wrong?
Well, I'm pretty sure you're not 'missing something obvious'! I stared at this code for fifteen minutes and can't really figure out what's going on. If you change the 'z's in the type signature to 'l's, it type checks, but that may make the function slightly less general than intended. -Brent
Keith Battocchi wrote:
data Nest a = Nil | Cons(a, (Nest (Pair a))) type Pair a = (a,a)
pair f (a,b) = (f a, f b)
efold :: forall n m b. (forall a. n a) -> (forall a . (m a, n (Pair a)) -> n a) -> (forall a. Pair (m a) -> m (Pair a)) -> (forall l z. (l b -> m (z b)) -> Nest (l b) -> n (z b)) 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)
If the problem is just understanding the type error, it may help to manually check the types. You only need to look at the second branch of the function definition, since this is the case that generates the error.
From the pattern-match, you get the type of xs:
xs :: Nest (Pair (l b)) -- (1) Combining the type of f with the result type of the efold definition, you get the type of the result of the recursive call: efold e f g (g . pair h) xs :: n (Pair (z b)) -- (2) This function makes use of polymorphic recursion. To analyse the type of the recursive call, you need a fresh batch of type variables, so you can distinguish the types of the arguments to the recursive call from the types of the formal parameters of the function definition. Since the first three arguments to the recursive call are unchanged, you only need fresh variables for b, l and z. I'll use primed versions of these variables: efold e f g :: (l' b' -> m (z' b')) -> Nest (l' b') -> n (z' b') -- (3)
From (3), you get an alternative view of the type of xs:
xs :: Nest (l' b') -- (4) You can now perform unification on these results. You need to be careful unifying with Pair types, since (Pair a) is really ((,) a a). Unifying (1) and (4), you get: 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.
I'm no expert in nested data types, but I doubt there is any additional generality to be had from trying to distinguish l and z. In that case, you can write both "l b" and "z b" as "a". You can also remove a superfluous tuple from the type definition: data Nest a = Nil | Cons a (Nest (Pair a)) type Pair a = (a,a) 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. Regards, Matthew
Matthew Brecknell
[...] 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
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
participants (3)
-
Brent Yorgey -
Keith Battocchi -
Matthew Brecknell