By focusing on FP nomenclature (whether an exception is regarded as "divergence" or not depends on your language -- note that I said "terminates"; the point is that the trace for each execution is finite) you're missing the issue, that exists regardless of language.
> It does, because foo does.
`foo bar` never crashes (unless I made some silly bug).
The term "diverge," when applied to an exception, is not a computational term but a term from a specific formalism (e.g.: Haskell). A computation is a sequence of states; if it ever reaches a terminal state (i.e., a state from which it cannot exit), it is said to terminate. You can apply the terms converge/diverge to termination/non-termination, but once you speak of exceptions, you're using a language-specific terminology.
> if you could prove that both functions always return some value then you can also say that composing them will always return some value
Yes, but that would be too hard. `foo` doesn't always return a value, but `foo bar` does. What can you prove about `foo` and `bar` separately that would make proving that easier, not harder?
A function that is non-partial is, in standard maths parlance, a total function https://en.wikipedia.org/wiki/Partial_function#Total_functio...
Such terms are certainly used in that sense by PLs eg in scala Function and PartialFunction types exist with those intended semantics, and it seems haskell recognises the terminology https://wiki.haskell.org/Partial_functions (though whether it supports them in the language definition or libraries I don't know).
@pron then makes an apparently incorrect claim which I dispute to try to help clarify. That's clarification not nitpicking (I intended that way anyway). @pron's point may be valid but if we don't have common meanings to words, this will go nowhere.
which word?
> I said that both subroutines "terminate". That is a word with a precise meaning in computation
I'd say so. But here's a clip from previous:
> zopa 23 hours ago :- How is `foo` "clearly terminating"? With `p = const False`' it's undefined for any even x >= 3.
-and you say-
> pron 23 hours ago :- It would terminate with an exception.
So you're claiming that 'terminating with an exception' is termination "with a precise meaning in computation". But that's a bloody strange definition I have never come across.
In fact it's so weird I had trouble finding a definition because it seems so fundamentally bizarre that nobody I've ever met has ever considered throwing an exception (or similar) due to precondition violation to be termination. But here goes:
1943: In a paper, Stephen Kleene states that "In setting up a complete algorithmic theory, what we do is describe a procedure ... which procedure necessarily terminates and in such manner that from the outcome we can read a definite answer, 'Yes' or 'No,' to the question, 'Is the predicate value true?'."
That from https://en.wikipedia.org/wiki/Halting_problem
So yes termination is defined and no it's not what you claim it is. No wonder people are getting confused.
as for... (edit: deleted this as poster accidentally linked to wrong comment)
I don't know what else I can say. Exceptions are not a computational concept, they're a language concept. The computation terminates in some well-defined state. That the language declares that that well-defined state is not considered a value is a language-specific thing.
> So yes termination is defined and no it's not what you claim it is.
It is exactly what I defined, as your quote shows. Termination and decision are not the same thing. Imagine that the decider could terminate with, Yes, No, or Error. It would still not be a decision procedure, but it is very much termination. And your very quote says exactly that when it says "terminates and in such manner that..."? If termination already means that it is in such manner, why is the qualification necessary?
Your definition of termination (to mean anything other than reaching a terminal state after a finite number of steps) is based on the fact that in a particular formalism, the lambda calculus, termination yields a normal form. Now, the lambda calculus doesn't have exceptions, and so every lambda term either reduces to a normal form or the reduction never terminates, but a language like Haskell adds a third possibility. Because Haskell draws inspiration from the lambda calculus, it's easier, in the discussion of Haskell, to map exceptions -- which don't yield a normal form but do terminate at a definite computational state -- to the same notion of divergence, that, in the lambda calculus, is synonymous with termination, but in Haskell it isn't. So I wouldn't be surprised if some people took it further, and used termination to be synonymous with "produces a normal form" in Haskell. But, again, this is not how the notion of termination is commonly defined in computation (many notions of computations don't even have the concept of a normal form or of a value). In Java, for example, where the denotation of a subroutine isn't similar to a partial function but is, rather, a predicate transformer, an exception and a return value are equally valid results.
But yeah, I agree that selling Haskell as maths, does tend to confuse, and so people can mistakenly think that Haskell terminology is canonical mathematical or computer-science terminology. And yeah, it is sometimes frustrating to speak with those who are only familiar with the mathematics of functional programming and not with the mathematics of imperative programming, or with the theory of computation in general, and so don't even know which terms are overloaded and which are canonical.
All of this, however, is so irrelevant to the point of my `foo bar` example (namely, that knowing things about components does not mean you can feasibly know things about their composition) that it's ridiculous.
> Yep, and that reply was posted 10 minutes before you referred to it.
OMG, I linked to that one because I had just written it and it was right in front of me. Here is the same answer in an older comment: https://news.ycombinator.com/item?id=20715970
So not only are you determined to focus on something that is entirely beside the point because you've completely missed the point, you are also wrong in the side-track you've chosen.
> Imagine that the decider could terminate with, Yes, No, or Error.
That's just not how it works. Mathematically a function, if it terminated, terminates with an answer. There is no error - the precondition of the function states what is acceptable and the function must come back with an answer (or possibly not terminate, but that's another thing). That's why the quote from Stephen Kleene[0] didn't mention errors.
If I want to define a function computing real-number square root, I set as a precondition that negative numbers must never be passed to it. That's it. That's the precondition - "this and only this is acceptable to this bit of code" is what it means.
In any language an exception should happen if you violate that ie. pass in a negative number. That may show up as an exception. But you don't want exceptions! Which is why you try to formally guarantee the precondition is met! So You are guaranteed of an answer (leaving aside non-termination).
All this formal stuff (at least in my world) is about verifying the code conforms to the precondition such that an error will never occur (edit: wrong, it's more than verifying to the precondition but go with it for now) . Also verifying that if the precondition is verified that termination will happen.
Put another way, taking the head of an empty list is meaningless, so you set the precondition (edit: of the function hd())to be that always
is_not_empty(lst)
If any program was entirely verified thus then no exceptions would be needed because the program would be correct (excluding resource exhaustion on our regrettably finite computers).
> Termination and decision are not the same thing.
Mathematically if it terminates, it decides. If it decided then it has terminated. Yes they are the same thing. That's what the quote says. Termination via exception is not in that world: "in such manner that from the outcome we can read a definite answer". Blowing up without deciding would mean termination (an exception in your terms) without providing yes/no. Useless.
I'm pretty weak in this area but I do know the basics, and it does not come across that you do.
> OMG, I linked to that one...
No probs, I edited out that.
[0] Heh, same kleene after whom was named the kleene star in regexes. Who know.
There is no such thing for a mathematical function to "terminate." In classical mathematics, a function is a one-valued relation, a set of pairs, if you like. There is no algorithm and no computation involved. Termination is a computation term. Divergence is a formalism-specific.
But now coming back to your original point and example: I don't think anyone from the Haskell and ML-family languages camp is claiming one can automatically deduce every possible decidable property from any function with their type system, or at least not yet :)
I don't think anyone claims that any property can be proven. I do think that some think that if a program can be decomposed into simple parts, whose "interesting" properties are provable in isolation, then you can feasibly prove interesting properties of their composition, which is not true. A proof of that was only given in the past 10-15 years, and is referenced in my post.
Like many things in mathematics, the term has been borrowed and changed. Look, for example at "function". Do you think "function" in programming (even in Haskell) means the exact same thing as in mathematics?
In general, partial functions mean that for some values, a function is undefined. But in a PL nothing is undefined. In some cases there would be an exception; in others the subroutine would loop forever. But a language like Haskell, because it wants its "functions" to resemble mathematical functions, declares that those perfectly normal computational behaviors correspond to "undefined". In imperative languages, where subroutines don't try to correspond to (partial) functions, throwing an exception does not correspond to undefined.