<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><br></div><div>TR is good for many of the ideas in TML, but some of its chapters are specific to TML's type system (structures and functors specifically, we allude to generative datatypes). If you are looking for a first dip into a language with an expressive type system, I can recommend TML. </div><div><br></div><div>If you are interested in an excursion into the theory of types and various variations -- though not covering TR's peculiar type system, Pierce's book is a must. </div><div><br></div><div>-- Matthias</div><div><br></div><br><div><div>On Apr 20, 2013, at 10:29 PM, Harry Spier wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><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>
____________________<br> Racket Users list:<br> <a href="http://lists.racket-lang.org/users">http://lists.racket-lang.org/users</a><br></blockquote></div><br></body></html>