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

2010/1/28 Carl Eastlund <carl.eastlund at gmail.com>:
> 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.

Oh, right.  Thanks-- I forgot about that.

>
> 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.

Yes, I understand this.

>
> 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.

That's exactly what I tried:

(let: ((r1 : (Parser-Result A T) (p1 tks ncur nmax))) ...)

I also tried to annotate r1 inside the cond branch:

(cond ((Ok? r1) #{r1 : (Parser-Result A T)}) ...)

>
> 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.

Yes, I'm really not confused about this (even if my sloppy terminology
suggests otherwise).

-Jon


>
> --Carl
>