[plt-scheme] typed-scheme: conditional branches and parametric polymorphism

2010/1/28 Jon Zeppieri <zeppieri at gmail.com>:
> I'm using typed-scheme in 4.2.3 and running into the following:
>
> (: || (All (A T) ((Parser A T) (Parser A T) -> (Parser A T))))
> (define (|| p1 p2)
>   (λ (tks ncur nmax)
>     (let ((r1 (p1 tks ncur nmax)))
>       (cond ((Ok? r1) r1)
>             (else (p2 tks ncur nmax))))))

First of all, let me point out that the "|" character is special in
Scheme; it is a paired escape character.  The name of your function is
the empty string, but it can be written (and is often printed) as
"||".  Just in case you get a strange error message about a function
with an empty name at some point, it is because your function name is
technically empty.

The return type of your function is (Parser A T).  It only makes sense
once A and T are instantiated, but the return type itself is
monomorphic for each such instatiation.  Similarly, the inputs are of
type (Parser A T) as well.  Inside the body of your function, p1 and
p2 do not have type (All (A T) (Parser A T)).  If they did, that would
mean no matter what parser was given to you, you could instantiate it
at any type you like.  Instead, they have the type (Parser A T) for
whatever A and T were given to you.

Try giving r1 a type in terms of A and T, without wrapping it in (All
(A T) ...).  Tell Typed Scheme what type it is for a given
instantiation, and it will hopefully be able to figure out what your
function is doing a little better.

Reasoning about polymorphism is tricky like this.  It's hard to figure
out exactly when and where the variables are quantified (so they can
be anything) versus instantiated (where they must be one thing, even
though it may be a different thing each time it runs).  But if the
type of a function is (All (A T) (... -> ...)), the A and T must be
instantiated before you actually "have" a function type, so they are
instantiated everywhere within the function.

--Carl