On Fri, 19 Apr 2013 17:27:03 -0400 Matthias Felleisen <matth...@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 ____________________ Racket Users list: http://lists.racket-lang.org/users
