"show" for functional types

newer
Re: [Haskell] What's up with this...

older
Re: [Haskell] reading binary files

Greg Buchholz

31 Mar 2006 31 Mar '06

7:57 p.m.

In section 5 of _Fun with Phantom Types_, Hinze states... "Let us move on to one of the miracles of theoretical computer science. In Haskell, one cannot show values of functional types. For reasons of computability, there is no systematic way of showing functions and any ad-hoc approach would destroy referential transparency (except if show were a constant function). For instance, if show yielded the text of a function definition, we could distinguish, say, quick sort from merge sort. Substituting one for the other could then possibly change the meaning of a program." ...I guess I'm not understanding what that means. Would there be some sort of contradiction that arises when trying to evaluate "show (show)" or somesuch? Can anyone point me in the direction of information that tries to explain why this is? I'm at a loss as to what search terms to use. Thanks, Greg Buchholz

Show replies by date

Neil Mitchell

31 Mar 31 Mar

8:11 p.m.

Hi, First, its useful to define referential transparency. In Haskell, if you have a definition f = not Then this means that anywhere you see f, you can replace it with not. For example "f True" and "not True" are the same, this is referentially transparent. Now lets define "super show" which takes a function, and prints its code behind it, so: superShow f = "not" superShow g = "\x -> case ..." now superShow f /= superShow g, so they are no longer referentially transparent. Hence, you have now broken referential transparency. So you can't show these two functions differently, so what can you do instead? You can just give up and show all functions the same instance Show (a -> b) where show x = "<function>" This is the constant definition of show mentioned. Thanks Neil On 4/1/06, Greg Buchholz wrote:

...

In section 5 of _Fun with Phantom Types_, Hinze states...

"Let us move on to one of the miracles of theoretical computer science. In Haskell, one cannot show values of functional types. For reasons of computability, there is no systematic way of showing functions and any ad-hoc approach would destroy referential transparency (except if show were a constant function). For instance, if show yielded the text of a function definition, we could distinguish, say, quick sort from merge sort. Substituting one for the other could then possibly change the meaning of a program."

...I guess I'm not understanding what that means. Would there be some sort of contradiction that arises when trying to evaluate "show (show)" or somesuch? Can anyone point me in the direction of information that tries to explain why this is? I'm at a loss as to what search terms to use.

Thanks,

Greg Buchholz _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Greg Buchholz

9:41 p.m.

Neil Mitchell wrote:

...

Now lets define "super show" which takes a function, and prints its code behind it, so:

superShow f = "not" superShow g = "\x -> case ..."

now superShow f /= superShow g, so they are no longer referentially transparent.

OK. I'm probably being really dense today, but where did "g" come from? Is this is the internal definition of "not"? And does this loss of referential transparency contaminate the rest of the language, or is this superShow just an anomaly? Thanks, Greg Buchholz

Brian Hulley

9:45 p.m.

Greg Buchholz wrote:

...

Neil Mitchell wrote:

...
Now lets define "super show" which takes a function, and prints its code behind it, so:

superShow f = "not" superShow g = "\x -> case ..."

now superShow f /= superShow g, so they are no longer referentially transparent.

OK. I'm probably being really dense today, but where did "g" come from? Is this is the internal definition of "not"? And does this loss of referential transparency contaminate the rest of the language, or is this superShow just an anomaly?

Here is another example. Consider two functions f and g which, given the same inputs, always return the same outputs as each other such as: f x = x + 2 g x = x + 1 + 1 Now since f and g compute the same results for the same inputs, anywhere in a program that you can use f you could just replace f by g and the observable behaviour of the program would be completely unaffected. This is what referential transparency means. However, if you allowed a function such as superShow, superShow f == "x + 2" and superShow g == "x + 1 + 1" so superShow f /= superShow g thus you could no longer just use f and g interchangeably, since these expressions have different results. Thus the existence of superShow would contaminate everything, because if you were using a library function for example you would have no way of knowing whether the writer of the function had used superShow somewhere deep in its implementation ie referential transparency is an all or nothing concept. Regards, Brian.

Greg Buchholz

11:10 p.m.

Brian Hulley wrote: ] Here is another example. Consider two functions f and g which, given the ] same inputs, always return the same outputs as each other such as: ] ] f x = x + 2 ] g x = x + 1 + 1 ] ] Now since f and g compute the same results for the same inputs, anywhere in ] a program that you can use f you could just replace f by g and the ] observable behaviour of the program would be completely unaffected. This is ] what referential transparency means. ] ] However, if you allowed a function such as superShow, superShow f == "x + ] 2" and superShow g == "x + 1 + 1" so superShow f /= superShow g thus you ] could no longer just use f and g interchangeably, since these expressions ] have different results. Hmm. It must be a little more complicated than that, right? Since after all you can print out *some* functions. That's what section 5 of _Fun with Phantom Types_ is about. Here's a slightly different example, using the AbsNum module from... http://www.haskell.org/hawiki/ShortExamples_2fSymbolDifferentiation

...

import AbsNum

f x = x + 2 g x = x + 1 + 1

y :: T Double y = Var "y"

main = do print (f y) print (g y)

...which results in... *Main> main (Var "y")+(Const (2.0)) (Var "y")+(Const (1.0))+(Const (1.0)) ...is this competely unrelated? Thanks, Greg Buchholz

Brian Hulley

1 Apr 1 Apr

7:50 a.m.

Greg Buchholz wrote:

...

Hmm. It must be a little more complicated than that, right? Since after all you can print out *some* functions. That's what section 5 of _Fun with Phantom Types_ is about. Here's a slightly different example, using the AbsNum module from...

http://www.haskell.org/hawiki/ShortExamples_2fSymbolDifferentiation

...
import AbsNum

f x = x + 2 g x = x + 1 + 1

y :: T Double y = Var "y"

main = do print (f y) print (g y)

...which results in...

*Main> main (Var "y")+(Const (2.0)) (Var "y")+(Const (1.0))+(Const (1.0))

...is this competely unrelated?

Interesting! Referential transparency (as I understand it) has indeed been violated. Perhaps the interaction of GADTs and type classes was not sufficiently studied before being introduced to the language. So I'm now just as puzzled as you. Thanks for this example, Brian.

Claus Reinke

9:05 a.m.

...

...
...
import AbsNum

f x = x + 2 g x = x + 1 + 1

y :: T Double y = Var "y"

main = do print (f y) print (g y)

...which results in...

*Main> main (Var "y")+(Const (2.0)) (Var "y")+(Const (1.0))+(Const (1.0))

...is this competely unrelated?

Interesting! Referential transparency (as I understand it) has indeed been violated. Perhaps the interaction of GADTs and type classes was not sufficiently studied before being introduced to the language.

So I'm now just as puzzled as you.

the usual way to achieve this uses the overloading of Nums in Haskell: when you write '1' or '1+2', the meaning of those expressions depends on their types. in particular, the example above uses 'T Double', not just 'Double'. recall the problem (simplified): mapping from values to representations is not a function (unless we pick a unique representative for each class of equivalent expressions). but there is nothing keeping us from going the other way: from representations to values. the example above is even simpler, as it only constructs representations. what the overloading for representation trick usually does is to create an instance of Num for representations of arithmetic expressions.when you write '1+2::Representation', that uses 'fromInteger' and '+' from the Num instance for the type 'Representation', and nothing prevents us from defining that instance in such a way that we construct a representaton instead of doing any additions. cheers, claus ps. that AbsNum module seems to do a lot more besides this, but search for the Num instance. a simpler example module, just pairing representations with values, can be found here: http://www.cs.kent.ac.uk/people/staff/cr3/toolbox/haskell/R.hs

Brian Hulley

11:53 a.m.

Claus Reinke wrote:

...

the usual way to achieve this uses the overloading of Nums in Haskell: when you write '1' or '1+2', the meaning of those expressions depends on their types. in particular, the example above uses 'T Double', not just 'Double'.

However there is nothing in the functions themselves that restricts their use to just T Double. Thus the functions can be compared for equality by supplying an argument of type T Double but used elsewhere in the program with args of type (plain) Double eg: -- Change to module AbsNum instance (Simplify a)=>Eq (T a) where (==) (Const x) (Const y) = x == y (==) (Var x) (Var y) = x == y (==) (Add xs) (Add ys) = and (map (\(x, y) -> x==y) (zip xs ys)) (==) _ _ = False -- Not needed for the example module Main where import AbsNum f x = x + 2.0 g x = x + 1.0 + 1.0 funeq :: (T Double -> T Double) -> (T Double -> T Double) -> Bool funeq p q = let y = Var "y" in p y == q y main = do print (funeq f g) print (f 10) print (g 10) putStrLn "" print (funeq f f) print (f 10) print (g 10)

...

main False 12.0 12.0

True 12.0 12.0 Thus we can determine that f is implemented by different code from g (The example would be even more convincing if Int's were used instead of Double's) and so f and g are not interchangeable.

...

... nothing prevents us from defining that instance in such a way that we construct a representaton instead of doing any additions.

Thus referential transparency of polymorphic functions is foiled. Regards, Brian.

Brian Hulley

12:11 p.m.

Brian Hulley wrote:

...

(==) (Add xs) (Add ys) = and (map (\(x, y) -> x==y) (zip xs ys))

What on earth was I thinking!!! ;-) Should be: (==) (Add xs) (Add ys) = xs == ys (Doesn't affect the validity of my argument though...)

Robert Dockins

12:34 p.m.

On Saturday 01 April 2006 11:53 am, Brian Hulley wrote:

...

Claus Reinke wrote:

...
the usual way to achieve this uses the overloading of Nums in Haskell: when you write '1' or '1+2', the meaning of those expressions depends on their types. in particular, the example above uses 'T Double', not just 'Double'.

However there is nothing in the functions themselves that restricts their use to just T Double. Thus the functions can be compared for equality by supplying an argument of type T Double but used elsewhere in the program with args of type (plain) Double eg:

Overloaded functions instantiated at different types are not (in general) the same function. If you mentally do the dictionary-translation, you'll see why. In particular for f, g :: XYZ a => a -> b, and types n m such that (XYZ n) and (XYZ m), f :: (n -> b) === g :: (n -> b) does *not* imply f :: (m -> b) === g :: (m -> b) That is where your argument falls down. Rob Dockins

Brian Hulley

12:59 p.m.

Robert Dockins wrote:

...

On Saturday 01 April 2006 11:53 am, Brian Hulley wrote:

...
Claus Reinke wrote:

...
the usual way to achieve this uses the overloading of Nums in Haskell: when you write '1' or '1+2', the meaning of those expressions depends on their types. in particular, the example above uses 'T Double', not just 'Double'.

However there is nothing in the functions themselves that restricts their use to just T Double. Thus the functions can be compared for equality by supplying an argument of type T Double but used elsewhere in the program with args of type (plain) Double eg:

Overloaded functions instantiated at different types are not (in general) the same function. If you mentally do the dictionary-translation, you'll see why.

In particular for f, g :: XYZ a => a -> b, and types n m such that (XYZ n) and (XYZ m),

f :: (n -> b) === g :: (n -> b)

does *not* imply

f :: (m -> b) === g :: (m -> b)

That is where your argument falls down.

No, it doesn't, because that wasn't my argument. Consider: f :: C a => a->a g :: C a => a->a Now if we can define just one instance of C, eg T1 where f (x::T1) \= g (x::T1), then we can tell f and g apart for all instances of C, even when there is another instance of C, eg T2, for which f (x::T2) == g (x::T2). Thus we can't just interchange the uses of f and g in the program because we can always use values of T1 to distinguish between uses of f :: T2 -> T2 and g :: T2 -> T2. If f (x::T1) == g (x::T1) then nothing has been demonstrated, as you rightly point out, because there could be another instance of of C eg T3 for which f (x::T3) \= g(x::T3). It is the inequality that is the key to breaking referential transparency, because the discovery of an inequality implies different code. Regards, Brian.

Robert Dockins

1:35 p.m.

[snip]

...

No, it doesn't, because that wasn't my argument. Consider:

f :: C a => a->a g :: C a => a->a

Now if we can define just one instance of C, eg T1 where f (x::T1) \= g (x::T1), then we can tell f and g apart for all instances of C, even when there is another instance of C, eg T2, for which f (x::T2) == g (x::T2). Thus we can't just interchange the uses of f and g in the program because we can always use values of T1 to distinguish between uses of f :: T2 -> T2 and g :: T2 -> T2.

...

If f (x::T1) == g (x::T1) then nothing has been demonstrated, as you rightly point out, because there could be another instance of of C eg T3 for which f (x::T3) \= g(x::T3).

I agree to this point.

...

It is the inequality that is the key to breaking referential transparency, because the discovery of an inequality implies different code.

Here is where you make the jump that I don't follow. You appear to be claiming that the AbsNum module coerces a Haskell compiler into breaking referential integrity by allowing you to discover a difference between the following two functions: f :: (Num a) => a -> a f x = x + 2 and g :: (Num a) => a -> a g x = x + 1 + 1 From an earlier post:

...

...
Now since f and g compute the same results for the same inputs, anywhere in a program that you can use f you could just replace f by g and the observable behaviour of the program would be completely unaffected. This is what referential transparency means.

My essential claim is that the above statement is in error (but in a fairly subtle way). It is only true when f and g are instantiated at appropriate types. This is what I meant by saying that overloading was muddying the waters. The original post did not have a type signature, so one _could_ assume that MR forced defaulting to Integer (the MR is evil, _evil_ I say), which would then make the statement true _in that context_. However the post with the AbsNum code instantiates f and g at a different type with different properties, and the equality does not hold.

...

Interesting! Referential transparency (as I understand it) has indeed been violated. Perhaps the interaction of GADTs and type classes was not sufficiently studied before being introduced to the language.

I believe your reasoning is correct, but you are using a false supposition. Rob Dockins

Brian Hulley

3:23 p.m.

Robert Dockins wrote:

...

[snip] From an earlier post:

...
...
Now since f and g compute the same results for the same inputs, anywhere in a program that you can use f you could just replace f by g and the observable behaviour of the program would be completely unaffected. This is what referential transparency means.

My essential claim is that the above statement is in error (but in a fairly subtle way).

Ok I see now! :-) I was confusing the concept of referential transparency with a kind of global code equivalence, so the rest of my argument is irrelevant. Thus I should have said: " For particular types T1 and T2, if (f (x::T1))::T2 === g x for all x in T1 then f :: T1->T2 and g ::T1->T2 can be freely substituted since the context T1->T2 cannot tell them apart." Thanks for pointing out the faulty definition, Regards, Brian.

Robert Dockins

4 Apr 4 Apr

10:02 a.m.

On Apr 1, 2006, at 3:23 PM, Brian Hulley wrote:

...

Robert Dockins wrote:

...
[snip] From an earlier post:

...
...
Now since f and g compute the same results for the same inputs, anywhere in a program that you can use f you could just replace f by g and the observable behaviour of the program would be completely unaffected. This is what referential transparency means.

My essential claim is that the above statement is in error (but in a fairly subtle way).

Ok I see now! :-) I was confusing the concept of referential transparency with a kind of global code equivalence, so the rest of my argument is irrelevant. Thus I should have said:

" For particular types T1 and T2, if (f (x::T1))::T2 === g x for all x in T1 then f :: T1->T2 and g ::T1->T2 can be freely substituted since the context T1->T2 cannot tell them apart."

Having thought about this a bit more, I realize that this statement is also too strong. In the lambda calculus, extensionality is equivalent to the validity of eta-conversion (Plotkin, Call-by-value, Call-by-name and the lambda calculus, 1975). However, in Haskell, eta-conversion is not valid (ie, meaning-preserving). Observe: f, g :: a -> b f = undefined g = \x -> undefined x forall x::a, f x === g x === _|_. However, 'seq' can tell them apart. seq f 'a' === _|_ seq g 'a' === 'a' So f and g are not replaceable in all term contexts (in particular, not in 'seq' contexts). As I understand it, it is exactly this issue that causes some to want 'seq' to be a class member from which functions are specifically excluded. Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG

Brian Hulley

5 Apr 5 Apr

10:49 a.m.

Robert Dockins wrote:

...

On Apr 1, 2006, at 3:23 PM, Brian Hulley wrote:

...
[snip] " For particular types T1 and T2, if (f (x::T1))::T2 === g x for all x in T1 then f :: T1->T2 and g ::T1->T2 can be freely substituted since the context T1->T2 cannot tell them apart."

Having thought about this a bit more, I realize that this statement is also too strong. In the lambda calculus, extensionality is equivalent to the validity of eta-conversion (Plotkin, Call-by-value, Call-by-name and the lambda calculus, 1975). However, in Haskell, eta-conversion is not valid (ie, meaning-preserving). Observe:

f, g :: a -> b f = undefined g = \x -> undefined x

forall x::a, f x === g x === _|_. However, 'seq' can tell them apart.

seq f 'a' === _|_ seq g 'a' === 'a'

So f and g are not replaceable in all term contexts (in particular, not in 'seq' contexts).

I should not have used functions, since in any case for full generality rt is about allowing equivalent expressions to be substituted eg as in: "For a particular type T, if f::T === g then f::T and g::T can be freely substituted since the context T cannot tell them apart" This of course begs the question of how === is defined and so perhaps is not that useful. If === must be defined extensionally then not all contexts in Haskell are referentially transparent since seq is referentially opaque, but this would render the whole notion of referential transparency useless for Haskell since there would be no way for a user of a library function to know whether or not the argument context(s) are transparent or opaque. At the moment I can't think of a non-extensional definition for === but there must be one around somewhere so that equational reasoning can be used. Regards, Brian.

Robert Dockins

11:25 a.m.

On Apr 5, 2006, at 10:49 AM, Brian Hulley wrote:

...

Robert Dockins wrote:

...
On Apr 1, 2006, at 3:23 PM, Brian Hulley wrote:

...
[snip] " For particular types T1 and T2, if (f (x::T1))::T2 === g x for all x in T1 then f :: T1->T2 and g ::T1->T2 can be freely substituted since the context T1->T2 cannot tell them apart."

Having thought about this a bit more, I realize that this statement is also too strong. In the lambda calculus, extensionality is equivalent to the validity of eta-conversion (Plotkin, Call-by-value, Call-by-name and the lambda calculus, 1975). However, in Haskell, eta-conversion is not valid (ie, meaning-preserving). Observe:

f, g :: a -> b f = undefined g = \x -> undefined x

forall x::a, f x === g x === _|_. However, 'seq' can tell them apart.

seq f 'a' === _|_ seq g 'a' === 'a'

So f and g are not replaceable in all term contexts (in particular, not in 'seq' contexts).

I should not have used functions, since in any case for full generality rt is about allowing equivalent expressions to be substituted eg as in:

"For a particular type T, if f::T === g then f::T and g::T can be freely substituted since the context T cannot tell them apart"

This of course begs the question of how === is defined and so perhaps is not that useful.

I had in mind "has the same denotational semantics", but the notation is a little sloppy. On the other hand, you could turn the definition around and say that === means two expression which can be freely substituted. To prove properties about ===, you then need to have a very precise definition of the semantics of the programming language. Unfortunately, I don't think Haskell's semantics are developed to quite that point.

...

If === must be defined extensionally then not all contexts in Haskell are referentially transparent since seq is referentially opaque, but this would render the whole notion of referential transparency useless for Haskell since there would be no way for a user of a library function to know whether or not the argument context(s) are transparent or opaque. At the moment I can't think of a non-extensional definition for === but there must be one around somewhere so that equational reasoning can be used.

There is a fair bit of disagreement about what referential transparency means. I found the following link after googling around a bit; it seems to address some of these issues. http://www.cs.indiana.edu/~sabry/papers/purelyFunctional.ps

...

Regards, Brian.

Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG

Josef Svenningsson

12:42 p.m.

Sorry to barge in in the middle of your discussion here.. On 4/5/06, Robert Dockins wrote:

...

There is a fair bit of disagreement about what referential transparency means. I found the following link after googling around a bit; it seems to address some of these issues.

http://www.cs.indiana.edu/~sabry/papers/purelyFunctional.ps

Do you have any reference to the fact that there is any diagreement about the term? I know it has been used sloppily at times but I think it is pretty well defined. See section 4 of the following paper: http://www.dina.kvl.dk/~sestoft/papers/SondergaardSestoft1990.pdf Readers digest: First we need a denotational semantics and a corresponding equality which I call '='. A language is then referentially transparent if for all expressions e,e1 and e2, if e1 = e2 then e[x:=e1] = e[x:=e2]. Here e[x:=e'] denotes substitution where the variable x is replaced with e' in the expression e. So it's a standard substitutivity property. The only problem here is that Haskell has a pretty hairy denotational semantics and I don't think anyone has spelled it out in detail. The thing which I think comes closest is the following paper which investigates the denotational implications of have seq as a primitive: http://www.crab.rutgers.edu/~pjohann/seqFinal.pdf Cheers, /Josef

Robert Dockins

1:06 p.m.

On Apr 5, 2006, at 12:42 PM, Josef Svenningsson wrote:

...

Sorry to barge in in the middle of your discussion here..

Hey, if we wanted a private conversation, we'd take it off-list. :-)

...

On 4/5/06, Robert Dockins wrote:

...
There is a fair bit of disagreement about what referential transparency means. I found the following link after googling around a bit; it seems to address some of these issues.

http://www.cs.indiana.edu/~sabry/papers/purelyFunctional.ps

Do you have any reference to the fact that there is any diagreement about the term? I know it has been used sloppily at times but I think it is pretty well defined. See section 4 of the following paper: http://www.dina.kvl.dk/~sestoft/papers/SondergaardSestoft1990.pdf

http://en.wikipedia.org/wiki/Referential_transparency http://lambda-the-ultimate.org/node/1237 It may be that experts have a well defined notion of what it means, but I think that non-experts (ie, most people) have a pretty vague idea of exactly what it means.

...

Readers digest: First we need a denotational semantics and a corresponding equality which I call '='. A language is then referentially transparent if for all expressions e,e1 and e2, if e1 = e2 then e[x:=e1] = e[x:=e2]. Here e[x:=e'] denotes substitution where the variable x is replaced with e' in the expression e.

So it's a standard substitutivity property. The only problem here is that Haskell has a pretty hairy denotational semantics and I don't think anyone has spelled it out in detail.

I think that may be the main problem, at least in this context. We can take a nice lovely definition of rt, as above, but its meaningless without a good semantic model. So we're forced to approximate and hand-wave, which is where the disagreement comes in.

...

The thing which I think comes closest is the following paper which investigates the denotational implications of have seq as a primitive: http://www.crab.rutgers.edu/~pjohann/seqFinal.pdf

Cheers,

/Josef

Thanks for these paper links; I'll be reading them as soon as I find a few moments. Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG

Josef Svenningsson

6:50 p.m.

On 4/5/06, Robert Dockins wrote:

...

Hey, if we wanted a private conversation, we'd take it off-list. :-)

:-)

...

...
Do you have any reference to the fact that there is any diagreement about the term? I know it has been used sloppily at times but I think it is pretty well defined. See section 4 of the following paper: http://www.dina.kvl.dk/~sestoft/papers/SondergaardSestoft1990.pdf

http://en.wikipedia.org/wiki/Referential_transparency http://lambda-the-ultimate.org/node/1237

It may be that experts have a well defined notion of what it means, but I think that non-experts (ie, most people) have a pretty vague idea of exactly what it means.

The wikipedia article was very enlightening on this subject, especially the disclaimer on the top :-) Thanks!

...

...
So it's a standard substitutivity property. The only problem here is that Haskell has a pretty hairy denotational semantics and I don't think anyone has spelled it out in detail.

I think that may be the main problem, at least in this context. We can take a nice lovely definition of rt, as above, but its meaningless without a good semantic model. So we're forced to approximate and hand-wave, which is where the disagreement comes in.

Yes, I know what you mean. In the last few weeks this legacy of hand-waving has been showing its ugly face on the haskell-prime list as well. Maybe its time to sit down and define properly what we mean in certain contexts. It seems we would need more than one semantics to cover the different ways that reason about Haskell program. Just so that one can say: "Here I'll be using Fast'n-Loose Reasoning(TM)" or "This law holds in the Handwaving Semantics(TM)". The point is to be able to reference these precisely defined approximations and thus enjoying being both sloppy and precise at the same time. But it's real work doing this kind of thing. During a graduate course at Chalmers we started at something like this but it grew pretty hairy pretty quickly. Cheers, /Josef

Claus Reinke

1 Apr 1 Apr

1:57 p.m.

...

However there is nothing in the functions themselves that restricts their use to just T Double. Thus the functions can be compared for equality by supplying an argument of type T Double but used elsewhere in the program with args of type (plain) Double eg: .. Thus we can determine that f is implemented by different code from g (The example would be even more convincing if Int's were used instead of Double's) and so f and g are not interchangeable.

if you have two functions f and g, and an argument applied to which they deliver different results, then the functions can hardly be equal, can they? if they are not equal, what makes you think they should be interchangeable?

...

...
... nothing prevents us from defining that instance in such a way that we construct a representaton instead of doing any additions.

Thus referential transparency of polymorphic functions is foiled.

polymorphic functions (as in: parametrically polymorphic) do not allow such tricks. overloaded expressions are interpreted as functions from type information to non-overloaded expressions, so you have to take that type information into account when comparing or exchanging the expressions. in particular, an overloaded expression instantiated at a particular type is not the same as the overloaded expression itself. btw, you'll notice that I avoid the use of terms like rt - there are too many non-equivalent interpretations of such terms flying around, so it is better to define what it is you're talking about (try this for one study of the many definitions [scanned paper - >3MB]: http://www.dina.kvl.dk/~sestoft/papers/SondergaardSestoft1990.pdf ). cheers, claus

Brian Hulley

4:21 p.m.

Claus Reinke wrote:

...

[snip] ... (try this for one study of the many definitions [scanned paper - >3MB]: http://www.dina.kvl.dk/~sestoft/papers/SondergaardSestoft1990.pdf ).

Thanks for the link, Regards, Brian.

Robert Dockins

12:17 p.m.

On Saturday 01 April 2006 07:50 am, Brian Hulley wrote:

...

Greg Buchholz wrote:

...
Hmm. It must be a little more complicated than that, right? Since after all you can print out *some* functions. That's what section 5 of _Fun with Phantom Types_ is about. Here's a slightly different example, using the AbsNum module from...

http://www.haskell.org/hawiki/ShortExamples_2fSymbolDifferentiation

...
import AbsNum

f x = x + 2 g x = x + 1 + 1

y :: T Double y = Var "y"

main = do print (f y) print (g y)

...which results in...

*Main> main (Var "y")+(Const (2.0)) (Var "y")+(Const (1.0))+(Const (1.0))

...is this competely unrelated?

Interesting! Referential transparency (as I understand it) has indeed been violated. Perhaps the interaction of GADTs and type classes was not sufficiently studied before being introduced to the language.

No, it hasn't -- the waters have just been muddied by overloading (+). You have reasoned that (x + 2) is extensionally equivalent to (x + 1 + 1) because this is true for integers. However, (+) has been mapped to a type constructor for which this property doesn't hold (aside: all sorts of useful algebraic properties like this also don't hold for floating point representations). So, you've 'show'ed two distinct values and gotten two distinct results -- no suprise. The general problem (as I see it) is that Haskell programers would like to identify programs up to extensionality, but a general 'show' on functions means that you (and the compiler) can only reason up to intensional (ie, syntactic) equality. That's a problem, of course, because the Haskell standard doesn't provide a syntactic interpretation of runtime functional values. Such a thing would be needed for runtime reflection on functional values (which is essentially what show would do). It might be possible, but it would surely mean one would have to be very careful what the compiler would be allowed to do, and the standard would have to be very precise about the meaning of functions. Actually, there are all kinds of cool things one could do with full runtime reflection; I wonder if anyone has persued the interaction of extensionality/intensionality, runtime reflection and referential integrity? Rob Dockins

Tomasz Zielonka

1:27 p.m.

On Sat, Apr 01, 2006 at 01:50:54PM +0100, Brian Hulley wrote:

...

Greg Buchholz wrote:

...
...
f x = x + 2 g x = x + 1 + 1

Interesting! Referential transparency (as I understand it) has indeed been violated. Perhaps the interaction of GADTs and type classes was not sufficiently studied before being introduced to the language.

You cal also tell them apart with some built-in Haskell types, try: (f 1e16 :: Double) == g 1e16 You automatically assume that Num operations have some additional properties, but it's not always true. When +, fromIntegral are unknown, you can't be sure that 1 + 1 is the same as 2. I think it is still meaningful to talk about referential transparency if you treat all functions like + and fromIntegral as black boxes. For example, in many programming languages it's not true that let y = f x in (y, y) is the same as (f x, f x) Best regards Tomasz

Lennart Augustsson

5 Apr 5 Apr

3:50 p.m.

Brian Hulley wrote:

...

Greg Buchholz wrote:

...
Hmm. It must be a little more complicated than that, right? Since after all you can print out *some* functions. That's what section 5 of _Fun with Phantom Types_ is about. Here's a slightly different example, using the AbsNum module from...

http://www.haskell.org/hawiki/ShortExamples_2fSymbolDifferentiation

...
import AbsNum

f x = x + 2 g x = x + 1 + 1

y :: T Double y = Var "y"

main = do print (f y) print (g y)

...which results in...

*Main> main (Var "y")+(Const (2.0)) (Var "y")+(Const (1.0))+(Const (1.0))

...is this competely unrelated?

Interesting! Referential transparency (as I understand it) has indeed been violated. Perhaps the interaction of GADTs and type classes was not sufficiently studied before being introduced to the language.

So I'm now just as puzzled as you.

There's no mystery. The + operator used in that example does not obey '1+1=2'. -- Lennart

Christopher Brown

1 Apr 1 Apr

5:22 a.m.

...

Here is another example. Consider two functions f and g which, given the same inputs, always return the same outputs as each other such as:

f x = x + 2 g x = x + 1 + 1

Now since f and g compute the same results for the same inputs, anywhere in a program that you can use f you could just replace f by g and the observable behaviour of the program would be completely unaffected. This is what referential transparency means.

Another example: In haskell the following is true: f x + g x == g x + f x Pure functions in Haskell do not have side effects, so for the same inputs they always give back the same output. This is referential transparency. In a language such as C, which does not have referential transparency, the functions f and g may change x by a side effect and therefore: f x + g x /= g x + f x In C (or a language with side effects). Cheers, Chris. Christopher Brown PhD Student, University of Kent. http://www.cs.kent.ac.uk/people/rpg/cmb21/ cmb21@kent.ac.uk

Tomasz Zielonka

1:33 p.m.

On Sat, Apr 01, 2006 at 11:22:15AM +0100, Christopher Brown wrote:

...

In haskell the following is true:

f x + g x == g x + f x

Be careful, you will get a counter-example from someone. In this example you assume that + is commutative for all types. I don't think that the Haskell 98 report mandates this. One safer example would be: let y = f x in (y, y) == (f x, f x) Best regards Tomasz

Neil Mitchell

7:39 a.m.

...

...
now superShow f /= superShow g, so they are no longer referentially transparent.

OK. I'm probably being really dense today, but where did "g" come from? Nope, I was being super dense, for "g" read "not"...

superShow f = "not" superShow not = "\x -> case x of {True -> False; False -> True}" superShow f /= superShow not

...

And does this loss of referential transparency contaminate the rest of the language, or is this superShow just an anomaly? Once you have any loss of transparency, you loose it totally. You would then have to go about proving that superShow was not called anywhere in the vicinity of the transformation you wish to appy, inlining by the compiler would no longer be safe...

Thanks Neil

Lennart Augustsson

5 Apr 5 Apr

3:45 p.m.

Neil Mitchell wrote:

...

Hi,

First, its useful to define referential transparency.

In Haskell, if you have a definition

f = not

Then this means that anywhere you see f, you can replace it with not. For example

"f True" and "not True" are the same, this is referentially transparent.

Now lets define "super show" which takes a function, and prints its code behind it, so:

superShow f = "not" superShow g = "\x -> case ..."

now superShow f /= superShow g, so they are no longer referentially transparent.

Hence, you have now broken referential transparency.

So you can't show these two functions differently, so what can you do instead? You can just give up and show all functions the same

instance Show (a -> b) where show x = "<function>"

This is the constant definition of show mentioned.

You can be less restrictive than that. The show function can give different results when applied to functions with different types without breaking anything. -- Lennart

Henning Thielemann

1 Apr 1 Apr

2:43 a.m.

On Fri, 31 Mar 2006, Greg Buchholz wrote:

...

In section 5 of _Fun with Phantom Types_, Hinze states...

"Let us move on to one of the miracles of theoretical computer science. In Haskell, one cannot show values of functional types. For reasons of computability, there is no systematic way of showing functions and any ad-hoc approach would destroy referential transparency (except if show were a constant function). For instance, if show yielded the text of a function definition, we could distinguish, say, quick sort from merge sort. Substituting one for the other could then possibly change the meaning of a program."

I find this statement misleading. I do not expect that (2+2::Int) is shown as "2+2", but as "4". Analogously I don't expect 'toLower' to be shown as "toLower". There are certainly several descriptions of the same value, independent from whether the value is a number or a function. So what _is_ a function? A function is a set of assignments from arguments to function values. That is, a natural way to show a function would be to print all assigments. Say Prelude> toLower [('A','a'), ('a','a'), ('1', '1'), ... In principle this instance of 'show' could be even implemented, if there would be a function that provides all values of a type. Another example Prelude> sort :: [Int] -> [Int] [([0],[0]), ([0,1],[0,1], ([1,0],[0,1]), ...

Fritz Ruehr

5:01 a.m.

On Mar 31, 2006, at 11:43 PM, Henning Thielemann wrote:

...

A function is a set of assignments from arguments to function values. That is, a natural way to show a function would be to print all assigments. Say

Prelude> toLower [('A','a'), ('a','a'), ('1', '1'), ...

In principle this instance of 'show' could be even implemented, if there would be a function that provides all values of a type.

You can use type classes to implement this for *finite* functions, i.e., total functions over types which are Enum and Bounded (and Show-able), using for example a tabular format for the show: > putStr (show (uncurry (&&))) (False,False) False (False,True) False (True,False) False (True,True) True It's especially easy to justify showing functions in this context, since one is providing the entire extension of the function (and in a nice canonical order, given the Enum class of the domain type). You can also extend the Enum and Bounded classes to functions over Enum and Bounded types, allowing fun stuff like this: > fromEnum (&&) 4 > (toEnum 4 :: Bool->Bool->Bool) True False False (Unfortunately, although the tabular show style thus extends to higher-order functions, it doesn't work well.) Of course, this is all a bit of a hack, since the straightforward implementation really only accounts for total functions ... . -- Fritz

Fritz Ruehr

3 Apr 3 Apr

6:41 a.m.

I've revised my thinking about printing (total, finite) functions: I should have respected the notion that a printed representation can be cut-and-pasted back in at the prompt for evaluation to something equal to the original. I've also revised my implementation to this effect, so that functions (over suitable classes of types) are now instances of the classes Bounded, Enum, Eq, Ord and Show, with the desired printing, as demonstrated by this session transcript:

...

...
not == not True not == id False id == (not . not) True fromEnum not 1 not == toEnum 1 True not (\x -> case x of False -> True; True -> False) not == (\x -> case x of False -> True; True -> False) True id :: Bool -> Bool (\x -> case x of False -> False; True -> True) const True :: Bool -> Bool (\x -> case x of False -> True; True -> True) (&&) == (&&) True (&&) == (||) False fromEnum (&&) 8 (&&) == toEnum 8 True (&&) (\x -> case x of False -> (\x -> case x of False -> False; True -> False); True -> (\x -> case x of False -> False; True -> True))

The printing is a bit ugly, but it would be somewhat improved in Haskell' if the LambdaCase suggestion is accepted (see http://hackage.haskell.org/trac/haskell-prime/wiki/LambdaCase), i.e., without the arbitrary choice of variable, and slightly shorter representations. Printing of properly higher-order functions doesn't have the nice read-back property, but only because Haskell doesn't support patterns over (suitably finite, total) functions. (One can paste back in the printed rep. for (&&), for example, and successfully compare it to the original, but not something of type (Bool->Bool)->Bool.) I can't imagine I'm the first to play around with this sort of thing, but I wonder why instances like these ought not be included in the Prelude. The functions are treated in a fully extensional manner, so I think it's all quite kosher. The ideas break down for partial functions, of course, but then so do the usual instances for enumerated data types (we can't successfully compare True with undefined, for example). And although the Ord and Enum instances are somewhat arbitrary, they are coherent with each other, generated in a principled fashion and agree with common practices (Ord and Enum for enumerated data types are themselves somewhat arbitrary). I suppose there's an argument from an efficiency perspective, but we don't prevent derivation of Eq for recursive types on the grounds that someone might compare huge trees. Here are the instances used above (well, the headers anyway), including products for good measure:

...

instance (Enum a, Bounded a, Enum b, Bounded b) => Bounded (a->b) where ... instance (Enum a, Bounded a, Enum b, Bounded b) => Enum (a -> b) where ... instance (Enum a, Bounded a, Eq b) => Eq (a->b) where ... instance (Enum a, Bounded a, Enum b, Bounded b, Eq b) => Ord (a -> b) where ... instance (Enum a, Bounded a, Show a, Show b) => Show (a->b) where ... instance (Bounded a, Bounded b) => Bounded (a,b) where ... instance (Enum a, Bounded a, Enum b, Bounded b) => Enum (a,b) where ...

-- Fritz On Apr 1, 2006, at 2:01 AM, Fritz Ruehr wrote:

...

You can use type classes to implement this for *finite* functions, i.e., total functions over types which are Enum and Bounded (and Show-able), using for example a tabular format for the show:

...
putStr (show (uncurry (&&))) (False,False) False (False,True) False (True,False) False (True,True) True

...

Claus Reinke

1 Apr 1 Apr

6:32 a.m.

...

In section 5 of _Fun with Phantom Types_, Hinze states...

"Let us move on to one of the miracles of theoretical computer science. In Haskell, one cannot show values of functional types. For reasons of computability, there is no systematic way of showing functions and any ad-hoc approach would destroy referential transparency (except if show were a constant function). For instance, if show yielded the text of a function definition, we could distinguish, say, quick sort from merge sort. Substituting one for the other could then possibly change the meaning of a program."

that doesn't look up to Ralf's usual standards, but it also looks more like an informal introduction to a section that may explore the issues in more detail. there is no problem in showing functions in general, and the 'show' problem is not specific to functions. there is a problem with converting expressions into representations to be made available to the functional programs from which those expressions came in the first place. functional languages provide many ways of writing expressions with the same meaning, as well as a normalization procedure that attempts to compute a unique normal form for each class of expressions. within such an equivalence class, you have many different representations, all with the same meaning, which is convenient for programming, because you may not know the specific result you are looking for, but perhaps you know that it is equivalent to 'sort [1,5,3,8]'. so you can use any member of the equivalence class to stand for the meaning of expressions in that class, and if we ignore performance, all that matters about an expression is its meaning. if you want to show an expression, you need to evaluate it, then find a representation for its meaning (for functions, perhaps as an enumeration of parameter/result pairs, or a lambda-calculus representation, or a number in an enumeration of all functions of a type, ..). what you cannot do, however, is showing an expression by returning a representation of its current form, because that would allow you to distinguish different members of the same equivalence class, meaning that they wouldn't be equivalent anymore! that holds even for simple arithmetic expressions: "3+2" and "2+3" and "5" are just three ways of writing down the same meaning. if you had a primitive "reify" such that 'reify (3+2) == "3+2"', but 'reify (2+3) == "2+3"', then that primitive wouldn't even be a function - it yields different results for different representations of the same argument! hth, claus

...

...I guess I'm not understanding what that means. Would there be some sort of contradiction that arises when trying to evaluate "show (show)" or somesuch? Can anyone point me in the direction of information that tries to explain why this is? I'm at a loss as to what search terms to use.

Thanks,

Greg Buchholz _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

6988

Age (days ago)

6992

Last active (days ago)

List overview

Download

31 comments

11 participants

participants (11)

Brian Hulley
Christopher Brown
Claus Reinke
Fritz Ruehr
Greg Buchholz
Henning Thielemann
Josef Svenningsson
Lennart Augustsson
Neil Mitchell
Robert Dockins
Tomasz Zielonka