<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Except in the complexity gymnastics and the fragility of the conclusions.<div><br></div><div>Humans can't do large scale complex brain gymnastics - that's why abstraction exists - if your proof process doesn't abstract (and in the C case you need to know *everything* about *everything* and have to "prove" it all in one go and that proof will not survive a single change) then it isn't feasible.</div><div><br></div><div>Haskell gives you the means to manage the complexity - and grasping complexity is humanities current challenge...</div><div><br></div><div>Neil<br><div><div><br></div><div><br></div><div><br><div><div>On 28 Jul 2012, at 05:43, damodar kulkarni wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">So a language is referentially transparent if replacing a sub-term with<br>
another with the same denotation doesn't change the overall meaning?<br>
But then isn't any language RT with a sufficiently cunning denotational<br>
semantics? Or even a dumb one that gives each term a distinct denotation.</blockquote><div><br>That's neat ... I mean, by performing sufficiently complicated brain gymnastics, one can do equational reasoning on C subroutines (functions!) too.<br>
<br></div>So, there is no "big" difference between C and Haskell when it comes to equational reasoning...<br><br> <br>Regards,<br>Damodar <br><br><br><div class="gmail_quote">On Sat, Jul 28, 2012 at 1:47 AM, Alexander Solla <span dir="ltr"><<a href="mailto:alex.solla@gmail.com" target="_blank">alex.solla@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br><br><div class="gmail_quote"><div>On Fri, Jul 27, 2012 at 12:06 PM, Ross Paterson <span dir="ltr"><<a href="mailto:ross@soi.city.ac.uk" target="_blank">ross@soi.city.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div>On Fri, Jul 27, 2012 at 07:19:40PM +0100, Chris Dornan wrote:<br>
> > So a language is referentially transparent if replacing a sub-term with another with the same<br>
> > denotation doesn't change the overall meaning?<br>
><br>
> Isn't this just summarizing the distinguishing characteristic of a denotational semantics?<br>
<br>
</div>Right, so where's the substance here?<br>
<div><br>
> My understanding is that RT is about how easy it is to carry out<br>
> _syntactical_ transformations of a program that preserve its meaning.<br>
> For example, if you can freely and naively inline a function definition<br>
> without having to worry too much about context then your PL is deemed<br>
> to possess lots of RT-goodness (according to FP propaganda anyway; note<br>
> you typically can't freely inline function definitions in a procedural<br>
> programming language because the actual arguments to the function may<br>
> involve dastardly side effects; even with a strict function-calling<br>
> semantics divergence will complicate matters).<br>
<br>
</div>Ah, but we only think that because of our blinkered world-view.<br>
<br>
Another way of looking at it is that the denotational semanticists have<br>
created a beautiful language to express the meanings of all those ugly<br>
languages, and we're programming in it.</blockquote><div><br></div></div><div>A third way to look at it is that mathematicians, philosophers, and logicians invented the semantics denotational semanticists have borrowed, specifically because of the properties derived from the philosophical commitments they made. Computer science has habit of taking ideas from other fields and merely renaming them. "Denotational semantics" is known as "model theory" to everyone else. </div>
<div><br></div><div>Let's consider a referentially /opaque/ context: quotation marks. We might say "It is necessary that four and four are eight. And we might also say that "The number of planets is eight." But we cannot unify the two by substitution and still preserve truth functional semantics. We would get "It is necessary that four and four are the number of planets" (via strict substitution joining on 'eight') or a more idiomatic phrasing like "It is necessary that the number of planets is four and four".</div>
<div><br></div><div>This is a big deal in logic, because there are a lot of languages which quantify over real things, like time, possibility and necessity, etc., and some of these are not referentially transparent. In particular, a model for such a language will have to use "frames" to represent context, and there typically is not a unique way to create the framing relation for a logic.</div>
</div>
<br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br><br clear="all"><br><br>
_______________________________________________<br>Haskell-Cafe mailing list<br><a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>http://www.haskell.org/mailman/listinfo/haskell-cafe<br></blockquote></div><br></div></div></div></body></html>