[racket] Polymorphic occurrence typing

From: Neil Toronto (neil.toronto at gmail.com)
Date: Thu Aug 12 16:11:13 EDT 2010

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.

BTW, shouldn't the first argument type to cons be Any instead of Nothing?

Neil T


Posted on the users mailing list.