Re: [Haskell-cafe] Wincomplete-uni-patterns and bidirectional patterns
I think the completeness checker works fine in all pattern-synonym-free cases, i.e. when you're using only real constructors.
One can envision a simple recursive divide-and-conquer algorithm, see below.
I don't actually understand why completeness
annotations are needed for pattern synonyms.
I remember reading somewhere, but I can't find it now, that GHC's coverage checker does not look inside pattern synonym definitions at all, and this is by design: namely to ensure abstraction boundaries. Looking inside the definition would mean that type checking behaviour (in a way -- if you count coverage checks as "type checking") of user code is influenced by invisible implementation details of the "constructors" they're using.
Compare that to 'type' versus 'newtype' on the type level: A type is just an alias, a synonym. The type checker has access to all information on the right hand side of the equality. With extensions like TypeSynonymInstances, A type alias is interchangeable with the aliased type. If what you report is true, they should not have called pattern synonyms a "synonym".
My own thoughts on this: if GHC would look inside pattern synonym definitions, then it would be hard to ensure that GHC thinks that certain things are _not_ complete even if technically they are. For example, if you have a data type with, say, 3 constructors, but you hide some of those (don't export them) and use pattern synonyms to make it look like 4 constructors, then you might want GHC's coverage checker to consider that a data type with 4 constructors, not one with 3. COMPLETE pragmas add "positive" information -- "this set is complete, in addition to whatever other complete sets GHC might already know" -- and there is no way to _subtract_ complete sets from GHC's knowledge base.
This is mostly me theorising, but perhaps it helps.
- other Tom
I don't think the number of constructors/patterns is the issue. Likely the problem lies in the fact that while ordinary constructors make up disjoint subsets of the type, with patterns you can define overlapping sets, which makes completeness checks much more complicated. Hence I believe that completeness checks in presence of patterns is equivalent to determine whether a disjunction of logic formulae, which are possibly self-referential, is a tautology. That may well be semi- decidable at best. Olaf
On Tue, Jan 16, 2024 at 04:16:26PM +0100, Olaf Klinke wrote:
I remember reading somewhere, but I can't find it now, that GHC's coverage checker does not look inside pattern synonym definitions at all, and this is by design: namely to ensure abstraction boundaries. Looking inside the definition would mean that type checking behaviour (in a way -- if you count coverage checks as "type checking") of user code is influenced by invisible implementation details of the "constructors" they're using.
Compare that to 'type' versus 'newtype' on the type level: A type is just an alias, a synonym. The type checker has access to all information on the right hand side of the equality. With extensions like TypeSynonymInstances, A type alias is interchangeable with the aliased type. If what you report is true, they should not have called pattern synonyms a "synonym".
Ah, they should be newpatterns!
On Tue, Jan 16, 2024 at 04:16:26PM +0100, Olaf Klinke wrote:
I don't think the number of constructors/patterns is the issue. Likely the problem lies in the fact that while ordinary constructors make up disjoint subsets of the type, with patterns you can define overlapping sets, which makes completeness checks much more complicated. Hence I believe that completeness checks in presence of patterns is equivalent to determine whether a disjunction of logic formulae, which are possibly self-referential, is a tautology. That may well be semi- decidable at best.
That seems plausible, but I think that interface stability is a more serious concern. It isn't enough to know that *as-implemented* at a given time some particular set of patterns is complete. The implementation of a set of patterns (or the underlying type) can change in a manner that changes complete <-> incomplete in either direction. Such changes are non-breaking, provided there was no "contract" (COMPLETE pragma) that the patterns are *intended* to be complete. Initially: data Foo = A | B pattern Good :: Foo; pattern Good = Foo A pattern Bad :: Foo; pattern Bad = Foo B Later: data Foo = A | B | C pattern Good :: Foo; pattern Good = Foo A pattern Bad :: Foo; pattern Bad = Foo B Later still: pattern Ugly :: Foo; pattern Ugly = Foo C All fine, if there was no expectation that "Good, Bad" is a COMPLETE set. Such completeness is a matter of interface contract (design intent), and cannot be derived. -- Viktor.
participants (3)
-
Olaf Klinke -
Tom Ellis -
Viktor Dukhovni