[racket] Polymorphic occurrence typing

Could Typed Racket generate more fine grained predicates in a
type-directed fashion to allow this sort of thing?

Jay

On Fri, Aug 13, 2010 at 8:32 AM, Sam Tobin-Hochstadt <samth at ccs.neu.edu> wrote:
> 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
> _________________________________________________
>  For list-related administrative tasks:
>  http://lists.racket-lang.org/listinfo/users
>



-- 
Jay McCarthy <jay at cs.byu.edu>
Assistant Professor / Brigham Young University
http://teammccarthy.org/jay

"The glory of God is Intelligence" - D&C 93