COMPLETE pragmas

Tue Sep 1 08:11:59 UTC 2020

Hi Edward,

I'd expect (1) to work after fixing #14422/#18276.
(3) might have been https://gitlab.haskell.org/ghc/ghc/-/issues/16682, so
it should be fixed nowadays.
(2) is a neat idea, but requires a GHC proposal I'm not currently willing
to get into. I can also see a design discussion around allowing arbitrary
"formulas" (e.g., not only what is effectively CNF).
A big bonus of your design is that it's really easy to integrate into the
current implementation, which is what I'd gladly do in case such a proposal
would get accepted.

Cheers
Sebastian

Am Di., 1. Sept. 2020 um 00:26 Uhr schrieb Edward Kmett <ekmett at gmail.com>:

> I'd be over the moon with happiness if I could hang COMPLETE pragmas on
> polymorphic types.
>
> I have 3 major issues with COMPLETE as it exists.
>
> 1.) Is what is mentioned here:
>
> Examples for me come up when trying to build a completely unboxed 'linear'
> library using backpack. In the end I want/need to supply a pattern synonym
> that works over, say, all the 2d vector types, extracting their elements,
> but right now I just get spammed by incomplete coverage warnings.
>
> type family Elem t :: Type
> class D2 where
>   _V2 :: Iso' t (Elem t, Elem t)
>
> pattern V2 :: D2 t => Elem t -> Elem t -> t
> pattern V2 a b <- (view _V2 -> (a,b)) where
>   V2 a b = review _V2 (a,b)
>
> There is no way to hang a COMPLETE pragma on that.
>
> 2.) Another scenario that I'd really love to see supported with COMPLETE
> pragmas is a way to use | notation with them like you can with MINIMAL
> pragmas.
>
> If you make smart constructors for a dozen constructors in your term type
> (don't judge me!), you wind up needing 2^12 COMPLETE pragmas to describe
> all the ways you might mix regular and start constructors today.
>
> {# COMPLETE (Lam | LAM), (Var | VAR), ... #-}
>
> would let you get away with a single such definition. This comes up when
> you have some kind of monoid that acts on terms and you want to push it
> down through
> the syntax tree invisibly to the user. Explicit substitutions, shifts in
> position in response to source code edits, etc.
>
> 3.) I had one other major usecase where I failed to be able to use a
> COMPLETE pragma:
>
> type Option a = (# a | (##) #)
>
> pattern Some :: a -> Option a
> pattern Some a = (# a | #)
>
> pattern None :: Option a
> pattern None = (# | (##) #)
>
> {-# COMPLETE Some, None #-}
>
> These worked _within_ a module, but was forgotten across module
> boundaries, which forced me to rather drastically change the module
> structure of a package, but it sounds a lot like the issue being discussed.
> No types to hang it on in the interface file. With the ability to define
> unlifted newtypes I guess this last one is less of a concern now?
>
> -Edward
>
> On Mon, Aug 31, 2020 at 2:29 PM Richard Eisenberg <rae at richarde.dev>
> wrote:
>
>> Hooray Sebastian!
>>
>> Somehow, I knew cluing you into this conundrum would help find a
>> solution. The approach you describe sounds quite plausible.
>>
>> Yet: types *do* matter, of course. So, I suppose the trick is this: have
>> the COMPLETE sets operate independent of types, but then use types in the
>> PM-checker when determining impossible cases? And, about your idea for
>> having pattern synonyms store pointers to their COMPLETE sets: I think data
>> constructors can also participate. But maybe there is always at least one
>> pattern synonym (which would be a reasonable restriction), so I guess you
>> can look at the pattern-match as a whole and use the pattern synonym to
>> find the relevant COMPLETE set(s).
>>
>> Thanks for taking a look!
>> Richard
>>
>> On Aug 31, 2020, at 4:23 PM, Sebastian Graf <sgraf1337 at gmail.com> wrote:
>>
>> Hi Richard,
>>
>> Am Mo., 31. Aug. 2020 um 21:30 Uhr schrieb Richard Eisenberg <
>> rae at richarde.dev>:
>>
>>> Hi Sebastian,
>>>
>>> I enjoyed your presentation last week at ICFP!
>>>
>>
>> Thank you :) I'm glad you liked it!
>>
>> This thread (
>>> https://ghc-devs.haskell.narkive.com/NXBBDXg1/suppressing-false-incomplete-pattern-matching-warnings-for-polymorphic-pattern-synonyms)
>>> played out before you became so interested in pattern-match coverage. I'd
>>> be curious for your thoughts there -- do you agree with the conclusions in
>>> the thread?
>>>
>>
>> I vaguely remember reading this thread. As you write there
>> <https://ghc-devs.haskell.narkive.com/NXBBDXg1/suppressing-false-incomplete-pattern-matching-warnings-for-polymorphic-pattern-synonyms#post9>
>>
>> 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.
>>>
>>
>> Without reading the whole thread, I think that solution is very possible.
>> The thread goes on to state that we currently attach COMPLETE sets to type
>> constructors, but that is only an implementational thing. I asked Matt (who
>> implemented it) somewhere and he said the only reason to attach it to type
>> constructors was because it was the easiest way to implement serialisation
>> to interface files.
>>
>> The thread also mentions that type-directed works better for the
>> pattern-match checker. In fact I disagree; we have to thin out COMPLETE
>> sets all the time anyway when new type evidence comes up, for example. It's
>> quite a hassle to find all the COMPLETE sets of the type constructors a
>> given type can be "represented" (I mean equality modulo type family
>> reductions here) as. I'm pretty sure it's broken in multiple ways, as
>> #18276 <https://gitlab.haskell.org/ghc/ghc/-/issues/18276> points out.
>>
>> Disregarding a bit of busy work for implementing serialisation to
>> interface files, it's probably far simpler to give each COMPLETE set a
>> Name/Unique and refer to them from the pattern synonyms that mention them
>> (we'd have to get creative for orphans, though). The relation is quite like
>> between a type class instance and the type in its head. A more worked
>> example is here:
>> https://gitlab.haskell.org/ghc/ghc/-/issues/18277#note_287827
>>
>> So, it's on my longer term TODO list to fix this.
>>
>>
>>> My motivation for asking is https://github.com/conal/linalg/pull/54
>>> (you don't need to read the whole thing), which can be boiled down to a
>>> request for a COMPLETE pragma that works at a polymorphic result type. (Or
>>> a COMPLETE pragma written in a module that is not the defining module for a
>>> pattern synonym.) https://gitlab.haskell.org/ghc/ghc/-/issues/14422
>>> describes a similar, but even more challenging scenario.
>>>
>>
>> I'll answer in the thread. (Oh, you also found #14422.) I think the
>> approach above will also fix #14422.
>>
>>>
>>> Do you see any ways forward here?
>>>
>> .
>>
>>>
>>> Thanks!
>>> Richard
>>
>>
>> Maybe I'll give it a try tomorrow.
>>
>>
>> _______________________________________________
>> 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/20200901/18426c27/attachment-0001.html>