|
From: | Jacques Carette |
Subject: | Re: [Aldor-l] [Axiom-developer] spad: language and compiler |
Date: | Wed, 30 Aug 2006 13:17:37 -0400 |
User-agent: | Thunderbird 1.5.0.5 (Windows/20060719) |
Gabriel Dos Reis wrote:
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.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...
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
[Prev in Thread] | Current Thread | [Next in Thread] |