4 ms·
The fact that most dependently typed languages (which have a much higher propensity for complicated exhaustiveness checking when pattern matching) don’t use a s
by johncolanduoni 5y ago
The fact that most dependently typed languages (which have a much higher propensity for complicated exhaustiveness checking when pattern matching) don’t use a serious SAT solver for this makes me doubt Rust would ever need to.
- sanity31415 5y agoDoesn't Liquid Haskell[1] use a SAT solver? [1] https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/
- johncolanduoni 5y agoLike most languages with refinement types it uses an SMT solver (a more general problem), though I’m not sure it uses it for pattern matching. I was thinking of Coq, Agda, Lean, etc. which are full-spectrum dependently typed languages. LiquidHaskell is more specialized, though its automated proof capabilities are much stronger.
- naasking 5y agoDependent typing goes beyond SMT and SAT, so those languages wouldn't be able to leverage those solvers except in specific circumstances. See the language F* [1], for instance. [1] https://www.fstar-lang.org/ https://www.fstar-lang.org/
- johncolanduoni 5y agoIt’s easy to embed the exact problem Rust has to solve for exhaustiveness checking into e.g. Lean’s pattern matching so they have the same opportunity to use SAT for such checks at least for some set of pattern matching situations (though as I said doubt it would be worthwhile). Using SMT for refinement types like F* does is mostly orthogonal to the problem this article is talking about, which arises just from structural pattern matching.