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

2010/1/28 Jon Zeppieri <zeppieri at gmail.com>:
> 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))))))
>>>
>>> This fails to typecheck, with the message:
>>> typecheck: Expected (U (Ok A T) Fail), but got #(struct:Ok (Any
>>> (Susp14 (U Stream-Null10 (Stream-Pair12 Any))) Integer Integer)) in:
>>> r1
>>>
>>> ... where the "r1" at the end of the message refers to the body of the
>>> first cond branch.
>>>
>>> Both type variables, A and T, are (it seems) instantiated as Any
>>> inside the branch.  It looks like the application of Ok? forces the
>>> instantiation.  To work around this, I can do:
>>>
>>> (: || (All (A T) ((Parser A T) (Parser A T) -> (Parser A T))))
>>> (define (|| p1 p2)
>>>  (λ (tks ncur nmax)
>>>    (let* ((r1 (p1 tks ncur nmax))
>>>           (cpy r1))
>>>      (cond ((Ok? cpy) r1)
>>>            (else (p2 tks ncur nmax))))))
>>>
>>> ... where, although r1 and cpy are synonyms, Ok? is never applied to
>>> r1, so its type variables are never instantiated. This code
>>> typechecks.
>>>
>>> Is this expected behavior?
>>>
>>> -Jon
>>
>> Jon,
>>
>> Try giving the binding of r1 an explicit type annotation in the
>> original version of the program (using the #{r1 : type} syntax).
>> Typed Scheme might need a little extra help in figuring out how to
>> instantiate its type.
>>
>> --Carl
>>
>
> I've tried.  If I annotate r1 at the point where it's bound, that's
> too early.  The type system doesn't consider r1's type variables
> instantiated outside of the cond body expression.  And if I try to
> annotate within the body expression, that's too late; it's an invalid
> universalization.
>
> -Jon

Hmm.  I didn't mean for you to give it a polymorphic type; I meant for
you to give it a type in terms of unquantified A and T.  The question
is whether Typed Scheme understands the body of the function is in
scope of A and T from the forall-type of the entire function.

--Carl