3 ms·
The blog author mentions at one point that Algebraic Data Types cannot determine pattern exaustiveness for things like match 100 { y if y > 0 => “p
by ufo 11y ago
The blog author mentions at one point that Algebraic Data Types cannot determine pattern exaustiveness for things like
match 100 {
y if y > 0 => “positive”,
y if y == 0 => “zero”,
y if y < 0 => “negative”,
};
and wonders if there is some kind of "algebraic data values" to notice that the previous case is exaustive.
In Haskell they solve this particular problem with an "Ordering" ADT:
data Ordering = LT | EQ | GT
case (compare 0 100) of
LT -> "Positive"
EQ -> "Equal"
GT -> "Negative"
Using a richer datatype instead of boolean predicates solves most problems. For some more advanced things you need extensions to the type systems. For example, to be able to say "this function, when applied to non-empty lists returns non-empty lists", you need Generalized Algebraic Data Types (gadts).
- pcwalton 11y agoSame in Rust: http://doc.rust-lang.org/std/cmp/enum.Ordering.html http://doc.rust-lang.org/std/cmp/enum.Ordering.html
- Veedrac 11y agomatch 100.cmp(&0) { Ordering::Greater => "positive", Ordering::Equal => "zero", Ordering::Less => "negative", }
- steveklabnik 11y agoTo elaborate a bit further, the reason that the original isn't exhaustive is that to know that, you would have to execute arbitrary code at compile time, the 'if'. The exhaustiveness check is only on the `y` part of the pattern.
- viraptor 11y agoIsn't this possible for some limited cases? I mean, if you only match on the integer value, this case is trivial. Similar cases are already analysed by gcc to tell you "this comparison is always true/false". I know it doesn't generalise and it "is it worth doing" may be a question, but it seems like most match blocks would fall easily under a very limited set of known cases.
- pcwalton 11y agoYes, it is possible for some cases—this is dependent types' bread and butter—but having an analysis in the type system that sometimes falls down in complex cases tends to lead to frustrating type errors, because it'll refer to types and constraints that the you didn't type and the compiler inferred. If we really wanted to go down this road, we would probably want to add real dependent types to Rust and surface them in the type grammar. (I personally think Rust 1.0 has spent its complexity budget, though, and I'd rather have HKT first in any case.) It's the same reason why we don't adopt a Nim-like "disjointness analysis" that can reason about arithmetic (as mentioned in the article).