On Tue 28 Sep, S. Alexander Jacobson wrote:
> PS Martin, if your comments come with an implied smirk, then I apologize
> for my lack of sense of humor
I don't think Martin was smirking. I think he was serious, and I agree with
him. I really don't think you can use type theoretical arguments discount
this. The fact that evaluation of some expressions will fail to terminate
(either by accident or design), so if the language is to be properly
specified _|_ must be considered, ugly as that is.
And I don't think that _|_ is ill typed. Haskell can infer types for
expressions (including _|_) without evaluating them. Type checking
wouldn't be much use otherwise. So you could say that the type of any
occurence of _|_ is the same as the corresponding expression.
Martins example..
bottom :: a
bottom = bottom
or perhaps..
bottom :: Bool
bottom = not bottom
> My simple point is that claims about the correctness or incorrectness of
> the behavior of a function are incoherent outside the function's domain;
But what is that domain? (see below)
> that, as an language implementation matter, it is handy to make _|_ a
> member of all types is irrelevant.
I don't think it's necessary to make it a member of all types (though
it may be convenient). Instead you could have separate _|_'s for every
type if you prefer.
> Haskell's (&&) only models the logical AND when it is passed booleans.
> To say that _|_ is a Haskell Boolean, is to create another concept domain
> (Haskell Boolean), which shares many properties with Logic Boolean but is
> not identical with it.
Yes, I suppose I agree here (see below).
> Understood in this manner, I don't think Parallel Haskell implementations
> need to make any promises about the sanity of the behvaior of functions
> when passed _|_.
I think they do, at least if they claim to be Haskell they must all make
the same promise, sane or otherwise :-)
(If they don't they aren't Haskell, they're different languages which
just happen to have the exactly the same syntax and type system as
Haskell.)
E.G.
That promise could be that any expression containing _|_ is also _|_.
This is straight forward strict semantics. But to fullfill that promise
every expression must be evaluated, so lazyness is lost. So lazy languages
need to make some other promise, I think. It would be helpful to understand
what that promise is.
> As a practical matter, it would be nice if
> program success/failure was consistent accross Haskell implementations,
> but this does not require that functions behave in any particularly sane
> manner when passed _|_, only that they behave consistently.
Yes, this is precisely the point I think, they do have to behave
consistently (if not sanely). But to get this consistency you have to
clearly differentiate legal program transformations from illegal ones (I.E.
transformations which modify termination properties). To do this _|_
_has_ to be considered. If this isn't so then you'll end up with an
incompletely specified language in which some programs will work or
not depending on which compiler you use.
** Health Warning **
What follows is my own extemely humble opinion which could well be wrong
------------------------------------------
Why I think we can't ignore _|_
------------------------------------------
I wrote:
> Is a function..
>
> 1- A mapping between input values and output values (which don't include
> _|_). I imagine this is what mathematicians would call a function.
>
> or..
>
> 2- A method of computation. For all its abstraction, as far as Haskell
> is concerned this has to be the correct way to view a function. This
> is what makes Haskell a _programming_ language, rather than a tool
> for reasoning about the properties of functions.
Perhaps to be clear, I should use different terminology for these 2
views, so..
A 'function' is a mathematicians mapping between input and output
values.
and..
A 'function method' is a method of computation (a bit of Haskell code say).
I could say that a function_method correctly implements a function if
for all arguments other than _|_ the function method returns the same
value that a mathematician would obtain using a mapping, such as a
look up table (which may be infinite).
I could also say that it is also possible to for 2 different
function_methods to correctly implement the same function, even if
they differ in their behavior wrt an argument of _|_. But this doesn't
make the 2 function methods equivalent.
I've been a little worried (and I'm probably not alone) that there is
a danger in trying to make optimising compilers too smart. How much
liberty should compilers have to mangle programs before the meaning
of a programmers source is lost. I.E. Before the executable code is
no longer implementing the same method as that chosen by the programmer.
(I think it's important that ultimately programmers should have control
of function methods, not compilers). In short, it's important that
the function method implemented by a compiler is 'equal' to that
chosen by the programmer, including it's behavior regarding undefined/
unevaluatable expressions (_|_) as an argument.
The problem with this approach is that many useful transformations which
a mathematician might use when considering function equality are invalid
when considering function method equality.
So what interests me is..
Is there a realisable (non-strict) evaluation strategy for which all
mathematicians function transformations are also valid function method
transformations?
and..
If such a strategy exists, how awkward is it to implement.
The reason this interests me is that we can settle all arguments
regarding wether or not _|_ should be considered. If it makes
no difference to legality of transformations, then who cares?
I don't know the answer, perhaps someone else does.
Perhaps someone has proven that no such strategy exists.
Perhaps mathematicians can't even agree on what a valid function
transformation is.
What I do know (I think:-) is that current Haskell semantics don't
have this desirable property. But strict semantics do, I think.
In my humble opinion the kind of concurrent semantics I mentioned
certainly allow more freedom in function method mangling, but to
write them into Haskell would require all Haskell implementations
to implement such concurrency (otherwise the behaviour of Haskell
programs would be inconsistent with Haskell semantics).
Regards
--
Adrian Hey
