Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

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

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 <mailto: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 a
>>> pattern J a = Just a
>>> 
>>> pattern N :: Maybe a
>>> pattern 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 <https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html>
>>> _______________________________________________
>>> ghc-devs mailing list
>>> ghc-devs at haskell.org <mailto:ghc-devs at haskell.org>
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs <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/0eca71dc/attachment.html>