[plt-scheme] typed-scheme: conditional branches and parametric polymorphism
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