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)) My brain was injured thinking about those types, though. :) On Wed, Feb 22, 2012 at 7:11 PM, Neil Toronto <neil.toro...@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 ⊥ > ____________________ > Racket Users list: > http://lists.racket-lang.org/users -- sam th sa...@ccs.neu.edu ____________________ Racket Users list: http://lists.racket-lang.org/users
