[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