<div dir="ltr"><br><div>Can someone recommend a good book on type systems?  Is &quot;The Little MLer&quot; a good place to start and can you do this book with typed Racket rather than ML.</div><div><br></div><div>Thanks,</div>
<div>Harry Spier</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Apr 19, 2013 at 5:27 PM, Matthias Felleisen <span dir="ltr">&lt;<a href="mailto:matthias@ccs.neu.edu" target="_blank">matthias@ccs.neu.edu</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im"><br>
On Apr 19, 2013, at 4:02 PM, Manfred Lotz wrote:<br>
<br>
&gt; But it is more powerful.<br>
<br>
<br>
</div>[[ This is a quibble that could take you off your chosen path for years.<br>
The words &#39;more powerful&#39; aren&#39;t that easy to agree with. Here are ways<br>
to make them incorrect:<br>
  -- in a sound type system, the type signature f : int -&gt; int means that<br>
        when you launch your program, f will never, ever be applied to a<br>
        bit string that represents a boolean. Our contract cannot guarantee<br>
        this much. It will only guarantee that when f is applied to #true,<br>
        an exn:fail:contract is signaled.<br>
  -- our contract system has a really hard time expressions g : ∀ t : t -&gt; t.<br>
        In a sound type system, assigning this forall type to g means that for<br>
        all possible types T in your module or types in modules linked to yours,<br>
        possibly written in the distant future, the function assumes signature<br>
        T -&gt; T. If you equip g with an analogous contract in our world, the<br>
        guarantee you get is that if g tries to misbehave -- by probing the<br>
        given argument, it (g) will not behave as you expect.<br>
  -- and lastly, you can easily imagine that proof systems can answer much<br>
        more complex questions than Turing machines, and that you can design<br>
        a type system that corresponds to such a proof system. Of course, you<br>
        would then not necessarily use algorithms to check your type correctness.<br>
As I said, studying this question may take you off the beaten track, but I think<br>
people on this mailing list should be as informed as people on the Haskell or<br>
ML lists. ]]<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
____________________<br>
  Racket Users list:<br>
  <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a><br>
</div></div></blockquote></div><br></div>