Orthogonal to the type system any unsynchronized parallel read/write is unsafe. <div><br></div><div>if (eq? (unbox bx) 3) </div><div> (let ((b (unbox bx))</div><div> ...</div><div><br></div><div>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.</div>
<div><br></div><div>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. </div>
<div><br></div><div>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.</div>
<div><br></div><div>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? </div>
<div><br></div><div>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.</div>
<div><br></div><div>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.</div>
<div><br></div><div><br></div><div><div class="gmail_quote">On Tue, Oct 30, 2012 at 5:25 PM, Neil Toronto <span dir="ltr"><<a href="mailto:neil.toronto@gmail.com" target="_blank">neil.toronto@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5">On 10/30/2012 01:24 PM, Danny Yoo wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On Tue, Oct 30, 2012 at 1:10 PM, Ray Racine <<a href="mailto:ray.racine@gmail.com" target="_blank">ray.racine@gmail.com</a>> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Been awhile as this is old library code, but I recall the below code once<br>
worked for me. Currently failing at the moment, though may have broken at<br>
any time of the last few months.<br>
</blockquote>
<br>
Hmmmm! This seems to be triggering based on HashTable being there. A<br>
reduced case also fails:<br>
<br>
#lang typed/racket/base<br>
(define-predicate myhash? (HashTable Symbol String))<br>
<br>
with the following error message:<br>
<br>
---<br>
<br>
Type Checker: Type (HashTable Symbol String) could not be converted to<br>
a contract. in: (HashTable Symbol String)<br>
</blockquote>
<br></div></div>
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:<br>
<br>
(define-predicate boxof-integer? (Boxof Integer))<br>
<br>
Now write some code using it:<br>
<br>
(define: bx : (Boxof Any) (box 4))<br>
<br>
(cond [(boxof-integer? bx)<br>
(define n (unbox bx))<br>
...]<br>
[else<br>
...])<br>
<br>
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)?<br>
<br>
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.<br>
<br>
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.<br>
<br>
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.<br>
<br>
Neil ⊥<br>
<br>
____________________<br>
Racket Users list:<br>
<a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/<u></u>users</a><br>
</blockquote></div><br></div>