[Aldor-l] [Axiom-developer] spad: language and compiler

[Jacques Carette]

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