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

From: Sam Tobin-Hochstadt (samth at ccs.neu.edu)
Date: Thu Jan 28 15:04:57 EST 2010

On Thu, Jan 28, 2010 at 11:58 AM, Carl Eastlund <carl.eastlund at gmail.com> wrote:
> 2010/1/28 Jon Zeppieri <zeppieri at gmail.com>:
>> 2010/1/28 Carl Eastlund <carl.eastlund at gmail.com>:
>>> 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)}) ...)
> Ah ha!  I think I found what you need.  Use either:
> (define: [A T] (|| [p1 : (Parser A T)] [p2 : (Parser A T)]) : (Parser A T)
>  <BODY>)
> ...or:
> (: || (All [A T] ((Parser A T) (Parser A T) -> (Parser A T)))
> (define ||
>  (plambda: [A T] ([p1 : (Parser A T)] [p1 : (Parser A T)])
>    <BODY>))
> The plambda: form and the define: variant with the variables up front
> both bind polymorphic type that are available in the input types,
> result type, and in the body of the function.  Use those, and you
> should be able to give a type to r1 in terms of A and T.  You can find
> both define: and plambda: in the Typed Scheme reference:
> http://docs.plt-scheme.org/ts-reference/index.html

This points to a bug in Typed Scheme - those type variables should be
bound in the body in the original defintion with the use of `:'.

sam th
samth at ccs.neu.edu

Posted on the users mailing list.