Polymorphic Recursion / Rank-2 Confusion
Can anyone tell me why the following doesn't work (and what I have to do to fix it)? I thought by specifying the type of coalw as rank-2 would allow it to be used both at a and (a,b). Dominic. Reading file "Test.hs":tten Type checking ERROR "Test.hs":18 - Inferred type is not general enough *** Expression : \(w1,w2) -> coalw w1 ++ coalw w2 *** Expected type : a -> [b] *** Inferred type : (a,b) -> [c] data Vector_ v w = Zero v | Even (Vector_ v (w,w)) | Odd (Vector_ (v,w) (w,w)) deriving Show vzero = Zero () vone = Odd (Zero ((),'a')) vtwo = Even (Odd (Zero ((),('a','b')))) vthree = Odd (Odd (Zero (((),'a'),('b','c')))) vfour = Even (Even (Odd (Zero ((),(('a','b'),('c','d')))))) coal_ :: (forall a b. a -> [b]) -> (forall c d. c -> [d]) -> Vector_ v w -> [w] coal_ coalv coalw (Zero v) = coalv v coal_ coalv coalw (Even v) = coal_ coalv (\(w1,w2) -> (coalw w1) ++ (coalw w2)) v coal_ coalv coalw (Odd v) = coal_ (\(v,w) -> (coalv v) ++ (coalw w)) (\(w1,w2) -> (coalw w1) ++ (coalw w2)) v
On zaterdag, sep 20, 2003, at 13:01 Europe/Amsterdam, Dominic Steinitz wrote:
Can anyone tell me why the following doesn't work (and what I have to do to fix it)? I thought by specifying the type of coalw as rank-2 would allow it to be used both at a and (a,b).
This will never work. A function expecting a value of type forall c d. c -> [d] needs to be passed a function which can turn an arbitrary value of an arbitrary type into a list of values of every other, arbitrary type; the only such (total) function I can think of is const []. The type checker is complaining because the value you pass it is a function which only accepts tuple inputs; it has to work for _all_ inputs of any type. If you explain what you're trying to do here, maybe someone can suggest a solution. Regards, Frank
On Sat, Sep 20, 2003 at 12:01:32PM +0100, Dominic Steinitz wrote:
Can anyone tell me why the following doesn't work (and what I have to do to fix it)? I thought by specifying the type of coalw as rank-2 would allow it to be used both at a and (a,b).
Change the signature to coal_ :: (v -> [a]) -> (w -> [a]) -> Vector_ v w -> [a] Then you can define type Vector = Vector_ () coal :: Vector a -> [a] coal = coal_ (const []) (:[])
On Sat, 20 Sep 2003, Ross Paterson wrote:
On Sat, Sep 20, 2003 at 12:01:32PM +0100, Dominic Steinitz wrote:
Can anyone tell me why the following doesn't work (and what I have to do to fix it)? I thought by specifying the type of coalw as rank-2 would allow it to be used both at a and (a,b).
Change the signature to
coal_ :: (v -> [a]) -> (w -> [a]) -> Vector_ v w -> [a]
Then you can define
type Vector = Vector_ ()
coal :: Vector a -> [a] coal = coal_ (const []) (:[]) _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Ross, Thanks very much. I was going to use coal :: Vector a -> [a] coal = coal_ (\() -> []) (\x -> [x]) but I prefer your definitions. Dominic. ----- Original Message ----- From: "Ross Paterson" <ross@soi.city.ac.uk> To: "Dominic Steinitz" <dominic.steinitz@blueyonder.co.uk> Cc: <haskell@haskell.org> Sent: Saturday, September 20, 2003 5:19 PM Subject: Re: Polymorphic Recursion / Rank-2 Confusion
On Sat, Sep 20, 2003 at 12:01:32PM +0100, Dominic Steinitz wrote:
Can anyone tell me why the following doesn't work (and what I have to do to fix it)? I thought by specifying the type of coalw as rank-2 would allow it to be used both at a and (a,b).
Change the signature to
coal_ :: (v -> [a]) -> (w -> [a]) -> Vector_ v w -> [a]
Then you can define
type Vector = Vector_ ()
coal :: Vector a -> [a] coal = coal_ (const []) (:[])
Sorry about the empty message. Send /= Cancel
Can anyone tell me why the following doesn't work (and what I have to do to fix it)? I thought by specifying the type of coalw as rank-2 would allow it to be used both at a and (a,b).
Frank explained why the type you gave wouldn't work. I would like to add that your function would type check without the type signature. This suggests something here is actively confusing. Do you have any idea what caused this problem? I hope to help teach Haskell to first year students, so I'm trying to figure out what parts of the language are hard to get, and how to usefull explain things. Anything in pure H98 that trips up an experienced programmer is worth some attention. Completely unrelated, I think Zero and One would be better names than Even and Odd because then the string of constructors writes the size of the vector in binary, LSB first. I can't see any mnenomic value to Even and Odd. How do you interpret Even and Odd? Thanks Brandon
Brandon, I get the error below without the type signature. My confusion was thinking I needed rank-2 types. In fact I only need polymorphic recursion. Ross Paterson's suggestion fixes the problem. I stole Even and Odd from Chris Okasaki's paper on square matrices. They relate to fast exponentation algorithm. There's something to be said for Zeror and One; as you say they give the structure in binary. My motivation in using this type was to see if, for example, I could restrict addition of a vector to another vector to vectors of the same length. This would be helpful in the crypto library where I end up having to either define new length Words all the time or using lists and losing the capability of ensuring I am manipulating lists of the same length. Dominic. hugs Type checking ERROR "Test1.hs":23 - Type error in function binding *** Term : coal_ *** Type : (a -> b) -> (c -> [d]) -> Vector_ a e -> b *** Does not match : (a -> b) -> ((c,c) -> [d]) -> Vector_ a (e,e) -> b *** Because : unification would give infinite type ghci Test1.hs:25: Occurs check: cannot construct the infinite type: t = (t, t1) Expected type: (t, t1) Inferred type: t In the first argument of `coalw', namely `w1' In the first argument of `(++)', namely `(coalw w1)' Failed, modules loaded: none. ----- Original Message ----- From: "Brandon Michael Moore" <brandon@its.caltech.edu> To: "Dominic Steinitz" <dominic.steinitz@blueyonder.co.uk> Cc: <haskell@haskell.org> Sent: Saturday, September 20, 2003 11:19 PM Subject: Re: Polymorphic Recursion / Rank-2 Confusion
Sorry about the empty message. Send /= Cancel
Can anyone tell me why the following doesn't work (and what I have to do to fix it)? I thought by specifying the type of coalw as rank-2 would allow it to be used both at a and (a,b).
Frank explained why the type you gave wouldn't work. I would like to add that your function would type check without the type signature. This suggests something here is actively confusing. Do you have any idea what caused this problem?
I hope to help teach Haskell to first year students, so I'm trying to figure out what parts of the language are hard to get, and how to usefull explain things. Anything in pure H98 that trips up an experienced programmer is worth some attention.
Completely unrelated, I think Zero and One would be better names than Even and Odd because then the string of constructors writes the size of the vector in binary, LSB first. I can't see any mnenomic value to Even and Odd. How do you interpret Even and Odd?
Thanks
Brandon
On Sun, 21 Sep 2003, Dominic Steinitz wrote:
Brandon,
I get the error below without the type signature. My confusion was thinking I needed rank-2 types. In fact I only need polymorphic recursion. Ross Paterson's suggestion fixes the problem. I stole Even and Odd from Chris Okasaki's paper on square matrices. They relate to fast exponentation algorithm. There's something to be said for Zeror and One; as you say they give the structure in binary.
I would guess you knew you needed a forall, but missed the implicit one out front. I'm glad you got this working. I'm surprised this didn't typecheck though. I usually put signatures on top level functions, so I suppose my intuition is more tuned to types that can be checked rather than types that can be inferred. Can anyone tell me what's wrong with the following derivation? join :: (a -> [c]) -> (b -> [c]) -> ((a,b) -> [c]) join f g (x,y) = f x ++ g y collect_ colv colw (Zero v) = colv v collect_ colv colw (Odd v) = collect_ colv (join colw colw) v collect_ colv colv (Even v) = collect_ (join colv colw) (join colw colw) v for the first equation, name the type of collect_ collect_ :: t name the arguments and unify collect_ with the argument types colv :: a colw :: b (Zero v) :: Vector v w t = a -> b -> Vector v w -> d The type of v follows from the data type definition v :: v The body is an application (colv v), so we get a = c -> d, c = v so far we have collect :: (v -> d) -> b -> Vector v w -> d which uses up all the constraints. In the next equation v has type v :: Vector v (w,w) b = (e -> [f]) (from the type of join) for the recursive call to collect, we get constraints like d[(w,w)/w] = d (e->[f])[(w,w)/w] = ((e,e) -> [f]) We can deduce that w is not in the free variables of d or f, and that e = w. Now we have the type collect :: (v -> d) -> (w -> [f]) -> Vector v w -> d In the last equation the use of join lets us deduce that d = [f], giving a final type collect :: (v -> [a]) -> (w -> [a]) -> Vector v w -> [a]. What did I do wrong here? Probably the constraints between unification varaibles. Is there a problem with that sort of reasoning? I think I'm probably expecting some sort of implicit quantification that I haven't really specified.
My motivation in using this type was to see if, for example, I could restrict addition of a vector to another vector to vectors of the same length. This would be helpful in the crypto library where I end up having to either define new length Words all the time or using lists and losing the capability of ensuring I am manipulating lists of the same length.
I've vaugely heard about something called Cryptol that Galois connections wrote, that compiles to Haskell. I don't know about the licensing status though. Brandon
On maandag, sep 22, 2003, at 00:07 Europe/Amsterdam, Brandon Michael Moore wrote:
Can anyone tell me what's wrong with the following derivation?
Without going through your derivation completely, the problem is almost certainly polymorphic recursion. Vector is a nested datatype---its definition calls itself with different type arguments---and so, although collect :: (v -> [a]) -> (w -> [a]) -> Vector v w -> [a] the recursive call to collect in, for example, the second clause, has a different type, namely: collect :: (v -> [a]) -> ((w,w) -> [a]) -> Vector v w -> [a] However, in the absence of an explicit type signature, Haskell will assume that the types of the top-level and recursive occurrences of collect are equal, which they are not, so you'll get a type error. Indeed, the error messages Dominic posted:
ERROR "Test1.hs":23 - Type error in function binding *** Term : coal_ *** Type : (a -> b) -> (c -> [d]) -> Vector_ a e -> b *** Does not match : (a -> b) -> ((c,c) -> [d]) -> Vector_ a (e,e) -> b *** Because : unification would give infinite type
Test1.hs:25: Occurs check: cannot construct the infinite type: t = (t, t1) Expected type: (t, t1) Inferred type: t In the first argument of `coalw', namely `w1' In the first argument of `(++)', namely `(coalw w1)'
corroborate this argument. Or, are you asking instead why it is that type inference does not work for polymorphic-recursive functions? Regards, Frank
participants (4)
-
Brandon Michael Moore -
Dominic Steinitz -
Frank Atanassow -
Ross Paterson