Your intuitions about both questions are right here. First, type variables are only introduced into scope automatically in the function body for function definitions. You can use `#:forall` with `define` to use polymorphic types inline, but that does not allow you to define a polymorphic store value.
Second, you're right that subtyping allows `store` to be covariant, meaning that anyone can put additional kinds of things in a store. You can change this so that store is invariant by making the allowed hashtables possible mutable, changing that field to `(HashTable addr \alpha)`. Then your last example won't type check. However, that will mean you need to pick an initial store type, instead of having it inferred, and it will mean that a `(store Integer)` is not usable when you need a `(store Number)`. Sam On Fri, Nov 10, 2017 at 11:10 AM, Richard Cobbe <rco...@pobox.com> wrote: > 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. -- 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.
