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

Sorry, I don't follow. I can't give r1 a monomorphic type (unless I'm
going to give it a polymorphic alias, like I did in the working
example above), since the return type has to be polymorphic.  I'm
probably misunderstanding your suggestion.

-Jon