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

From: Jon Zeppieri (zeppieri at gmail.com)
Date: Thu Jan 28 12:28:44 EST 2010

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


Posted on the users mailing list.