[racket] Typed Racket Predicate Generation Regression?

On 10/30/2012 01:24 PM, Danny Yoo wrote:
> On Tue, Oct 30, 2012 at 1:10 PM, Ray Racine <ray.racine at gmail.com> wrote:
>> Been awhile as this is old library code, but I recall the below code once
>> worked for me.  Currently failing at the moment, though may have broken at
>> any time of the last few months.
>
> Hmmmm!  This seems to be triggering based on HashTable being there.  A
> reduced case also fails:
>
>      #lang typed/racket/base
>      (define-predicate myhash? (HashTable Symbol String))
>
> with the following error message:
>
> ---
>
> Type Checker: Type (HashTable Symbol String) could not be converted to
> a contract. in: (HashTable Symbol String)

You'll have that problem with every mutable container type, for a good 
reason. Let's say we can do it. Write an erroneous predicate:

   (define-predicate boxof-integer? (Boxof Integer))

Now write some code using it:

   (define: bx : (Boxof Any)  (box 4))

   (cond [(boxof-integer? bx)
          (define n (unbox bx))
          ...]
         [else
          ...])

Obviously, the type of `n' is Integer. But what can its runtime value 
be? What if there were a parallel thread changing its contents? What if, 
in the first "...", you called a thunk with `bx' in its closure that 
happened to change its contents to (list 4)?

We'd suddenly lose one of the main properties we rely on from a type 
system: preservation. Preservation says that, if the type system proves 
an expression has a certain type, its runtime value will have that type.

Unfortunately, the HashTable type doesn't correctly describe the 
behavior of *immutable* hashes. I've made a suggestion to the TR Lords 
about this, and they're considering it. (It would allow you to declare 
that a function doesn't mutate its possibly mutable arguments.) They may 
do something cooler. But its obvious that something needs to be done.

Until that happens, use immutable types as much as possible. I'd also 
try putting a functional wrapper around HashTable, but I'm not 
optimistic about that one.

Neil ⊥