Discussion:
Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms
(too old to reply)
Shayan Najd
2018-10-25 11:36:10 UTC
Permalink
Dear GHC hackers,

On our work on the new front-end AST for GHC [0] based on TTG [1], we
would like to use a pattern synonym like the following [2]:

{{{
pattern LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a
pattern LL s m <- (decomposeSrcSpan -> (m , s))
where
LL s m = composeSrcSpan (m , s)
}}}

We know that any match on `LL` patterns, makes the pattern matching
total, as it uses a view pattern with a total output pattern (i.e., in
`decomposeSrcSpan -> (m , s)`, the pattern `(m , s)` is total).

As far as I understand, currently COMPLETE pragmas cannot be used with
such a polymorphic pattern.

What do you suggest us to do to avoid the false incomplete pattern
matching warnings?

Thanks,
Shayan

[0] https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow
[1] https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow/TreesThatGrowGuidance
[2] https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow/HandlingSourceLocations
Richard Eisenberg
2018-10-25 12:51:29 UTC
Permalink
This sounds like an infelicity in COMPLETE pragmas. Do we have a documented reason why fixing this is impossible?

Richard
Post by Shayan Najd
Dear GHC hackers,
On our work on the new front-end AST for GHC [0] based on TTG [1], we
{{{
pattern LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a
pattern LL s m <- (decomposeSrcSpan -> (m , s))
where
LL s m = composeSrcSpan (m , s)
}}}
We know that any match on `LL` patterns, makes the pattern matching
total, as it uses a view pattern with a total output pattern (i.e., in
`decomposeSrcSpan -> (m , s)`, the pattern `(m , s)` is total).
As far as I understand, currently COMPLETE pragmas cannot be used with
such a polymorphic pattern.
What do you suggest us to do to avoid the false incomplete pattern
matching warnings?
Thanks,
Shayan
[0] https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow
[1] https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow/TreesThatGrowGuidance
[2] https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow/HandlingSourceLocations
_______________________________________________
ghc-devs mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Ryan Scott
2018-10-25 13:30:42 UTC
Permalink
The fact that `LL` can't be used in a COMPLETE pragma is a consequence
of its current design. Per the users' guide [1]:

To make things more formal, when the pattern-match checker
requests a set of constructors for some data type constructor T, the
checker returns:

* The original set of data constructors for T
* Any COMPLETE sets of type T

Note the use of the phrase *type constructor*. The return type of all
constructor-like things in a COMPLETE set must all be headed by the
same type constructor T. Since `LL`'s return type is simply a type
variable `a`, this simply doesn't work with the design of COMPLETE
sets.

But to be perfectly honest, I feel that trying to put `LL` into a
COMPLETE set is like putting a square peg into a round hole. The
original motivation for COMPLETE sets, as given in this wiki page [2],
is to support using pattern synonyms in an abstract matter—that is, to
ensure that users who match on pattern synonyms don't have any
internal implementation details of those pattern synonyms leak into
error messages. This is well and good for many use cases, but there
are also many use cases where we don't *care* about abstraction.
Sometimes, we simply define a pattern synonym to be a convenient
shorthand for a complicated pattern to facilitate code reuse, and
nothing more.

`LL` is a perfect example of this, in my opinion. `LL` is simply a
thin wrapper around the use of `decomposeSrcSpan` as a view pattern.
Trying to put `LL` into a COMPLETE set is silly since our intention
isn't to hide the implementation details of decomposing a `SrcSpan`,
but rather to avoid the need to copy-paste `(decomposeSrcSpan -> (m ,
s))` in a bazillion patterns. Correspondingly, any use of `LL` ought
to be treated as if the `(decomposeSrcSpan -> (m , s))` pattern were
inlined—and from the pattern-match coverage checker's point of view,
that *is* exhaustive!

What's the moral of the story here? To me, this is a sign that the
design space of pattern synonym coverage checking isn't rich enough.
In addition to the existing {-# COMPLETE #-} machinery that we have
today, I think we need to have a separate pragma for pattern synonyms
that are intended to be transparent, non-abstract wrappers around
patterns ({-# TRANSPARENT #-}, perhaps).

Ryan S.
-----
[1] https://downloads.haskell.org/~ghc/8.6.1/docs/html/users_guide/glasgow_exts.html#complete-pragma
[2] https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms/CompleteSigs
Richard Eisenberg
2018-10-25 14:20:14 UTC
Permalink
In a rare move, I disagree with Ryan here.

Why don't we want LL to be abstract? I personally don't want to be thinking of some desugaring to a view pattern when I say LL. I want just to be pattern matching. Is there a reason we can't extend COMPLETE pragmas to cover this case?

Richard
Post by Ryan Scott
The fact that `LL` can't be used in a COMPLETE pragma is a consequence
To make things more formal, when the pattern-match checker
requests a set of constructors for some data type constructor T, the
* The original set of data constructors for T
* Any COMPLETE sets of type T
Note the use of the phrase *type constructor*. The return type of all
constructor-like things in a COMPLETE set must all be headed by the
same type constructor T. Since `LL`'s return type is simply a type
variable `a`, this simply doesn't work with the design of COMPLETE
sets.
But to be perfectly honest, I feel that trying to put `LL` into a
COMPLETE set is like putting a square peg into a round hole. The
original motivation for COMPLETE sets, as given in this wiki page [2],
is to support using pattern synonyms in an abstract matter—that is, to
ensure that users who match on pattern synonyms don't have any
internal implementation details of those pattern synonyms leak into
error messages. This is well and good for many use cases, but there
are also many use cases where we don't *care* about abstraction.
Sometimes, we simply define a pattern synonym to be a convenient
shorthand for a complicated pattern to facilitate code reuse, and
nothing more.
`LL` is a perfect example of this, in my opinion. `LL` is simply a
thin wrapper around the use of `decomposeSrcSpan` as a view pattern.
Trying to put `LL` into a COMPLETE set is silly since our intention
isn't to hide the implementation details of decomposing a `SrcSpan`,
but rather to avoid the need to copy-paste `(decomposeSrcSpan -> (m ,
s))` in a bazillion patterns. Correspondingly, any use of `LL` ought
to be treated as if the `(decomposeSrcSpan -> (m , s))` pattern were
inlined—and from the pattern-match coverage checker's point of view,
that *is* exhaustive!
What's the moral of the story here? To me, this is a sign that the
design space of pattern synonym coverage checking isn't rich enough.
In addition to the existing {-# COMPLETE #-} machinery that we have
today, I think we need to have a separate pragma for pattern synonyms
that are intended to be transparent, non-abstract wrappers around
patterns ({-# TRANSPARENT #-}, perhaps).
Ryan S.
-----
[1] https://downloads.haskell.org/~ghc/8.6.1/docs/html/users_guide/glasgow_exts.html#complete-pragma
[2] https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms/CompleteSigs
_______________________________________________
ghc-devs mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Matthew Pickering
2018-10-25 14:35:01 UTC
Permalink
I think that `LL` is precisely intended for abstraction. If this
`COMPLETE` pragma were possible to implement then a user shouldn't
know the difference between the old and new representations.

The reason that `COMPLETE` pragmas are designed like this is that it's
how the pattern match checker is defined. The collection of patterns
used for the checking are queried by the type of the patterns so it
made sense to associate
each `COMPLETE` set with a specific type.
Post by Ryan Scott
The fact that `LL` can't be used in a COMPLETE pragma is a consequence
To make things more formal, when the pattern-match checker
requests a set of constructors for some data type constructor T, the
* The original set of data constructors for T
* Any COMPLETE sets of type T
Note the use of the phrase *type constructor*. The return type of all
constructor-like things in a COMPLETE set must all be headed by the
same type constructor T. Since `LL`'s return type is simply a type
variable `a`, this simply doesn't work with the design of COMPLETE
sets.
But to be perfectly honest, I feel that trying to put `LL` into a
COMPLETE set is like putting a square peg into a round hole. The
original motivation for COMPLETE sets, as given in this wiki page [2],
is to support using pattern synonyms in an abstract matter—that is, to
ensure that users who match on pattern synonyms don't have any
internal implementation details of those pattern synonyms leak into
error messages. This is well and good for many use cases, but there
are also many use cases where we don't *care* about abstraction.
Sometimes, we simply define a pattern synonym to be a convenient
shorthand for a complicated pattern to facilitate code reuse, and
nothing more.
`LL` is a perfect example of this, in my opinion. `LL` is simply a
thin wrapper around the use of `decomposeSrcSpan` as a view pattern.
Trying to put `LL` into a COMPLETE set is silly since our intention
isn't to hide the implementation details of decomposing a `SrcSpan`,
but rather to avoid the need to copy-paste `(decomposeSrcSpan -> (m ,
s))` in a bazillion patterns. Correspondingly, any use of `LL` ought
to be treated as if the `(decomposeSrcSpan -> (m , s))` pattern were
inlined—and from the pattern-match coverage checker's point of view,
that *is* exhaustive!
What's the moral of the story here? To me, this is a sign that the
design space of pattern synonym coverage checking isn't rich enough.
In addition to the existing {-# COMPLETE #-} machinery that we have
today, I think we need to have a separate pragma for pattern synonyms
that are intended to be transparent, non-abstract wrappers around
patterns ({-# TRANSPARENT #-}, perhaps).
Ryan S.
-----
[1] https://downloads.haskell.org/~ghc/8.6.1/docs/html/users_guide/glasgow_exts.html#complete-pragma
[2] https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms/CompleteSigs
_______________________________________________
ghc-devs mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Ryan Scott
2018-10-25 14:40:06 UTC
Permalink
You *can* put `LL` into a COMPLETE set, but under the stipulation that
you specify which type constructor it's monomorphized to. To quote the
wiki page on COMPLETE sets:

In the case where all the patterns are polymorphic, a user must
provide a type signature but we accept the definition regardless of
the type signature they provide. The type constructor for the whole
set of patterns is the type constructor as specified by the user. If
the user does not provide a type signature then the definition is
rejected as ambiguous.

This design is a consequence of the design of the pattern match
checker. Complete sets of patterns must be identified relative to a
type. This is a sanity check as users would never be able to match on
all constructors if the set of patterns is inconsistent in this
manner.

In other words, this would work provided that you'd be willing to list
every single instance of `HasSrcSpan` in its own COMPLETE set. It's
tedious, but possible.

Ryan S.
-----
[1] https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms/CompleteSigs#Typing
Shayan Najd
2018-10-25 15:59:47 UTC
Permalink
[Ryan Scott:]
In other words, this would work provided that you'd be willing to list
every single instance of `HasSrcSpan` in its own COMPLETE set. It's
tedious, but possible.
Yes, for the cases where `LL` is used monomorphically, we can use the
per-instance COMPLETE pragma, but it does not scale to the generic
cases where `LL` is used polymorphically.
Consider the following where `Exp` and `Pat` are both instances of `HasSrcSpan`:
{{{
{-# COMPLETE LL :: Exp #-}
{-# COMPLETE LL :: Pat #-}

unLocExp :: Exp -> Exp
unLocExp (LL _ m) = m

unLocPat :: Pat -> Pat
unLocPat (LL _ m) = m

unLocGen :: HasLoc a => a -> SrcSpanLess a
unLocGen (LL _ m) = m
}}}

In the functions `unLocExp` and `unLocPat`, the related COMPLETE
pragmas rightly avoid the false incomplete pattern matching warnings.

However, to avoid the false incomplete pattern matching warning in
`unLocGen`, either I should add a catch-all case
`unLocGen _ = error "Impossible!"`
or expose the internal view patterns and hence break the abstraction
`unLocGen (decomposeSrcSpan->(_ , m)) = m`

We want to avoid both solutions and unfortunately, this problem arises
frequently enough.
For example, in GHC, there are plenty of such generic cases (e.g.,
`sL1` or the like in the parser).
[Ryan Scott:]
Complete sets of patterns must be identified relative to a type.
Technically `HasSrcSpan a0 |- a0` is a type, for a Skolem variable
`a0`; I understand if you mean relative to a concrete type, but I
don't understand why (I have no experience with GHC's totality checker
code).
Why can't it be syntactic? We should allow programmers to express
things like "when you see `LL` treat the related pattern matching
group as total".

/Shayan
You *can* put `LL` into a COMPLETE set, but under the stipulation that
you specify which type constructor it's monomorphized to. To quote the
In the case where all the patterns are polymorphic, a user must
provide a type signature but we accept the definition regardless of
the type signature they provide. The type constructor for the whole
set of patterns is the type constructor as specified by the user. If
the user does not provide a type signature then the definition is
rejected as ambiguous.
This design is a consequence of the design of the pattern match
checker. Complete sets of patterns must be identified relative to a
type. This is a sanity check as users would never be able to match on
all constructors if the set of patterns is inconsistent in this
manner.
In other words, this would work provided that you'd be willing to list
every single instance of `HasSrcSpan` in its own COMPLETE set. It's
tedious, but possible.
Ryan S.
-----
[1] https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms/CompleteSigs#Typing
_______________________________________________
ghc-devs mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Sylvain Henry
2018-10-25 16:24:02 UTC
Permalink
Post by Ryan Scott
In the case where all the patterns are polymorphic, a user must
provide a type signature but we accept the definition regardless of
the type signature they provide.
Currently we can specify the type *constructor* in a COMPLETE pragma:

pattern J :: a -> Maybe apattern J a = Just apattern N :: Maybe apattern
N = Nothing{-# COMPLETE N, J :: Maybe #-}


Instead if we could specify the type with its free vars, we could refer
to them in conlike signatures:

{-# COMPLETE N, [J:: a -> Maybe a ] :: Maybe a #-}

The COMPLETE pragma for LL could be:

{-# COMPLETE [LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a ] :: a
#-}


I'm borrowing the list comprehension syntax on purpose because it would
allow to define a set of conlikes from a type-list (see my request [1]):

{-# COMPLETE [V :: (c :< cs) => c -> Variant cs | c <- cs ] :: Variant
cs #-}
Post by Ryan Scott
To make things more formal, when the pattern-match checker
requests a set of constructors for some data type constructor T, the
* The original set of data constructors for T
* Any COMPLETE sets of type T
Note the use of the phrase *type constructor*. The return type of all
constructor-like things in a COMPLETE set must all be headed by the
same type constructor T. Since `LL`'s return type is simply a type
variable `a`, this simply doesn't work with the design of COMPLETE
sets.
Could we use a mechanism similar to instance resolution (with
FlexibleInstances) for the checker to return matching COMPLETE sets instead?


--Sylvain


[1] https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html
Richard Eisenberg
2018-10-26 03:59:09 UTC
Permalink
I'm afraid I don't understand what your new syntax means. And, while I know it doesn't work today, what's wrong (in theory) with

{-# COMPLETE LL #-}

No types! (That's a rare thing for me to extol...)

I feel I must be missing something here.

Thanks,
Richard
Post by Sylvain Henry
Post by Ryan Scott
In the case where all the patterns are polymorphic, a user must
provide a type signature but we accept the definition regardless of
the type signature they provide.
pattern J :: a -> Maybe a
pattern J a = Just a
pattern N :: Maybe a
pattern N = Nothing
{-# COMPLETE N, J :: Maybe #-}
{-# COMPLETE N, [ J :: a -> Maybe a ] :: Maybe a #-}
{-# COMPLETE [ LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a ] :: a #-}
{-# COMPLETE [ V :: (c :< cs) => c -> Variant cs
| c <- cs
] :: Variant cs
#-}
Post by Ryan Scott
To make things more formal, when the pattern-match checker
requests a set of constructors for some data type constructor T, the
* The original set of data constructors for T
* Any COMPLETE sets of type T
Note the use of the phrase *type constructor*. The return type of all
constructor-like things in a COMPLETE set must all be headed by the
same type constructor T. Since `LL`'s return type is simply a type
variable `a`, this simply doesn't work with the design of COMPLETE
sets.
Could we use a mechanism similar to instance resolution (with FlexibleInstances) for the checker to return matching COMPLETE sets instead?
--Sylvain
[1] https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html <https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html>
_______________________________________________
ghc-devs mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Sylvain Henry
2018-10-26 09:20:55 UTC
Permalink
Sorry I wasn't clear. I'm not an expert on the topic but it seems to me
that there are two orthogonal concerns:

1) How does the checker retrieve COMPLETE sets.

Currently it seems to "attach" them to data type constructors (e.g.
Maybe). If instead it retrieved them by matching types (e.g. "Maybe a",
"a") we could write:

{-# COMPLETE LL #-}

From an implementation point of view, it seems to me that finding
complete sets would become similar to finding (flexible, overlapping)
class instances. Pseudo-code:

class Complete a where
  conlikes :: [ConLike]
instance Complete (Maybe a) where
conlikes = [Nothing @a, Just @a]
instance Complete (Maybe a) where
conlikes = [N @a, J @a]
instance Complete a where
  conlikes = [LL @a]
...


2) COMPLETE set depending on the matched type.

It is a thread hijack from me but while we are thinking about
refactoring COMPLETE pragmas to support polymorphism, maybe we could
support this too. The idea is to build a different set of conlikes
depending on the matched type. Pseudo-code:

instance Complete (Variant cs) where
conlikes = [V @c | c <- cs] -- cs is a type list

(I don't really care about the pragma syntax)

Sorry for the thread hijack!
Regards,
Sylvain
Post by Richard Eisenberg
I'm afraid I don't understand what your new syntax means. And, while I
know it doesn't work today, what's wrong (in theory) with
{-# COMPLETE LL #-}
No types! (That's a rare thing for me to extol...)
I feel I must be missing something here.
Thanks,
Richard
Post by Sylvain Henry
Post by Ryan Scott
In the case where all the patterns are polymorphic, a user must
provide a type signature but we accept the definition regardless of
the type signature they provide.
pattern J :: a -> Maybe apattern J a = Just apattern N :: Maybe
apattern N = Nothing{-# COMPLETE N, J :: Maybe #-}
Instead if we could specify the type with its free vars, we could
{-# COMPLETE N, [J:: a -> Maybe a ] :: Maybe a #-}
{-# COMPLETE [LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a ]
:: a #-}
I'm borrowing the list comprehension syntax on purpose because it
would allow to define a set of conlikes from a type-list (see my
Variant cs #-}
Post by Ryan Scott
To make things more formal, when the pattern-match checker
requests a set of constructors for some data type constructor T, the
* The original set of data constructors for T
* Any COMPLETE sets of type T
Note the use of the phrase *type constructor*. The return type of all
constructor-like things in a COMPLETE set must all be headed by the
same type constructor T. Since `LL`'s return type is simply a type
variable `a`, this simply doesn't work with the design of COMPLETE
sets.
Could we use a mechanism similar to instance resolution (with
FlexibleInstances) for the checker to return matching COMPLETE sets instead?
--Sylvain
[1]https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html
_______________________________________________
ghc-devs mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Richard Eisenberg
2018-10-26 17:04:45 UTC
Permalink
Aha. So you're viewing complete sets as a type-directed property, where we can take a type and look up what complete sets of patterns of that type might be.

Then, when checking a pattern-match for completeness, we use the inferred type of the pattern, access its complete sets, and if these match up. (Perhaps an implementation may optimize this process.)

What I like about this approach is that it works well with GADTs, where, e.g., VNil is a complete set for type Vec a Zero but not for Vec a n.

I take back my claim of "No types!" then, as this does sound like it has the right properties.

For now, I don't want to get bogged down by syntax -- let's figure out how the idea should work first, and then we can worry about syntax.

Here's a stab at a formalization of this idea, written in metatheory, not Haskell:

Let C : Type -> Set of set of patterns. C will be the lookup function for complete sets. Suppose we have a pattern match, at type tau, matching against patterns Ps. Let S = C(tau). S is then a set of sets of patterns. The question is this: Is there a set s in S such that Ps is a superset of s? If yes, then the match is complete.

What do we think of this design? Of course, the challenge is in building C, but we'll tackle that next.

Richard
Post by Sylvain Henry
1) How does the checker retrieve COMPLETE sets.
{-# COMPLETE LL #-}
class Complete a where
conlikes :: [ConLike]
instance Complete (Maybe a) where
instance Complete (Maybe a) where
instance Complete a where
...
2) COMPLETE set depending on the matched type.
instance Complete (Variant cs) where
(I don't really care about the pragma syntax)
Sorry for the thread hijack!
Regards,
Sylvain
Post by Richard Eisenberg
I'm afraid I don't understand what your new syntax means. And, while I know it doesn't work today, what's wrong (in theory) with
{-# COMPLETE LL #-}
No types! (That's a rare thing for me to extol...)
I feel I must be missing something here.
Thanks,
Richard
Post by Sylvain Henry
Post by Ryan Scott
In the case where all the patterns are polymorphic, a user must
provide a type signature but we accept the definition regardless of
the type signature they provide.
pattern J :: a -> Maybe a
pattern J a = Just a
pattern N :: Maybe a
pattern N = Nothing
{-# COMPLETE N, J :: Maybe #-}
{-# COMPLETE N, [ J :: a -> Maybe a ] :: Maybe a #-}
{-# COMPLETE [ LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a ] :: a #-}
{-# COMPLETE [ V :: (c :< cs) => c -> Variant cs
| c <- cs
] :: Variant cs
#-}
Post by Ryan Scott
To make things more formal, when the pattern-match checker
requests a set of constructors for some data type constructor T, the
* The original set of data constructors for T
* Any COMPLETE sets of type T
Note the use of the phrase *type constructor*. The return type of all
constructor-like things in a COMPLETE set must all be headed by the
same type constructor T. Since `LL`'s return type is simply a type
variable `a`, this simply doesn't work with the design of COMPLETE
sets.
Could we use a mechanism similar to instance resolution (with FlexibleInstances) for the checker to return matching COMPLETE sets instead?
--Sylvain
[1] https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html <https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html>
_______________________________________________
ghc-devs mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs <http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs>
Carter Schonwald
2018-10-27 01:43:18 UTC
Permalink
off hand, once we're in in viewpattern/ pattern synonym land, ORDER of the
abstracted constructors matters!

consider
foo,bar,baz,quux,boom :: Nat -> String

plus some pattern synonyms i name "PowerOfTwo", "Even" and "Odd"

foo (PowerOfTwo x) = "power of two"
foo (Even x) = "even"
foo (Odd x) = "odd"

bar (Even x) = "even"
bar (Odd x) = "odd"

baz (PowerOfTwo x) = "power of two"
baz (Odd x) = "odd"

quux (Even x) = "even"
quux (Odd x) = "odd"
quux (PowerOfTwo) = "power of two"

boom (Even x) = "even"
boom (PowerOfTwo x) = "power of two"
boom (Odd x) = "odd"

foo and bar are both total definitions with unambiguous meanings, even
though bar's patterns are a suffix of foos'!
baz is partial!

both boom and quux have a redudant overlapping case, power of two!

so some thoughts

1) order matters!
2) pattern synonyms at type T are part of an infinite lattice, Top element
== accept everything, Bottom element = reject everything

3) PowerOfTwo <= Even in the Lattice for Natual, both are "incomparable"
with Odd

4) for a simple case on a single value at type T, assume c1 <= c2
, then if c1 x -> ... is before c2 x -> in the
cases, then both are useful/computationally meaningful
OTHERWISE
when its
case x :: T of
c2 x -> ...
c1 x -> ...
then the 'c1 x' is redundant


this is slightly orthogonal to other facets of this discussion so far, but
i realized that Richard's Set of Sets of patterns model misses some useful/
meaningful examples/extra structure from
a) the implicit lattice of different patterns possibly being super/subsets
(which is still something of an approximation, but with these example I
shared above I hope i've sketched out some motivation )
b) we can possibly model HOW ordering of clauses impacts coverage/totality
/ redundancy of clauses

I'm not sure if it'd be pleasant/good from a user experience perspective to
have this sort of partial ordering modelling stuff, but certainly seems
like it would help distinguish some useful examples where the program
meaning / coverage is sensitive to clause ordering


i can try to spell this out more if theres interest, but I wanted to share
while the iron was hot

best!
-Carter
Post by Richard Eisenberg
Aha. So you're viewing complete sets as a type-directed property, where we
can take a type and look up what complete sets of patterns of that type
might be.
Then, when checking a pattern-match for completeness, we use the inferred
type of the pattern, access its complete sets, and if these match up.
(Perhaps an implementation may optimize this process.)
What I like about this approach is that it works well with GADTs, where,
e.g., VNil is a complete set for type Vec a Zero but not for Vec a n.
I take back my claim of "No types!" then, as this does sound like it has
the right properties.
For now, I don't want to get bogged down by syntax -- let's figure out how
the idea should work first, and then we can worry about syntax.
Let C : Type -> Set of set of patterns. C will be the lookup function for
complete sets. Suppose we have a pattern match, at type tau, matching
against patterns Ps. Let S = C(tau). S is then a set of sets of patterns.
The question is this: Is there a set s in S such that Ps is a superset of
s? If yes, then the match is complete.
What do we think of this design? Of course, the challenge is in building
C, but we'll tackle that next.
Richard
Sorry I wasn't clear. I'm not an expert on the topic but it seems to me
1) How does the checker retrieve COMPLETE sets.
Currently it seems to "attach" them to data type constructors (e.g.
Maybe). If instead it retrieved them by matching types (e.g. "Maybe a",
{-# COMPLETE LL #-}
From an implementation point of view, it seems to me that finding complete
sets would become similar to finding (flexible, overlapping) class
class Complete a where
conlikes :: [ConLike]
instance Complete (Maybe a) where
instance Complete (Maybe a) where
instance Complete a where
...
2) COMPLETE set depending on the matched type.
It is a thread hijack from me but while we are thinking about refactoring
COMPLETE pragmas to support polymorphism, maybe we could support this too.
The idea is to build a different set of conlikes depending on the matched
instance Complete (Variant cs) where
(I don't really care about the pragma syntax)
Sorry for the thread hijack!
Regards,
Sylvain
I'm afraid I don't understand what your new syntax means. And, while I
know it doesn't work today, what's wrong (in theory) with
{-# COMPLETE LL #-}
No types! (That's a rare thing for me to extol...)
I feel I must be missing something here.
Thanks,
Richard
Post by Ryan Scott
In the case where all the patterns are polymorphic, a user must
provide a type signature but we accept the definition regardless of
the type signature they provide.
pattern J :: a -> Maybe apattern J a = Just apattern N :: Maybe apattern N = Nothing{-# COMPLETE N, J :: Maybe #-}
Instead if we could specify the type with its free vars, we could refer to
{-# COMPLETE N, [ J :: a -> Maybe a ] :: Maybe a #-}
{-# COMPLETE [ LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a ] :: a #-}
I'm borrowing the list comprehension syntax on purpose because it would
{-# COMPLETE [ V :: (c :< cs) => c -> Variant cs
| c <- cs
] :: Variant cs
#-}
Post by Ryan Scott
To make things more formal, when the pattern-match checker > requests a
set of constructors for some data type constructor T, the > checker
returns: > > * The original set of data constructors for T > * Any COMPLETE
sets of type T > > Note the use of the phrase **type constructor**. The
return type of all > constructor-like things in a COMPLETE set must all be
headed by the > same type constructor T. Since `LL`'s return type is simply
a type > variable `a`, this simply doesn't work with the design of COMPLETE
Post by Ryan Scott
sets.
Could we use a mechanism similar to instance resolution (with
FlexibleInstances) for the checker to return matching COMPLETE sets instead?
--Sylvain
[1] https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html
_______________________________________________
ghc-devs mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Richard Eisenberg
2018-10-29 03:54:56 UTC
Permalink
ORDER of the abstracted constructors matters!
That's a very good point. So we don't have a set of sets -- we have a set of lists (where normal constructors -- which have no overlap -- would appear in the lists in every possible permutation).

Again, please don't take my set of lists too seriously from an implementation point of view. We clearly wouldn't implement it this way. But I want to use this abstraction to understand the shape of the problem and what an idealized solution might look like before worrying about implementation and syntax.

Richard
Sylvain Henry
2018-10-29 13:51:50 UTC
Permalink
I've just found this related ticket:
https://ghc.haskell.org/trac/ghc/ticket/14422
Post by Richard Eisenberg
Aha. So you're viewing complete sets as a type-directed property,
where we can take a type and look up what complete sets of patterns of
that type might be.
Then, when checking a pattern-match for completeness, we use the
inferred type of the pattern, access its complete sets, and if these
match up. (Perhaps an implementation may optimize this process.)
What I like about this approach is that it works well with GADTs,
where, e.g., VNil is a complete set for type Vec a Zero but not for
Vec a n.
I take back my claim of "No types!" then, as this does sound like it
has the right properties.
For now, I don't want to get bogged down by syntax -- let's figure out
how the idea should work first, and then we can worry about syntax.
Let C : Type -> Set of set of patterns. C will be the lookup function
for complete sets. Suppose we have a pattern match, at type tau,
matching against patterns Ps. Let S = C(tau). S is then a set of sets
of patterns. The question is this: Is there a set s in S such that Ps
is a superset of s? If yes, then the match is complete.
What do we think of this design? Of course, the challenge is in
building C, but we'll tackle that next.
Richard
Post by Sylvain Henry
Sorry I wasn't clear. I'm not an expert on the topic but it seems to
1) How does the checker retrieve COMPLETE sets.
Currently it seems to "attach" them to data type constructors (e.g.
Maybe). If instead it retrieved them by matching types (e.g. "Maybe
{-# COMPLETE LL #-}
From an implementation point of view, it seems to me that finding
complete sets would become similar to finding (flexible, overlapping)
class Complete a where
  conlikes :: [ConLike]
instance Complete (Maybe a) where
instance Complete (Maybe a) where
instance Complete a where
...
2) COMPLETE set depending on the matched type.
It is a thread hijack from me but while we are thinking about
refactoring COMPLETE pragmas to support polymorphism, maybe we could
support this too. The idea is to build a different set of conlikes
instance Complete (Variant cs) where
(I don't really care about the pragma syntax)
Sorry for the thread hijack!
Regards,
Sylvain
Post by Richard Eisenberg
I'm afraid I don't understand what your new syntax means. And, while
I know it doesn't work today, what's wrong (in theory) with
{-# COMPLETE LL #-}
No types! (That's a rare thing for me to extol...)
I feel I must be missing something here.
Thanks,
Richard
Post by Sylvain Henry
Post by Ryan Scott
In the case where all the patterns are polymorphic, a user must
provide a type signature but we accept the definition regardless of
the type signature they provide.
pattern J :: a -> Maybe apattern J a = Just apattern N :: Maybe
apattern N = Nothing{-# COMPLETE N, J :: Maybe #-}
Instead if we could specify the type with its free vars, we could
{-# COMPLETE N, [J:: a -> Maybe a ] :: Maybe a #-}
{-# COMPLETE [LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a ]
:: a #-}
I'm borrowing the list comprehension syntax on purpose because it
would allow to define a set of conlikes from a type-list (see my
Variant cs #-}
Post by Ryan Scott
To make things more formal, when the pattern-match checker
requests a set of constructors for some data type constructor T, the
* The original set of data constructors for T
* Any COMPLETE sets of type T
Note the use of the phrase *type constructor*. The return type of all
constructor-like things in a COMPLETE set must all be headed by the
same type constructor T. Since `LL`'s return type is simply a type
variable `a`, this simply doesn't work with the design of COMPLETE
sets.
Could we use a mechanism similar to instance resolution (with
FlexibleInstances) for the checker to return matching COMPLETE sets instead?
--Sylvain
[1]https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html
_______________________________________________
ghc-devs mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Shayan Najd
2018-11-10 01:37:25 UTC
Permalink
I also realised the COMPLETE pragmas are even less helpful (at least
for my case mentioned above) as they cannot be used when orphaned.
For example, I tried to follow the partial solution of introducing
multiple COMPLETE pragmas, one per a concrete instance of
`HasSrcSpan`. I defined the pattern synonym `LL` in
`basicTypes/SrcLoc.hs` and wanted to naturally define a COMPLETE
pragma for when `LL` is used for `Pat` in `hsSyn/HsPat.hs`. I got an
error complaining about orphaned COMPLETE pragmas. The only
unacceptable way (that I can see) that makes it work is to have a
module defining `LL`, importing all the instances of `HasSrcSpan`, and
all the COMPLETE pragmas (one per instance).

I have made a ticket about the original concern here:
https://ghc.haskell.org/trac/ghc/ticket/15885

Until we come up with a good and general solution to this ticket, do
you know of a hack to suppress the false incomplete pattern matching
warnings in GHC? Should we add clauses like `foo _ = panic
"Impossible! How did you manage to bypass a complete matching?"`?

/Shayan
I've just found this related ticket: https://ghc.haskell.org/trac/ghc/ticket/14422
Aha. So you're viewing complete sets as a type-directed property, where we can take a type and look up what complete sets of patterns of that type might be.
Then, when checking a pattern-match for completeness, we use the inferred type of the pattern, access its complete sets, and if these match up. (Perhaps an implementation may optimize this process.)
What I like about this approach is that it works well with GADTs, where, e.g., VNil is a complete set for type Vec a Zero but not for Vec a n.
I take back my claim of "No types!" then, as this does sound like it has the right properties.
For now, I don't want to get bogged down by syntax -- let's figure out how the idea should work first, and then we can worry about syntax.
Let C : Type -> Set of set of patterns. C will be the lookup function for complete sets. Suppose we have a pattern match, at type tau, matching against patterns Ps. Let S = C(tau). S is then a set of sets of patterns. The question is this: Is there a set s in S such that Ps is a superset of s? If yes, then the match is complete.
What do we think of this design? Of course, the challenge is in building C, but we'll tackle that next.
Richard
1) How does the checker retrieve COMPLETE sets.
{-# COMPLETE LL #-}
class Complete a where
conlikes :: [ConLike]
instance Complete (Maybe a) where
instance Complete (Maybe a) where
instance Complete a where
...
2) COMPLETE set depending on the matched type.
instance Complete (Variant cs) where
(I don't really care about the pragma syntax)
Sorry for the thread hijack!
Regards,
Sylvain
I'm afraid I don't understand what your new syntax means. And, while I know it doesn't work today, what's wrong (in theory) with
{-# COMPLETE LL #-}
No types! (That's a rare thing for me to extol...)
I feel I must be missing something here.
Thanks,
Richard
Post by Ryan Scott
In the case where all the patterns are polymorphic, a user must
provide a type signature but we accept the definition regardless of
the type signature they provide.
pattern J :: a -> Maybe a
pattern J a = Just a
pattern N :: Maybe a
pattern N = Nothing
{-# COMPLETE N, J :: Maybe #-}
{-# COMPLETE N, [ J :: a -> Maybe a ] :: Maybe a #-}
{-# COMPLETE [ LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a ] :: a #-}
{-# COMPLETE [ V :: (c :< cs) => c -> Variant cs
| c <- cs
] :: Variant cs
#-}
Post by Ryan Scott
To make things more formal, when the pattern-match checker
requests a set of constructors for some data type constructor T, the
* The original set of data constructors for T
* Any COMPLETE sets of type T
Note the use of the phrase *type constructor*. The return type of all
constructor-like things in a COMPLETE set must all be headed by the
same type constructor T. Since `LL`'s return type is simply a type
variable `a`, this simply doesn't work with the design of COMPLETE
sets.
Could we use a mechanism similar to instance resolution (with FlexibleInstances) for the checker to return matching COMPLETE sets instead?
--Sylvain
[1] https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html
_______________________________________________
ghc-devs mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Loading...