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

[Rustom Mody]

On Sat, Dec 24, 2011 at 8:20 PM, Alexander Solla <alex.solla at gmail.com>wrote:

>
>
> On Wed, Dec 21, 2011 at 8:39 PM, MigMit <miguelimo38 at yandex.ru> 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!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20111224/c1b5cde4/attachment-0001.htm>