On Dec 18, 2007 6:01 PM, Paul Hudak <[EMAIL PROTECTED]> wrote: > Well, my caveat was that the Haskell designers wanted it this way. So > you are essentially rejecting my caveat, rather than creating a new one. > :-)
I mean, I reject the answer "They wanted it this way" because I think the answer should be, "They wanted it this way because They looked at substituting equals under a lambda, and They saw it was good" ;-) > > Caveat one, there may be useful ways to for functions to implement > > Show that don't conflict with extensionality (i.e., the property that > > two functions are equal if they yield the same results for all > > inputs). > > > Sure, and I suppose one way to do this is to put the show function for > functions into the IO monad -- then you can't inspect the results. But > if you want to inspect the result, then I have no idea how to do this. If you can show and enumerate the argument type and show the result type of a function, one way is to enumerate the graph of the function. The wiki page gives the example, Prelude> \x -> x+x functionFromGraph [(0,0), (1,2), (2,4), (3,6), Interrupted. If you have special compiler support, and consider a fragment of Haskell that contains only functions -- i.e., no algebraic data types, no Ints etc. (it's kind of a boring fragment!, but you can have Church numbers) --, you can reduce the function to head normal form. Head normal form looks like this: \VAR1 VAR2 ... VARm -> VARi EXPR1 ... EXPRn and there is a reduction strategy that finds the head normal form of an arbitrary expression if there is one; a proof that if there isn't one, the expression denotes bottom; and a proof that if you have two HNFs, and they differ in the part before EXPR1 or differ in the number of EXPRjs, these HNFs denote different values. Therefore, when you have reduced the function to HNF, you can print "\VAR1 VAR2 ... VARm -> VARi " (or more precisely, you can write a lazy 'show' that yields the above characters as soon as it has computed the HNF). Then, you go on to recursively compute the HNF of EXPR1, and you show that inside parantheses. Some examples: show (\x -> x) == "\a -> a" show (.) == "\a b c -> a (b c)" (let fix f = f (fix f) in show fix) == "\a -> a (a (a (a (a................. [Unless I'm making some stupid mistake] It's well-established that this is computable and doesn't break extensionality (i.e., that applying this show to two functions with the same extension will give the same result -- or conversely, if show gives different results for two functions, there are arguments for which these functions yield different results). By itself, this isn't very interesting, but I *think* you should be able to add algebraic data types and case expressions to this fragment of Haskell and still do "essentially" the same thing. Then, you could show, for example, show either == "\a b c -> case c of { Left d -> a d; Right e -> b e }" - Benja _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe