[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