Polymorphic Recursion / Rank-2 Confusion

[Brandon Michael Moore]

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