<div dir="ltr">off hand, once we're in in viewpattern/ pattern synonym land, ORDER of the abstracted constructors matters!<div><br></div><div>consider </div><div>foo,bar,baz,quux,boom :: Nat -> String</div><div><br></div><div>plus some pattern synonyms i name "PowerOfTwo", "Even" and "Odd" </div><div><br></div><div>foo (PowerOfTwo x) = "power of two"</div><div>foo (Even x) = "even"</div><div>foo (Odd x) = "odd"</div><div><br></div><div>bar (Even x) = "even"</div><div>bar (Odd x) = "odd"</div><div><br></div><div>baz (PowerOfTwo x) = "power of two"</div><div>baz (Odd x) = "odd"</div><div><br></div><div>quux (Even x) = "even"</div><div>quux (Odd x) = "odd"</div><div>quux (PowerOfTwo) = "power of two"</div><div><br></div><div>boom (Even x) = "even"<br>boom (PowerOfTwo x) = "power of two"</div><div>boom (Odd x) = "odd"</div><div><br></div><div>foo and bar are both total definitions with unambiguous meanings, even though bar's patterns are a suffix of foos'!</div><div>baz is partial!</div><div><br></div><div>both boom and quux have a redudant overlapping case, power of two!</div><div><br></div><div>so some thoughts</div><div><br></div><div>1) order matters!</div><div>2) pattern synonyms at type T are part of an infinite lattice, Top element == accept everything, Bottom element = reject everything</div><div><br></div><div>3) PowerOfTwo <= Even in the Lattice for Natual, both are "incomparable" with Odd</div><div><br></div><div>4) for a simple case on a single value at type T, assume c1 <= c2</div><div> , then if c1 x -> ... is before c2 x -> in the cases, then both are useful/computationally meaningful</div><div> OTHERWISE</div><div> when its </div><div> case x :: T of </div><div> c2 x -> ...</div><div> c1 x -> ...</div><div>then the 'c1 x' is redundant</div><div><br></div><div><br></div><div>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</div><div>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 )</div><div>b) we can possibly model HOW ordering of clauses impacts coverage/totality / redundancy of clauses</div><div><br></div><div>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 </div><div><br></div><div>i can try to spell this out more if theres interest, but I wanted to share while the iron was hot</div><div><br></div><div>best!</div><div>-Carter</div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Fri, Oct 26, 2018 at 1:05 PM Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu">rae@cs.brynmawr.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space">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.<div><br></div><div>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.)</div><div><br></div><div>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.</div><div><br></div><div>I take back my claim of "No types!" then, as this does sound like it has the right properties.</div><div><br></div><div>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.</div><div><br></div><div>Here's a stab at a formalization of this idea, written in metatheory, not Haskell:</div><div><br></div><div>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.</div><div><br></div><div>What do we think of this design? Of course, the challenge is in building C, but we'll tackle that next.</div><div><br></div><div>Richard<br><div><div><br><blockquote type="cite"><div>On Oct 26, 2018, at 5:20 AM, Sylvain Henry <<a href="mailto:sylvain@haskus.fr" target="_blank">sylvain@haskus.fr</a>> wrote:</div><br class="m_3081504951675166151Apple-interchange-newline"><div>
<div text="#000000" bgcolor="#FFFFFF"><p>Sorry I wasn't clear. I'm not an expert on the topic but it seems
to me that there are two orthogonal concerns:</p><p>1) How does the checker retrieve COMPLETE sets.</p><p>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:</p><p>{-# COMPLETE LL #-}<br>
</p><p>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:<br>
</p>
<pre>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]
...
</pre><p><br>
</p><p>2) COMPLETE set depending on the matched type.</p><p>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:<br>
</p>
<pre>instance Complete (Variant cs) where
conlikes = [V @c | c <- cs] -- cs is a type list
</pre><p>(I don't really care about the pragma syntax)</p><p>Sorry for the thread hijack!<br>
Regards,<br>
Sylvain<br>
</p><p><br>
</p>
<div class="m_3081504951675166151moz-cite-prefix">On 10/26/18 5:59 AM, Richard Eisenberg
wrote:<br>
</div>
<blockquote type="cite">
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
<div><br>
</div>
<div>{-# COMPLETE LL #-}</div>
<div><br>
</div>
<div>No types! (That's a rare thing for me to extol...)</div>
<div><br>
</div>
<div>I feel I must be missing something here.</div>
<div><br>
</div>
<div>Thanks,</div>
<div>Richard<br>
<div><br>
<blockquote type="cite">
<div>On Oct 25, 2018, at 12:24 PM, Sylvain Henry
<<a href="mailto:sylvain@haskus.fr" target="_blank">sylvain@haskus.fr</a>> wrote:</div>
<br class="m_3081504951675166151Apple-interchange-newline">
<div>
<div text="#000000" bgcolor="#FFFFFF">
<pre class="m_3081504951675166151moz-quote-pre">> 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. </pre><p>Currently we can specify the type
*constructor* in a COMPLETE pragma:</p>
<pre><tt>pattern J :: a -> Maybe a</tt><tt>
</tt><tt>pattern J a = Just a</tt><tt>
</tt><tt>
</tt><tt>pattern N :: Maybe a</tt><tt>
</tt><tt>pattern N = Nothing</tt><tt>
</tt><tt>
</tt><tt>{-# COMPLETE N, J :: Maybe #-}</tt><tt>
</tt></pre><p><br>
</p><p>Instead if we could specify the type with
its free vars, we could refer to them in conlike
signatures:</p>
<pre><span class="m_3081504951675166151p">{-# COMPLETE N, [</span><span class="m_3081504951675166151p"><span class="m_3081504951675166151kt"> J</span></span><span class="m_3081504951675166151p"><span class="m_3081504951675166151kt"></span> <span class="m_3081504951675166151ow">::</span> a -> Maybe a ] :: Maybe a #-}</span></pre><p>The COMPLETE pragma for LL could be:<span class="m_3081504951675166151p"></span><br>
<span class="m_3081504951675166151p"></span></p>
<pre><pre><span class="m_3081504951675166151p">{-# COMPLETE [</span><span class="m_3081504951675166151p"><span class="m_3081504951675166151kt"> LL</span> <span class="m_3081504951675166151ow">::</span> <span class="m_3081504951675166151kt">HasSrcSpan</span> a <span class="m_3081504951675166151ow">=></span> <span class="m_3081504951675166151kt">SrcSpan</span> <span class="m_3081504951675166151ow">-></span> <span class="m_3081504951675166151kt">SrcSpanLess</span> a <span class="m_3081504951675166151ow">-></span> a ] :: a #-}
</span></pre></pre>
<br><p>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]):<span class="m_3081504951675166151p"></span><br>
<span class="m_3081504951675166151p"></span></p>
<pre><pre><span class="m_3081504951675166151p">{-# COMPLETE [</span><span class="m_3081504951675166151p"><span class="m_3081504951675166151kt"> V</span> <span class="m_3081504951675166151ow">::</span> </span><span class="m_3081504951675166151p"><span class="m_3081504951675166151p">(c :< cs) => c -> Variant cs</span>
| c <- cs
] :: Variant cs
#-}</span>
</pre>
> 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 <b class="m_3081504951675166151moz-txt-star"><span class="m_3081504951675166151moz-txt-tag">*</span>type constructor<span class="m_3081504951675166151moz-txt-tag">*</span></b>. 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.
</pre><p>Could we use a mechanism similar to instance
resolution (with FlexibleInstances) for the checker to
return matching COMPLETE sets instead?</p>
<pre>--Sylvain
[1] <a class="m_3081504951675166151moz-txt-link-freetext" href="https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html" target="_blank">https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html</a>
<span class="m_3081504951675166151p"></span></pre>
</div>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a class="m_3081504951675166151moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</div>
</blockquote>
</div>
<br>
</div>
</blockquote>
</div>
</div></blockquote></div><br></div></div></div>_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>