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.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
