On Tue, Dec 20, 2011 at 9:16 PM, MigMit
<miguelimo38@yandex.ru> wrote:
On 21 Dec 2011, at 08:24, Alexander Solla wrote:
> I would rather have an incomplete semantic, and have all the incomplete parts collapsed into something we call "bottom".
I don't see the reason to limit ourselves to that. Of course, in total languages like Agda there is no need for (_|_). But in a turing-complete lazy language like Haskell we really need it. Of course, it makes not much sense to write "fix id" anywhere in your program; but, for example, lists like "1:2:3:4:5:_|_" can be really useful.
It is not "limiting" to make distinctions that capture real differences. An overly broad generalization limits what can be proved. Can we prove that every vehicle with wheels has a motor? Of course not -- bicycles exist. Can we prove every car has a motor? Yes we can. Throwing bottoms into the collection of values is like throwing bicycles into the collection of cars. We can say /less/ about the collection than we could before, /because/ the collection is more general.
And denotational semantics is not just nice. It is useful. It's the best way to understand why the program we just wrote doesn't terminate.
Denotational semantics is unrealistic. It is a Platonic model of constructive computation. Alan Turing introduced the notion of an "oracle" to deal with what we are calling bottom. An oracle is a "thing" that (magically) "knows" what a bottom value denotes, without having to wait for an infinite number of steps. Does Haskell offer oracles? If not, we should abandon the use of distinct bottoms. The /defining/ feature of a bottom is that it doesn't have an interpretation.
Note that I am not suggesting abandoning the notion of /a/ bottom. They should all be treated alike, and be treated differently from every other Haskell value. Every other Haskell value /does/ have an interpretation. Bottom is different from every "other value". We should exclude it from the collection of values. Treating things that are not alike as if they are introduces a loss of information. We can prove useful things about the collection "real" values that we cannot prove about bottom, and so, about the collection of real values and bottoms.
I happen to only write Haskell programs that terminate. It is not that hard. We must merely restrict ourselves to the total fragment of the language, and there are straight-forward methods to do so. In particular, I suggest the paper "Fast and Loose Reasoning is Morally Correct":