Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms
Carter Schonwald
carter.schonwald at gmail.com
Sat Oct 27 01:43:18 UTC 2018
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
On Fri, Oct 26, 2018 at 1:05 PM Richard Eisenberg <rae at cs.brynmawr.edu>
wrote:
> 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
>
> On Oct 26, 2018, at 5:20 AM, Sylvain Henry <sylvain at haskus.fr> wrote:
>
> 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
>
>
> On 10/26/18 5:59 AM, Richard Eisenberg wrote:
>
> 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
>
> On Oct 25, 2018, at 12:24 PM, Sylvain Henry <sylvain at haskus.fr> wrote:
>
> > 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
> #-}
>
> > 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.
>
> 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
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20181026/532c4c39/attachment.html>
More information about the ghc-devs
mailing list