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