On Thu, Feb 23, 2012 at 1:30 PM, Neil Toronto <neil.toro...@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 sa...@ccs.neu.edu ____________________ Racket Users list: http://lists.racket-lang.org/users
