[racket] How to read procedure documentation?

From: Matthias Felleisen (matthias at ccs.neu.edu)
Date: Fri Apr 19 17:27:03 EDT 2013

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. ]]

Posted on the users mailing list.