[Haskell-cafe] New to Haskell
Benja Fallenstein
benja.fallenstein at gmail.com
Tue Dec 18 12:31:04 EST 2007
On Dec 18, 2007 6:01 PM, Paul Hudak <paul.hudak at yale.edu> 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
More information about the Haskell-Cafe
mailing list