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

It's probably not what you think. :)

Jay and I just submitted a paper to FLOPS (conditionally accepted) that 
defines an untyped lambda calculus, lambda-ZFC, that contains a model of 
set theory and primitive set operations. The basic idea is to "port" 
constructions from contemporary math into lambda-ZFC, then gradually 
change the computable ones until they can be implemented. It's an 
intermediate language between set-theoretic math and functional 
languages - necessary because set theory sucks for writing algorithms, 
and because there's not a good lambda calculus for writing set theory.

As an example, the paper defines a monad that calculates exact real 
limits, then derives a computable replacement for it. Certain lambda-ZFC 
programs that use the uncomputable `bind' can be changed to use the 
computable `bind' - programs that meet certain proof obligations. We 
used it to write a 13-line program in Racket that computes pi to 
arbitrary accuracy.

(Huh. I could probably fit it in a tweet.)

ANYWAY... I started using Redex to define a type system for lambda-ZFC. 
Then I figured out that TR could let me prototype it easily first. So 
I've been writing typed lambda-ZFC test cases in TR. The primitives - 
powerset, union, replacement, cardinality, etc. - just raise errors, but 
the programs themselves really do define heady stuff like the cumulative 
hierarchy, closure operators and beth cardinals.

It would be fun to try to port Coq's constructive ordinals to phantom 
types in TR, though, to see how far I could get with occurrence typing 
instead of dependent typing.

Neil ⊥

On 02/22/2012 06:50 PM, Matthias Felleisen wrote:
>
> 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
>