Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?

On Sat, Dec 24, 2011 at 8:20 PM, Alexander Solla wrote:

On Wed, Dec 21, 2011 at 8:39 PM, MigMit wrote:

...

On 22 Dec 2011, at 06:25, Alexander Solla wrote:

...

Denotational semantics is unrealistic.

And so are imaginary numbers. But they are damn useful for electrical circuits calculations, so who cares?

Not a fair comparison. Quaternions are not particularly useful for electrical circuits, because it is unrealistic to apply a four-dimensional construct to two-dimensional phase spaces. In the same way, denotational semantics adds features which do not apply to a theory of finite computation.

...

...

The /defining/ feature of a bottom is that it doesn't have an interpretation.

...

What do you mean by "interpretation"?

You know, the basic notion of a function which maps syntax to concrete values.

http://en.wikipedia.org/wiki/Model_theory

...

...

They should all be treated alike, and be treated differently from every other Haskell value.

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. What is fst doing? It computes "forall (x,y) |- x". Using the language of model theory, we can say that Haskell computes an interpretation "forall (x,y) |= x". It is _|_ that lacks an intepretation, not fst. We can see that by trying "fst (_|_,1), which reduces to _|_ by the proof rule for fst. _|_ lacks an interpretation, so the run-time either loops forever or throws an error (notice that error throwing is only done with compiler magic -- if you define your own undefined = undefined, using it will loop. GHC is specially trained to look for Prelude.undefined to throw the "undefined" error.)

...

...

Every other Haskell value /does/ have an interpretation.

So, (_|_) is bad, but (1, _|_) is good?

I did not introduce "good" and "bad" into this discussion. I have merely said (in more words) that I want my hypothetical perfect language to prefer OPERATIONAL (model) SEMANTICS for a typed PARACONSISTENT LOGIC over the DENOTATIONAL SEMANTICS which the official documentation sometimes dips into.

Using examples from denotational semantics is not going to change my mind about the applicability of one or the other. It is clear that denotational semantics is a Platonic model of constructive computation.

You make it sound as though platonism is somehow bad. Before we get into that lets look at a capsule of our history: Kronecker and Cantor disagree on whether sets exist. K: God created the natural numbers; all the rest is the work of man. C: All manner of infinite sets exist (presumably in the mind of God?) A generation later and continuing, Hilbert and Brouwer disagree on what constitutes a proof. A little later Goedel sets out to demolish Hilbert's formalist agenda. The (interpretations of) Hilbert's philosophical position is particularly curious: For Brouwer, Hilbert is wrong because he is a platonist -- believes in completed infinities For Goedel, Hilbert is wrong because he is not a platonist -- he is looking for mechanizable proofs. Talk of two stools!! Turing tries to demolish Goedel. His real intention is AI not the Turing machine. He does not succeed -- simple questions turn out to be undecidable/non-computable. However a 'side-effect' (ahem) of his attempts via the TM is ... the computer. That Goedel was a (mostly closet) platonist: http://guidetoreality.blogspot.com/2006/12/gdels-platonism.html Am I arguing that platonism is good? Dunno... I am only pointing out that the tension between platonism and its opponents (formalist, empiricist, constructivist etc) is evidently a strong driver for progress BTW a more detailed look at the historical arguments would show that the disagreements were more violent than anything on this list :-) Hopefully on this list we will be cordial and wish each other a merry Christmas!