I'm getting surprising results trying to define an abstract polymorphic type in Typed Racket. Could someone shed some light on this?
Consider the following definitions: (struct addr ([ptr : Natural])) (struct (α) store ([next-addr : addr] [table : (Immutable-HashTable addr α)])) (: empty-store (All (α) (-> (store α)))) (define (empty-store) (store (addr 0) (make-immutable-hash null))) (: alloc (All (α) (store α) α -> (Values (store α) addr))) (define (alloc st v) (let ([a (store-next-addr st)]) (values (store (inc-addr a) (hash-set (store-table st) a v)) a))) ;; definitions of inc-addr & other store operations elided for brevity I have two questions at this point, a big one and a small one. Small question: it'd be nice to define empty-store to have type (All (α) (store α)) -- i.e., without the eta expansion -- but I can't figure out how to do this. In particular, the following doesn't work: (: empty-store (All (α) (store α))) (define empty-store (store (addr 0) ((inst make-immutable-hash addr α) null))) I get an error that "type name `α' is unbound", referring to the use of α in the use of `inst'. This surprises me, because section 4.8.3 (Lexically Scoped Type Variables) of the Typed Racket Guide seems to say that α should be in scope here. Does that only work for function definitions? Is there another way to do this without the thunk? * * * * * Big question: with the original version of empty-store, I get some very surprising behavior. Consider the following uses: (: s (store String)) (define s ((inst empty-store String))) (define-values (s1 addr) (alloc s 3)) This type-checks -- even the application of `alloc' in the last line. What's going on here? In my understanding of parametric polymorphism, this can't be well-typed: α cannot be both String and Positive-Byte in the same type application. Did I overlook something in the Typed Racket manuals that explains this? After the final definition, `s1' has type (store (U Positive-Byte String)). This does look sound to me, in that the values in the store are indeed either Positive-Bytes or Strings. But this makes it difficult to use the type system to prevent clients from adding non-strings to the store. Is it possible to express that restriction in Typed Racket? (Context: I only actually intend to use `store' with a single type, but I want to define that type in a separate module. Since the type's definition refers to `addr', I made `store' polymorphic to break the cyclical dependency.) Thanks, Richard -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.