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