On Tue, Dec 20, 2011 at 9:16 PM, MigMit <miguelim...@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": http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.8232
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe