[Haskell-cafe] Wincomplete-uni-patterns and bidirectional patterns

[Olaf Klinke]

> > 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.
> 

You are right: It is possible that the types of the bidirectional
patterns do not change, but the completeness changes. In your example
given I would argue the contract is broken, because the new patterns
are for a different type Foo. Instead

-- before: Good, Bad are complete
data Foo = A | B

pattern Good :: Foo
pattern Good = A

pattern Bad :: Foo
pattern Bad = B

-- after: Good, Bad are incomplete
-- Foo, Good as before

pattern Bad = A

Here neither the definition of Foo nor the types of Good or Bad have
changed, but completeness has.

Here is why I think that completeness checks even with pattern synonyms
should work and we would not need COMPLETE pragmas. The algorithm for a
set of patterns of type T is:
1. Construct a Stone [1] space X from the given type T. (Often X = T)
2. Translate each pattern to a clopen of that Stone space
3. Use Stone duality to translate coverage into a Zeroth-order logic
problem, which is decidable.

Let us define an equivalence relation on the elements of a type. Say
x~y whenever there is no pattern that can distinguish x and y by
pattern match. Notice that any pattern partitions the set of
equivalence classes into two disjoint subsets, think of isJust or
isNothing. In general, given a pattern Pat for type T, write

isPat :: T -> Bool
isPat x = case x of
    Pat -> True
    _ -> False

For functions types, there is only one equivalence class, because there
is only one way to pattern-match a function. Observe that two elements
can be distinguished by a set of patterns if and only if there is one
element in the pattern set that already distinguishes them. Do pattern
synonyms refine the equivalence relation induced by ordinary
constructors? No. Consider

type Clopen x = x -> Bool

data C = L C | R C

cl :: Clopen C
cl = isL . shift where
 isL :: Clopen C -- a pattern
 isL (L c) = True
 isL (R c) = False
 shift :: C -> C
 shift (L c) = c
 shift (R c) = c

Can one define a single pattern synonym

pattern CL :: C -> C

such that CL matches c if any only if cl c == True?
Note that cl is the disjunction of two ordinary patterns, namely 
L (L _)
R (L _)
CL morally should be the pattern (_(L _)) but that is not valid pattern
syntax. Indeed with synonyms we can define the CL pattern:

{-# LANGUAGE PatternSynonyms, ViewPatterns #-}
swap :: C -> C
swap (L (R c)) = R (L c)
swap (R (L c)) = L (R c)
swap c = c

pattern CL c <- (swap -> L c)

isCL :: Clopen C
isCL c = case c of
 CL _ -> True
 _ -> False

Now, at least as long as a type X has only a finite number of
constructors (integers with numeric literals being an exception), the
type Clopen X defines a Stone space, a compact zero-dimensional
Hausdorff space. By Stone duality these are dually equivalent to
Boolean algebras. The duality translates the problem of coverage by
clopens to the problem of proving that the disjunction of some elements
in the algebra is the top element 'True'. Since Zeroth-order logic is
decidable, completness checks even in the presence of pattern synonyms
should be, too. 
For the countably infinite type C above, one can use the Select monad
[2] to decide whether any number of clopens covers the space, pattern
or not. 
For numeric literal patterns we can safely say that any set of patterns
is not covering unless a wildcard pattern is among them. 

Olaf 

[1] https://en.wikipedia.org/wiki/Stone_space
[2] https://hackage.haskell.org/package/transformers-0.6.1.1/docs/Control-Monad-Trans-Select.html
see also https://hackage.haskell.org/package/infinite-search