Reddy on Referential Transparency

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
13 messages Options
Reply | Threaded
Open this post in threaded view
|

Reddy on Referential Transparency

Chris Dornan
Café,

For those who haven’t seen it Uday Reddy has a comprehensive answer to a
request
to explain referential transparency on Stack Overflow.

 
http://stackoverflow.com/questions/210835/what-is-referential-transparency/9
859966#9859966

For good measure he finishes with a rather scathing assessment of functional
programmers’ claim to ownership of RT:

    Functional programmers don't know much of this research.
   Their ideas on referential transparency are to be taken
   with a large grain of salt.

Marvellous! 'Tis rare to find such a robust assessment combined with
understanding (and it certainly makes me think a bit).

Have we become a bit complacent about RT?

Chris



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Reddy on Referential Transparency

Claus Reinke
> Have we become a bit complacent about RT?

We're not complacent, we just know things without having to
check references. Just kidding, of course, functional programmers
tend to enjoy improving their understanding!-)

The Strachey reference is worth reading - great that it is online
these days, but it can be useful to complement it with others.

Before Quine, there was Carroll, who explored meaning [1]
and referential opacity [2], among other things. Also useful
is Sondergaard and Sestoft [3], which explores both the history
and the differences between not-quite-equivalent definitions.

I happen to disagree with Reddy's assertion that having to
explain a complicated language with the help of a less complicated
one is perfectly adequate. Reddy himself has done good work on
semantics of programming languages, but I'm a programmer
first - if the language I work with does not give me the qualities
that its semantics give me, then my means of expression and
understanding are limited by the translation.

All to be taken with grain of salt, active mind and sense of humor.
Claus

[1, Chapter 6]
    http://en.wikiquote.org/wiki/Through_the_Looking-Glass

[2, the name of the song]
    http://homepages.tcp.co.uk/~nicholson/alice.html

[3] Søndergaard, Sestoft (1990). "Referential transparency,
    definiteness and unfoldability". Acta Informatica 27 (6): 505-517.
    http://www.itu.dk/people/sestoft/papers/SondergaardSestoft1990.pdf
 


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Reddy on Referential Transparency

Chris Dornan
Claus Reinke [mailto:[hidden email]]:

> I happen to disagree with Reddy's assertion that having to explain a
complicated language
> with the help of a less complicated one is perfectly adequate. Reddy
himself has done good
> work on semantics of programming languages, but I'm a programmer first -
if the language
> I work with does not give me the qualities that its semantics give me,
then my means of
> expression and understanding are limited by the translation.

I also disagree. Haskell makes extensive use of translation into a core but
those translations
work so well because of the strong referential transparency guarantees that
you get with
Haskell.

Equational reasoning locally and leaning on types for refactoring are
intimately integrated into
my functional programming process (as I bet they are for most Haskell
programmers) -- I think
the academic promise of RT has become quite 'real'.

Something that may not be obvious to someone who doesn't program Haskell at
scale is the major
benefits of 'ghc -Wall'.  Working with the -Wall subset of Haskell (as many
do on production code)
problems with accidental variable capture is much more difficult to do -- a
terrific safeguard when
(equationally) working code.

Chris
 


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Reddy on Referential Transparency

Ross Paterson
In reply to this post by Chris Dornan
On Fri, Jul 27, 2012 at 01:08:31PM +0100, Chris Dornan wrote:

> For those who haven’t seen it Uday Reddy has a comprehensive answer to a
> request to explain referential transparency on Stack Overflow.
>  
> http://stackoverflow.com/questions/210835/what-is-referential-transparency/9
> 859966#9859966
>
> For good measure he finishes with a rather scathing assessment of functional
> programmers’ claim to ownership of RT:
>
>     Functional programmers don't know much of this research.
>    Their ideas on referential transparency are to be taken
>    with a large grain of salt.
>
> Marvellous! 'Tis rare to find such a robust assessment combined with
> understanding (and it certainly makes me think a bit).

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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Reddy on Referential Transparency

Chris Dornan
> 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?

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).

Chris



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Reddy on Referential Transparency

Ross Paterson
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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Reddy on Referential Transparency

Chris Dornan


On Jul 27, 2012 8:07 PM, "Ross Paterson" <[hidden email]> wrote:

> 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.

I think that's the idea.

Also works out for compiler writers, parallel implementations, etc.

Problem is from a 'classical' programming perspective it's an acquired taste.

Chris


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Reddy on Referential Transparency

Alexander Solla
In reply to this post by Ross Paterson


On Fri, Jul 27, 2012 at 12:06 PM, Ross Paterson <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> wrote:


On Fri, Jul 27, 2012 at 12:06 PM, Ross Paterson <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe






_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Reddy on Referential Transparency

Neil Davies
Except in the complexity gymnastics and the fragility of the conclusions.

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.

Haskell gives you the means to manage the complexity - and grasping complexity is humanities current challenge...

Neil



On 28 Jul 2012, at 05:43, damodar kulkarni wrote:



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 <[hidden email]> wrote:


On Fri, Jul 27, 2012 at 12:06 PM, Ross Paterson <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe





_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Reddy on Referential Transparency

Jay Sulzberger
In reply to this post by damodar kulkarni


On Sat, 28 Jul 2012, damodar kulkarni <[hidden email]> wrote:

> 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

The general theory of equational reasoning is often applicable
because often we have a collection of sentences S of the form

   x = y

where x and y are "terms", and often we have a set of models M,
where given a system of backround assumptions, we can ask of the
above sentence, call it s, whether in some particular model m, is
it the case that

   eval(x) = eval(y)

where now the sentence above is not a sentence of S, but rather a
fact, under assumptions, about the model m, namely that what the
term x means in m is equal to what the term y means in m.  Here
we have written what the term x refers to in m as "eval(x)".  For
example x might be "(vector-ref part-of-backround 17)" in some
Lisp source code, given as text, and y might
"(vector-ref part-of-backround 116)", and part-of-backround is
some vector which comes from, in general both the model m and,
this is a "scare phrase", the backround assumptions.  Oi, please
forgive tangle here!

Note that the = in the sentence s is not the same = as in the
model m, and we should in a first text write them with different
symbols.  As terms x and y are not equal-as-terms.  It is only
their "values" in m that are equal-in-m.

(Obtuse Precisian Crank Further Remark: And the general theory of
equality often applies to whatever sort of object lies in the
vector part-of-backround at position 17, and also to whatever
lies at position 116.  THE ARGUMENT IS COMPLETE!  But see

  http://iml.univ-mrs.fr/~girard/TS2.pdf

for more and different.)


Personal remark: I remember the wonderful feeling of having a
weight lifted from me when I read this in Roger C. Lyndon's "Notes on Logic":

   Oi, ah, I cannot find the quote tonight.

The quote was something like

   In this book we shall work at the level of precision which
   today is standard in works on the theory of groups, say.

by which Lyndon meant that certain extraordinarily finicky
considerations were, by the date of composition, standard, and
the reader might be trusted to handle these without error.

Of course, as a beginner coming to Haskell, and as an old Lisper

(my first Lisp was LISP 1.5, for which see
http://www.softwarepreservation.org/projects/LISP/book/LISP%201.5%20Programmers%20Manual.pdf)

I wish that Haskell made more patent to my un-practiced eye more
of such finicky details^Wbasics.  Naturally what I'd like is
Haskell source code presented in the usual parenthesized prefix
notation of Lisp, with of course, every term having an
immediately available complete explicit typing, which could
perhaps be presented when one clicks on the term (perhaps plists
might be part of the mechanism).

BRING OUT THE CORE!

oo--JS.


>
>
> On Sat, Jul 28, 2012 at 1:47 AM, Alexander Solla <[hidden email]>wrote:
>
>>
>>
>> On Fri, Jul 27, 2012 at 12:06 PM, Ross Paterson <[hidden email]>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
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Reddy on Referential Transparency

wren ng thornton
In reply to this post by Ross Paterson
On 7/27/12 1:49 PM, Ross Paterson wrote:
> 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.

Yes, but such denotations aren't useful for very much. The whole point
of denotational semantics is to assert that some (primitive) expressions
denote the same thing, and then to derive that other expressions (e.g.,
whole programs) denote the same thing. If we say that every expression
is different from every other expression, then ---for example--- the
only semantics-preserving transformation is the identity transformation.
Our semantics is, thus, worthless for vetting whether a compiler's
transformation is "okay" or not. In fact, this model explains exactly
nothing about the *meaning* of those expressions.

--
Live well,
~wren

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Reddy on Referential Transparency

Chris Dornan
In reply to this post by Ross Paterson
Uday Reddy has followed up with another substantial and interesting post on referential transparency here:

    http://stackoverflow.com/questions/210835/what-is-referential-transparency/11740176#11740176

The thrust of his argument appears to be that functional programmers have created a lot of confusion around the ideas of referential transparency. I sympathize but I think he is going too far.

As I see it, while the very close association of functional programming and related concepts with referential transparency may have led to some confusion around the concept that doesn't mean that the specific means that functional programmers have been using to increase (classically understood) RT in functional programs is somehow invalid.

Reddy has responded to my comment here

    http://stackoverflow.com/a/11680011/306550

and I have followed up in turn.

Chris


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe