On 02/23/2012 03:16 PM, Sam Tobin-Hochstadt wrote:
On Thu, Feb 23, 2012 at 1:30 PM, Neil Toronto<neil.toro...@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 ⊥
____________________
Racket Users list:
http://lists.racket-lang.org/users
