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

From: Jon Zeppieri (zeppieri at gmail.com)
Date: Thu Jan 28 15:27:18 EST 2010

On Thu, Jan 28, 2010 at 2:58 PM, 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
> --Carl

Same error.  I really appreciate the help, though.

I've also tried annotating the inner lambda:

(define: (A T) (|| (p1 : (Parser A T)) (p2 : (Parser A T))) : (Parser A T)
  (lambda: ((tks : (Stream T)) (ncur : Integer) (nmax : Integer))
           (let: ((r1 : (Parser-Result A T) (p1 tks ncur nmax)))
                 (cond ((Ok? r1) #{r1 : (Parser-Result A T)})
                       (else (p2 tks ncur nmax))))))

For this particular function, it's easy just to handle the Fail case
of Parser-Result first, and handle the Ok case in the else clause:

(: || (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 ((Fail? r1) (p2 tks ncur nmax))
            (else r1)))))


Posted on the users mailing list.