# [racket] Polymorphic occurrence typing

On Thu, Aug 12, 2010 at 4:11 PM, Neil Toronto <neil.toronto at gmail.com> wrote:
>* Are there any plans for it? Would it be difficult to do? I ask because it
*>* seems it would make using polymorphic struct subtypes easier. Here's an
*>* example of the problem:
*>*
*>*
*>* #lang typed/racket
*>*
*>* (struct: (T) datum ([val : T]))
*>* (struct: (T) data datum ([vals : (Listof T)]))
*>*
*>* (: get-vals (All (T) ((datum T) -> (Listof T))))
*>* ;; Returns the values in the struct as a list
*>* (define (get-vals d)
*>* ; type error here:
*>* (cond [(data? d) (cons (datum-val d) (data-vals d))]
*>* [(datum? d) (list (datum-val d))]))
*>*
*>* (get-vals (data 1 '(2 3 4)))
*>*
*>* #|
*>* Type Checker: Polymorphic function cons could not be applied to arguments:
*>* Types: a (Listof a) -> (Listof a)
*>* a b -> (Pairof a b)
*>* Arguments: Nothing (Listof Any)
*>* Expected result: (Listof T)
*>* in: (cons (datum-val d) (data-vals d))
*>* |#
*>*
*>*
*>* The problem is the type of data?, which is (Any -> Boolean : (data Any)), so
*>* in the first branch above, d has type (data Any) instead of (data T). But if
*>* data? : (All (S) (Any -> Boolean : (data S))), it seems I could make this
*>* function work, even if I had to annotate data? with (Any -> Boolean : (data
*>* T)) to use it.
*
Unfortunately, that isn't the semantics of the underlying struct
predicate - there's no way to ask Racket to "specialize" struct
predicates to a particular type. The Typed Racket type corresponds to
what the `data?' predicate that the `struct' form defines.
--
sam th
samth at ccs.neu.edu