So are you going to reconstruct all of set theory in TR, including ordinals up to epsilon0 and cardinals below aleph-something?
On Feb 22, 2012, at 7: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)) > > 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 ____________________ Racket Users list: http://lists.racket-lang.org/users
