[Haskell-cafe] "show" for functional types
robdockins at fastmail.fm
Sat Apr 1 12:17:25 EST 2006
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?
More information about the Haskell-Cafe