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.
