On 02/22/2012 05: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))
Turns out this wasn't enough to solve my problem in general, because
this function always returns the same type. Here's a simple one that
doesn't:
(: set-id (All (a) ((Set a) -> (Set a))))
(define (set-id A) A)
(: set-id* (All (a) ((Set* a) -> (Set* a))))
(define (set-id* A)
((inst set-id (U a (Set* a))) A))
Using `inst' makes the argument type pass, but I get an error on the
return type:
Expected (Rec T (U Empty-Set
(Opaque-Set (U a T))))
but got (U Empty-Set
(Opaque-Set (U a (Rec T (U Empty-Set
(Opaque-Set (U a T)))))))
I've formatted it so that it's easy to see that the body type is just an
unfold of the expected type. Is there a way to make TR realize that
they're isomorphic?
Neil ⊥
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
