[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