Gabriel Dos Reis wrote:
I agree with most of what you said. However, the slogan "well-typed
programs don't go wrong" does some value that I would heisate to
compromise...
But well-typed programs can still diverge! So "go wrong" just means
that _when_ they return a value, it is guaranteed to be of the right type.
You can do the same thing for types - this is usually called a 'kinding'
system. In fact some languages (like Tim Sheard's Omega --
http://web.cecs.pdx.edu/~sheard/Omega/index.html) push that further by
having a complete hierarchy (the names often used for the lower levels
are term - type - kind - sort).
A "well-kinded" type doesn't "go wrong" either [assuming termination].
Jacques
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
