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

One essential trait of Typed Scheme is to accommodate 'occurrence  
typing' where occurrences of variables are assigned a type that  
combines the declared type with the type-like predicates that dominate  
the control flow to this occurrence.

Since Ok? appears to be such a predicate (a structure predicate), this  
is exactly what you want from Typed Scheme.


On Jan 28, 2010, at 12:28 PM, Jon Zeppieri wrote:

> 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
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme