"show" for functional types

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

"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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "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 = "<function>"

This is the constant definition of show mentioned.

Thanks

Neil

On 4/1/06, Greg Buchholz <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "show" for functional types

Henning Thielemann
In reply to this post by Greg Buchholz

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "show" for functional types

C.M.Brown
In reply to this post by Brian Hulley
>
> 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/
[hidden email]



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

Re: "show" for functional types

Claus Reinke
In reply to this post by 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."

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

Re: "show" for functional types

Neil Mitchell
In reply to this post by Greg Buchholz
> > 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "show" for functional types

Brian Hulley
In reply to this post by Greg Buchholz
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "show" for functional types

Bugzilla from robdockins@fastmail.fm
In reply to this post by Brian Hulley
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "show" for functional types

Bugzilla from robdockins@fastmail.fm
In reply to this post by Brian Hulley
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "show" for functional types

Tomasz Zielonka
In reply to this post by Brian Hulley
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "show" for functional types

Tomasz Zielonka
In reply to this post by C.M.Brown
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: "show" for functional types

Bugzilla from robdockins@fastmail.fm
In reply to this post by Brian Hulley
[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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
12