[Haskell-cafe] Reddy on Referential Transparency

[damodar kulkarni]

So a language is referentially transparent if replacing a sub-term with
> another with the same denotation doesn't change the overall meaning?
> But then isn't any language RT with a sufficiently cunning denotational
> semantics?  Or even a dumb one that gives each term a distinct denotation.


That's neat ... I mean, by performing sufficiently complicated brain
gymnastics, one can do equational reasoning on C subroutines (functions!)
too.

So, there is no "big" difference between C and Haskell when it comes to
equational reasoning...


Regards,
Damodar


On Sat, Jul 28, 2012 at 1:47 AM, Alexander Solla <alex.solla at gmail.com>wrote:

>
>
> On Fri, Jul 27, 2012 at 12:06 PM, Ross Paterson <ross at soi.city.ac.uk>wrote:
>
>> On Fri, Jul 27, 2012 at 07:19:40PM +0100, Chris Dornan wrote:
>> > > So a language is referentially transparent if replacing a sub-term
>> with another with the same
>> > > denotation doesn't change the overall meaning?
>> >
>> > Isn't this just summarizing the distinguishing characteristic of a
>> denotational semantics?
>>
>> Right, so where's the substance here?
>>
>> > My understanding is that RT is about how easy it is to carry out
>> > _syntactical_ transformations of a program that preserve its meaning.
>> > For example, if you can freely and naively inline a function definition
>> > without having to worry too much about context then your PL is deemed
>> > to possess lots of RT-goodness (according to FP propaganda anyway; note
>> > you typically can't freely inline function definitions in a procedural
>> > programming language because the actual arguments to the function may
>> > involve dastardly side effects; even with a strict function-calling
>> > semantics divergence will complicate matters).
>>
>> Ah, but we only think that because of our blinkered world-view.
>>
>> Another way of looking at it is that the denotational semanticists have
>> created a beautiful language to express the meanings of all those ugly
>> languages, and we're programming in it.
>
>
> 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.
>
> 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".
>
> 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.
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120728/c8cbba79/attachment.htm>