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

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?

Neil ⊥

> On Wed, Feb 22, 2012 at 7:11 PM, Neil Toronto<neil.toronto at gmail.com>  wrote:
>> I'd like to use the same functions to operate on both "flat" container types
>> and arbitrarily nested container types. More precisely, I want a type for
>> `Set*' that allows this program otherwise unchanged:
>>
>>
>> #lang typed/racket
>>
>> (struct: Empty-Set ())
>> (struct: (a) Opaque-Set ([error-thunk : (->  a)]))   ; Phantom type
>>
>> (define-type (Set a) (U Empty-Set (Opaque-Set a)))  ; Flat sets
>> (define-type (Set* a) (Rec T (Set (U a T))))        ; Nested sets
>>
>> ;; Type of "pure" sets, currently doing double-duty for cardinals:
>> (define-type Hereditary-Set (Set* Nothing))
>>
>> ;; Cardinality operator
>> (: card (All (a) ((Set a) ->  Hereditary-Set)))
>> (define (card A) (error 'card "unimplementable"))
>>
>> (: card* (All (a) ((Set* a) ->  Hereditary-Set)))
>> (define (card* A)
>>   (card A))  ; checking fails here
>>
>>
>> I think the problem is that a (U a T) isn't a subtype of `a' - it's a
>> supertype. But I can't figure out how to make a recursive type that's a
>> subtype of its corresponding "flat" type.
>>
>> Neil ⊥