[racket] How to read procedure documentation?

From: Manfred Lotz (manfred.lotz at arcor.de)
Date: Sat Apr 20 00:37:44 EDT 2013

On Fri, 19 Apr 2013 17:27:03 -0400
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. ]]
> 
> 
> 

Yes, you are right. When I said 'more powerful' I didn't mean to
compare against languages like Haskell or ML which have a type system.

I just meant from a documentation point of view it is more powerful to
say that a parameter e.g. must satisfy path-string? than to say it must
be a string which must be a valid path name. In this case I don't need
to ask what is a valid path string but could find the exact meaning by
looking into path-string?.

My understanding is that parameter path-string? will be
checked at run time but only if the programmer who coded e.g.
file->string did call path-string?. 


-- 
Manfred


 




Posted on the users mailing list.