[racket] TR Predicates For Mutable Datatypes

On Tue, Nov 6, 2012 at 5:19 PM, Ray Racine <ray.racine at gmail.com> wrote:
> To pick up on a previous topic:
>
> OK given define-predicate doesn't work for mutable datatypes.
>
> (define-predicate T? (HashTable Symbol String)) ;; goes boom
>
> Are we also saying in effect that no possible manual predicate construction
> will be accepted by TR?

No, this can't work.  There's no way to test at one point whether
getting data out of that hash table will always produce a string --
someone with a different reference to the data could add an integer.

> i,e, is there any form of the below one can construct that TR will accept?
>
> (: T? (Any -> Boolean : (HashTable Symbol String)))
> (define (T? ht)
>   ...)

However, in 5.3.1, you can use the `cast` form:

#lang typed/racket
(define: t : (HashTable Any Any) (make-hash))
(define: s : (HashTable Symbol String) (cast t (HashTable Symbol String)))

> (hash-set! t 'x 6)
> (hash-ref s 'x)
. . #hash((x . 6) (5 . 6) (5 . 6)): broke its contract
 promised: String
 produced: 6

Thanks to Eric Dobson for implementing this.
--
sam th
samth at ccs.neu.edu