Re: [Haskell-cafe] "show" for functional types

[Josef Svenningsson]

On 4/5/06, Robert Dockins <[EMAIL PROTECTED]> 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] "show" for functional types

[Lennart Augustsson]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] "show" for functional types

[Lennart Augustsson]

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 = ""

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] "show" for functional types

[Robert Dockins]

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 <[EMAIL PROTECTED]> 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



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

Re: [Haskell-cafe] "show" for functional types

[Josef Svenningsson]

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

On 4/5/06, Robert Dockins <[EMAIL PROTECTED]> 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] "show" for functional types

[Robert Dockins]

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



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

Re: [Haskell-cafe] "show" for functional types

[Brian Hulley]

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. 


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

Re: [Haskell-cafe] "show" for functional types

[Robert Dockins]

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

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

Re: [Haskell-cafe] "show" for functional types

[Fritz Ruehr]

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

...


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

Re: [Haskell-cafe] "show" for functional types

[Brian Hulley]

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.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] "show" for functional types

[Brian Hulley]

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. 


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

Re: [Haskell-cafe] "show" for functional types

[Claus Reinke]

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

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

Re: [Haskell-cafe] "show" for functional types

[Robert Dockins]

[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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] "show" for functional types

[Tomasz Zielonka]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] "show" for functional types

[Tomasz Zielonka]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] "show" for functional types

[Brian Hulley]

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. 


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

Re: [Haskell-cafe] "show" for functional types

[Robert Dockins]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] "show" for functional types

[Robert Dockins]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] "show" for functional types

[Brian Hulley]

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


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

Re: [Haskell-cafe] "show" for functional types

[Brian Hulley]

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. 


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

Re: [Haskell-cafe] "show" for functional types

[Claus Reinke]

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

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

Re: [Haskell-cafe] "show" for functional types

[Brian Hulley]

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. 


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

Re: [Haskell-cafe] "show" for functional types

[Neil Mitchell]

> > 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] "show" for functional types

[Claus Reinke]

   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

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

Re: [Haskell-cafe] "show" for functional types

[Christopher Brown]

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/
[EMAIL PROTECTED]



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

Re: [Haskell-cafe] "show" for functional types

[Fritz Ruehr]

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

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

Re: [Haskell-cafe] "show" for functional types

[Henning Thielemann]

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]), ...
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] "show" for functional types

[Greg Buchholz]

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

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

Re: [Haskell-cafe] "show" for functional types

[Brian Hulley]

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. 


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

Re: [Haskell-cafe] "show" for functional types

[Greg Buchholz]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] "show" for functional types

[Neil Mitchell]

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 = ""

This is the constant definition of show mentioned.

Thanks

Neil

On 4/1/06, Greg Buchholz <[EMAIL PROTECTED]> 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
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] "show" for functional types

[Greg Buchholz]

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