27.12.2011, 07:30, "Alexander Solla" <alex.so...@gmail.com>:
And why exactly should we limit ourselves to some theory you happen to like?Because the question was about MY IDEAL.
You're right. I'm confusing two different threads. My apologies.
But (_|_) IS a concrete value.Um, perhaps in denotational semantics. But even in that case, it is not a HASKELL value.
Could you please clarify the meaning of "HASKELL value"? Does it mean something that can be represented in memory, fully evaluated? If so, infinite lists like [1..] aren't HASKELL value's either, which is rather limiting. Or is it something else?
You seem to be mixing up syntax and semantics.
Unlikely. But, in case I'm wrong, I'd like to know what makes you think that I put any attention on syntax...
But they ARE very similar to other values. They can be members of otherwise meaningful structures, and you can do calculations with these structures. "fst (1, _|_)" is a good and meaningful calculation.Mere syntax.
So what?
...except for this. See, I didn't want to argue about definitions here, so I didn't ask you why do you think of that as a syntactic issue. That was a mistake. So: what is the reason for you to say that "fst (1, _|_)" is a "mere syntax"?
I am proposing we give Haskell bottoms semantics that bring it in line with the bottoms from various theories including lattice theory, the theory of sets, the theory of logic, as opposed to using denotational semantics' bottom semantic, which is unrealistic for a variety of reasons.
Erm... but denotational semantics IS based on lattice theory (which, in turn, is based on the theory of sets). So how on Earth can they be "opposed" to each other?
Haskell bottoms can't be compared, due to Rice's theorem. Haskell bottoms cannot be given an interpretation as a Haskell value.
Well, lots of things can't be compared. Functions, for example. Do you mean that functions like "id" are not what you call "Haskell value"?
What happens to referential transparency when distinct things are all defined by the same equation?... = let x = x in xundefined, seq, unsafeCoerce, and many other "primitives" are defined using that equation. (See GHC.Prim) The Haskell definition for these distinct things /does nothing/. It loops. The semantics we get for them (an error message if we use undefined, a causal side-effect if we use seq, type coercion if we use unsafeCoerce) is done /magically/ by the compiler. As far as Haskell, as a language, is concerned, all of these are bottom, and they are all /equal/, because of referential transparency/substitutionality.
No. The mere fact that Prim.hs contains some stub doesn't mean anything. In fact, the Prim.hs header states: "It is not code to actually be used. Its only purpose is to be consumed by haddock."
"seq" has a very clear semantics - and yes, I do mean denotational semantics here - which has nothing to do with Prim.hs "definition".
Oops.
Indeed.
Well, that's a different story.No, it's the same story that I've been telling.
Yes, and again, I'm sorry for that.
It is clear that denotational semantics is a Platonic model of constructive computation.
Could you please stop offending abstract notions?What? Platonic does not mean "bad".
The way I see it, phylosphical notions are all offensive.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
