[racket] TR: Making recursive types as subtypes of non-recursive types
On 02/23/2012 03:16 PM, Sam Tobin-Hochstadt wrote:
> On Thu, Feb 23, 2012 at 1:30 PM, Neil Toronto<neil.toronto at gmail.com> wrote:
>> (: 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.
I sent a bug report with a more concrete example:
Would it be useful for TR to expose some of its recursive types
machinery; i.e. provide `Fold' and `Unfold' as type constructors, for
the cases where inference needs that kind of help? For example, I think
this would be cleaner than wrapping `set-id' with `inst':
(define (set-id* A)
(set-id (ann A (Unfold (Set* a)))))
But I don't know whether it would work. :)
Neil ⊥