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 <[email protected]>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
