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 _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
