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

From: Neil Toronto (neil.toronto at gmail.com)
Date: Wed Feb 22 19:11:56 EST 2012

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 ⊥

Posted on the users mailing list.