[racket-dev] Unfolding twice?

From: Neil Toronto (neil.toronto at gmail.com)
Date: Fri Aug 10 12:33:01 EDT 2012

Using typed `flatten' takes too much manual instantiation. In the 
following program, the first three uses fail to typecheck; the last passes.

#lang typed/racket

(define-type (Treeof A) (Rec T (U A (Listof T))))

(: flatten (All (A) ((Treeof A) (Any -> Boolean : A) -> (Listof A))))
(define (flatten lst pred?)
   (error 'unimplemented))

(define ws (flatten (sequence->list (in-range -1.4 1.400001 0.2))
(define xs ((inst flatten Float)
             (sequence->list (in-range -1.4 1.400001 0.2))
(define ys (flatten ((inst sequence->list Float)
                      (in-range -1.4 1.400001 0.2))
(define zs ((inst flatten Float)
             ((inst sequence->list Float)
              (in-range -1.4 1.400001 0.2))

I think the problem is that TR only unfolds the type of (Treeof A) once. 
If I manually unfold it once; i.e., I change it to this:

   (define-type (Treeof A) (U A (Listof (Rec T (U A (Listof T))))))

then the program passes, because TR now unfolds it twice.

Would it be feasible to have TR, when something with recursive types 
fails to typecheck, calculate an upper bound on the number of unfolds, 
unfold that many times, and try again?

Neil ⊥

Posted on the dev mailing list.