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