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

Alexander Solla alex.solla at gmail.com
Sat Dec 24 15:50:13 CET 2011


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 know, my scientific advisor used to say "math is about calling
> different things by the same name; philosophy is about calling the same
> thing by different names". It seems to me that philosophy is something
> you're doing now, whereas programming is all about math.
>

Then you are mistaken.  I am talking about choosing the appropriate
mathematical model of computation to accurately, clearly, and simply
describe the language's semantics.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20111224/cf071c8c/attachment.htm>


More information about the Haskell-Cafe mailing list