Re: [Haskell-cafe] if-then without -else?

Therefore (if False then a) would give an exception.
Yes. And the question is, why is possible to write this program using "case" but not with "if". For the first part (allow incomplete sets of patterns in "case"): No matter how hard we try, Haskell is not a total language - there'll always be programs that denote bottom, by raising exceptions (e.g., from incomplete patterns), or by non-termination - which cannot be prohibited statically if we want both the language to be Turing complete, and type inference to be decidable. Cf. Agda, which is total, and therefore has a coverage checker (for patterns) as well as a termination checker. But then the second part (do not allow incomplete "if") appears to be an inconsistency in the design. Mind you - I don't propose to change this. The question is just about justification for the design. Are there applications for an incomplete "if"? I can imagine something like assertions, as in "f x = if some-precondition x then some-computation x" Of course, that's only helpful if the exception contains source information. - J.W.

In hindsight, maybe non-exhaustive case expression should be errors, not warnings. But then adding new constructor to the type could break existing code in multiple places, even if constructor is never used. Not everybody ready to pay this price. For the "if" expressions, condition type is always Bool with two constructors, so enforcing totality looks like natural choice here. On Mon, Jul 9, 2018 at 2:40 PM Johannes Waldmann < johannes.waldmann@htwk-leipzig.de> wrote:
Therefore (if False then a) would give an exception.
Yes. And the question is, why is possible to write this program using "case" but not with "if".
For the first part (allow incomplete sets of patterns in "case"):
No matter how hard we try, Haskell is not a total language - there'll always be programs that denote bottom, by raising exceptions (e.g., from incomplete patterns), or by non-termination - which cannot be prohibited statically if we want both the language to be Turing complete, and type inference to be decidable.
Cf. Agda, which is total, and therefore has a coverage checker (for patterns) as well as a termination checker.
But then the second part (do not allow incomplete "if") appears to be an inconsistency in the design.
Mind you - I don't propose to change this. The question is just about justification for the design.
Are there applications for an incomplete "if"? I can imagine something like assertions, as in "f x = if some-precondition x then some-computation x" Of course, that's only helpful if the exception contains source information.
- J.W. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

If-without-else implies “empty-else”. It’s possible in monad context in “return ()” form. There are “when”, “unless” functions already. But in pure context “empty-else” can not imply empty result for “else” branch (what value should be used in “else” branch?). Empty-if exists in most languages in statements, i.e. under “IO a”, but not in expressions, so “a ? x : y” in C/C++, “x if a else y” in Python needs “else” branch. Non-exhaustive case is like “if ... then ... else undefined” IMHO.
From: Olga Ershova
Sent: 9 июля 2018 г. 21:55
To: Johannes Waldmann
Cc: Haskell Cafe
Subject: Re: [Haskell-cafe] if-then without -else?
In hindsight, maybe non-exhaustive case expression should be errors, not warnings. But then adding new constructor to the type could break existing code in multiple places, even if constructor is never used. Not everybody ready to pay this price.
For the "if" expressions, condition type is always Bool with two constructors, so enforcing totality looks like natural choice here.
On Mon, Jul 9, 2018 at 2:40 PM Johannes Waldmann
Therefore (if False then a) would give an exception.
Yes. And the question is, why is possible to write this program using "case" but not with "if". For the first part (allow incomplete sets of patterns in "case"): No matter how hard we try, Haskell is not a total language - there'll always be programs that denote bottom, by raising exceptions (e.g., from incomplete patterns), or by non-termination - which cannot be prohibited statically if we want both the language to be Turing complete, and type inference to be decidable. Cf. Agda, which is total, and therefore has a coverage checker (for patterns) as well as a termination checker. But then the second part (do not allow incomplete "if") appears to be an inconsistency in the design. Mind you - I don't propose to change this. The question is just about justification for the design. Are there applications for an incomplete "if"? I can imagine something like assertions, as in "f x = if some-precondition x then some-computation x" Of course, that's only helpful if the exception contains source information. - J.W. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

On 2018-07-09 12:54 PM, Olga Ershova wrote:
In hindsight, maybe non-exhaustive case expression should be errors, not warnings. But then adding new constructor to the type could break existing code in multiple places, even if constructor is never used. Not everybody ready to pay this price.
You make a good point, and this is the best explanation I've seen in this discussion. However, even if the constructor is never used in your own code, it may well be used in library code that you call. I think it's dangerous for for the programmer not to know when a new constructor is added. I prefer to have this warning enabled, and my policy is to use -Wall -Werror from the start of any new project. I then turn off specific warnings (eg orphans) with a pragma in individual source files when I really need to use something. I was interested to see that GHC allows you to turn any warning into an error, so I assume Haskell could be made total for pattern matching with: -Werror=incomplete-patterns

On Mon, Jul 09, 2018 at 08:39:49PM +0200, Johannes Waldmann wrote:
Therefore (if False then a) would give an exception.
Yes. And the question is, why is possible to write this program using "case" but not with "if".
Because the error conditions around case were badly designed. My understanding is that a large majority of Haskell developers believe that it should not be possible to omit a branch in a case statement.
participants (5)
-
Johannes Waldmann
-
Neil Mayhew
-
Olga Ershova
-
Paul
-
Tom Ellis