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