[racket] TR: Making recursive types as subtypes of non-recursive types

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.toronto at 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
> samth at ccs.neu.edu
> 
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users