[racket] Typed Racket Predicate Generation Regression?

Orthogonal to the type system any unsynchronized parallel read/write is
unsafe.

if (eq? (unbox bx) 3)
  (let ((b (unbox bx))
        ...

Here assume the type system is not subverted there is a serious lurking
problem nonetheless.  Actually larger, as at least if the parallel process
consistently subverted the type an eventual contract violation with blame
is likely.

I guess I'm trying to say is, in general all Racket code without special
structuring by the programmer is not thread safe.  Unsafe in any manner of
manifestations.  Yes one subset of parallel mutation unsafeness will cause
a type subversion / contract violation.   I can insert a doomed typecast in
any number of languages.  All comes with the territory.

Is Racket planning on some sort of effects type system as well?  Perhaps
allowing mutation only in atomic blocks or STM computations?  Is MR,
Monadic Racket on the roadmap?  All exciting possibilities.

Of course the most basic of mutable containers is the global variable.
Consider (define: x : Any 4) along with an accompanying Byzantine parallel
process whirling away busily set!'ing x to all sorts of fuzzed values.
 Shall the set! construct be banned from TR?

I suppose this situation goes to the heart of the goals of TR.  Is it a
pragmatic type system, designed to guide ones aim and
minimize inadvertent loss of limb, or a martinet willing to ban 32oz
servings of soft drinks for my own well being.

To be clear, I'm not arguing one way or the other here, this stuff is way
over my head, just trying to think through all the ramifications this slope
bends towards.  FWIW, I'm in the TR should be my able consul and
trusted advisor, but not my jail keeper inhibitor camp.   I reserve the
right and accept the responsibility to partake of a  BigGulp despite my
good Doctor's advice.


On Tue, Oct 30, 2012 at 5:25 PM, Neil Toronto <neil.toronto at gmail.com>wrote:

> 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 ⊥
>
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/**users <http://lists.racket-lang.org/users>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20121031/e23964e0/attachment.html>