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
