<div dir="ltr"><br><div>Can someone recommend a good book on type systems? Is "The Little MLer" 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"><<a href="mailto:matthias@ccs.neu.edu" target="_blank">matthias@ccs.neu.edu</a>></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>
> 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 'more powerful' aren'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 -> 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 -> 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 -> 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>