<div dir="ltr">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.<br><br>For the "if" expressions, condition type is always Bool with two constructors, so enforcing totality looks like natural choice here.</div><br><div class="gmail_quote"><div dir="ltr">On Mon, Jul 9, 2018 at 2:40 PM Johannes Waldmann <<a href="mailto:johannes.waldmann@htwk-leipzig.de">johannes.waldmann@htwk-leipzig.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">> Therefore (if False then a) would give an exception.<br>
<br>
Yes. And the question is, why is possible to write<br>
this program using "case" but not with "if".<br>
<br>
For the first part (allow incomplete sets of patterns in "case"):<br>
<br>
No matter how hard we try, Haskell is not a total language -<br>
there'll always be programs that denote bottom,<br>
by raising exceptions (e.g., from incomplete patterns),<br>
or by non-termination - which cannot be prohibited statically<br>
if we want both the language to be Turing complete,<br>
and type inference to be decidable.<br>
<br>
Cf. Agda, which is total, and therefore<br>
has a coverage checker (for patterns)<br>
as well as a termination checker.<br>
<br>
But then the second part (do not allow incomplete "if")<br>
appears to be an inconsistency in the design.<br>
<br>
Mind you - I don't propose to change this.<br>
The question is just about justification for the design.<br>
<br>
Are there applications for an incomplete "if"?<br>
I can imagine something like assertions,<br>
as in "f x = if some-precondition x then some-computation x"<br>
Of course, that's only helpful if the exception<br>
contains source information.<br>
<br>
- J.W.<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>