[racket] How to read procedure documentation?

From: Matthias Felleisen (matthias at ccs.neu.edu)
Date: Sun Apr 21 16:35:08 EDT 2013

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. 

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. 

-- Matthias


On Apr 20, 2013, at 10:29 PM, Harry Spier wrote:

> 
> 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.
> 
> Thanks,
> Harry Spier
> 
> 
> On Fri, Apr 19, 2013 at 5:27 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
> 
> On Apr 19, 2013, at 4:02 PM, Manfred Lotz wrote:
> 
> > But it is more powerful.
> 
> 
> [[ This is a quibble that could take you off your chosen path for years.
> The words 'more powerful' aren't that easy to agree with. Here are ways
> to make them incorrect:
>   -- in a sound type system, the type signature f : int -> int means that
>         when you launch your program, f will never, ever be applied to a
>         bit string that represents a boolean. Our contract cannot guarantee
>         this much. It will only guarantee that when f is applied to #true,
>         an exn:fail:contract is signaled.
>   -- our contract system has a really hard time expressions g : ∀ t : t -> t.
>         In a sound type system, assigning this forall type to g means that for
>         all possible types T in your module or types in modules linked to yours,
>         possibly written in the distant future, the function assumes signature
>         T -> T. If you equip g with an analogous contract in our world, the
>         guarantee you get is that if g tries to misbehave -- by probing the
>         given argument, it (g) will not behave as you expect.
>   -- and lastly, you can easily imagine that proof systems can answer much
>         more complex questions than Turing machines, and that you can design
>         a type system that corresponds to such a proof system. Of course, you
>         would then not necessarily use algorithms to check your type correctness.
> As I said, studying this question may take you off the beaten track, but I think
> people on this mailing list should be as informed as people on the Haskell or
> ML lists. ]]
> 
> 
> 
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
> 
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20130421/bba6e869/attachment-0001.html>

Posted on the users mailing list.