> > All (all?) I'm proposing is to print them out.
>
> Yes we do, and it's fine for the *implementation* to print such things out.
> But it is NOT fine to cross the dividing line of (1) the implementation, and
> (2) the language it implements. As I believe I have made abundantly clear
> a showFun function which exists *within* the language destroys many of our
> reasoning properties.
[and, taken out of order:]
> Now of course, when we look on the calculus *from the outside* then we can
> see into the internal structure of terms. So looking from the outside gives
> a richer view than looking in. So as I said before, it *is* ok for an
> implementation to provide information about the structure of closures
> etc., but it must not be done via a showFun function within the language.
I find this somewhat puzzling. Why should a function, showFun, that
returns a representation of a function be any more fatal to reasoning
properties than a function that returns sentences from War and Peace?
> [...]
> Let's go back to the lambda calculus again. Here are some lambda terms
> which we may hope exist within the calculus. I state their defining
> property and whether such a term exists or not. The properties are
> universally quantified over ALL lambda terms E.
>
> a E = E Yes
> b [E] = [E] Yes
> c [E] = E Yes
> d E = [E] NO
>
> It's not that I am being restrictive, or hooked on semantics, or anything
> like that. It is simply a matter that no such lambda term exists. Try to
> write one if you like.
I suspect that the problem is that the operation is being described as
E -> [E]. If you think of it as returning a useful representation,
interpretation up the the user, what's the problem?
Note that I'm not saying showFun is a desirable addition to the
language. There may be many (other) reasons for thinking it isn't.
-- jd
