# [racket] TR: Making recursive types as subtypes of non-recursive types

On Thu, Feb 23, 2012 at 1:30 PM, Neil Toronto <neil.toronto at gmail.com> wrote:
>* On 02/22/2012 05:35 PM, Sam Tobin-Hochstadt wrote:
*>>*
*>>* You're very close -- you just need to give inference a little more
*>>* help. This definition works:
*>>*
*>>* (: card* (All (a) ((Set* a) -> Hereditary-Set)))
*>>* (define (card* A)
*>>* ((inst card (U a (Set* a))) A))
*>*
*>*
*>* Turns out this wasn't enough to solve my problem in general, because this
*>* function always returns the same type. Here's a simple one that doesn't:
*>*
*>*
*>* (: set-id (All (a) ((Set a) -> (Set a))))
*>* (define (set-id A) A)
*>*
*>* (: set-id* (All (a) ((Set* a) -> (Set* a))))
*>* (define (set-id* A)
*>* ((inst set-id (U a (Set* a))) A))
*>*
*>*
*>* Using `inst' makes the argument type pass, but I get an error on the return
*>* type:
*>*
*>* Expected (Rec T (U Empty-Set
*>* (Opaque-Set (U a T))))
*>*
*>* but got (U Empty-Set
*>* (Opaque-Set (U a (Rec T (U Empty-Set
*>* (Opaque-Set (U a T)))))))
*>*
*>* I've formatted it so that it's easy to see that the body type is just an
*>* unfold of the expected type. Is there a way to make TR realize that they're
*>* isomorphic?
*
That really should work, I'm not sure why it doesn't.
This does work:
(: set-id* (All (a) ((Set* a) -> (Set (U a (Set* a))))))
(define (set-id* A)
((inst set-id (U a (Set* a))) A))
--
sam th
samth at ccs.neu.edu