<html>
<head>
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>I've just found this related ticket:
<a class="moz-txt-link-freetext" href="https://ghc.haskell.org/trac/ghc/ticket/14422">https://ghc.haskell.org/trac/ghc/ticket/14422</a></p>
<p><br>
</p>
<div class="moz-cite-prefix">On 10/26/18 7:04 PM, Richard Eisenberg
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:DFF38AF9-3F24-4539-817C-306884987021@cs.brynmawr.edu">
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
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 class=""><br class="">
</div>
<div class="">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 class=""><br class="">
</div>
<div class="">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 class=""><br class="">
</div>
<div class="">I take back my claim of "No types!" then, as this
does sound like it has the right properties.</div>
<div class=""><br class="">
</div>
<div class="">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 class=""><br class="">
</div>
<div class="">Here's a stab at a formalization of this idea,
written in metatheory, not Haskell:</div>
<div class=""><br class="">
</div>
<div class="">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 class=""><br class="">
</div>
<div class="">What do we think of this design? Of course, the
challenge is in building C, but we'll tackle that next.</div>
<div class=""><br class="">
</div>
<div class="">Richard<br class="">
<div class="">
<div><br class="">
<blockquote type="cite" class="">
<div class="">On Oct 26, 2018, at 5:20 AM, Sylvain Henry
<<a href="mailto:sylvain@haskus.fr" class=""
moz-do-not-send="true">sylvain@haskus.fr</a>>
wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252" class="">
<div text="#000000" bgcolor="#FFFFFF" class="">
<p class="">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 class="">1) How does the checker retrieve COMPLETE
sets.</p>
<p class="">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 class="">{-# COMPLETE LL #-}<br class="">
</p>
<p class="">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 class="">
</p>
<pre class="">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 class=""><br class="">
</p>
<p class="">2) COMPLETE set depending on the matched
type.</p>
<p class="">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
class="">
</p>
<pre class="">instance Complete (Variant cs) where
conlikes = [V @c | c <- cs] -- cs is a type list
</pre>
<p class="">(I don't really care about the pragma
syntax)</p>
<p class="">Sorry for the thread hijack!<br class="">
Regards,<br class="">
Sylvain<br class="">
</p>
<p class=""><br class="">
</p>
<div class="moz-cite-prefix">On 10/26/18 5:59 AM,
Richard Eisenberg wrote:<br class="">
</div>
<blockquote type="cite"
cite="mid:7031558E-BDD9-4571-A5C3-CFF486455BEA@cs.brynmawr.edu"
class="">
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252" class="">
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 class=""><br class="">
</div>
<div class="">{-# COMPLETE LL #-}</div>
<div class=""><br class="">
</div>
<div class="">No types! (That's a rare thing for me
to extol...)</div>
<div class=""><br class="">
</div>
<div class="">I feel I must be missing something
here.</div>
<div class=""><br class="">
</div>
<div class="">Thanks,</div>
<div class="">Richard<br class="">
<div class=""><br class="">
<blockquote type="cite" class="">
<div class="">On Oct 25, 2018, at 12:24 PM,
Sylvain Henry <<a
href="mailto:sylvain@haskus.fr" class=""
moz-do-not-send="true">sylvain@haskus.fr</a>>
wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<meta http-equiv="Content-Type"
content="text/html; charset=windows-1252"
class="">
<div text="#000000" bgcolor="#FFFFFF"
class="">
<pre class="moz-quote-pre" wrap="">> 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 class="">Currently we can specify the
type *constructor* in a COMPLETE pragma:</p>
<pre class=""><tt class="">pattern J :: a -> Maybe a</tt><tt class="">
</tt><tt class="">pattern J a = Just a</tt><tt class="">
</tt><tt class="">
</tt><tt class="">pattern N :: Maybe a</tt><tt class="">
</tt><tt class="">pattern N = Nothing</tt><tt class="">
</tt><tt class="">
</tt><tt class="">{-# COMPLETE N, J :: Maybe #-}</tt><tt class="">
</tt></pre>
<p class=""><br class="">
</p>
<p class="">Instead if we could specify
the type with its free vars, we could
refer to them in conlike signatures:</p>
<pre class=""><span class="p">{-# COMPLETE N, [</span><span class="p"><span class="kt"> J</span></span><span class="p"><span class="kt"></span> <span class="ow">::</span> a -> Maybe a ] :: Maybe a #-}</span></pre>
<p class="">The COMPLETE pragma for LL
could be:<span class="p"></span><br
class="">
<span class="p"></span></p>
<pre class=""><pre class=""><span class="p">{-# COMPLETE [</span><span class="p"><span class="kt"> LL</span> <span class="ow">::</span> <span class="kt">HasSrcSpan</span> a <span class="ow">=></span> <span class="kt">SrcSpan</span> <span class="ow">-></span> <span class="kt">SrcSpanLess</span> a <span class="ow">-></span> a ] :: a #-}
</span></pre></pre>
<br class="">
<p class="">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="p"></span><br
class="">
<span class="p"></span></p>
<pre class=""><pre class=""><span class="p">{-# COMPLETE [</span><span class="p"><span class="kt"> V</span> <span class="ow">::</span> </span><span class="p"><span class="p">(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="moz-txt-star"><span class="moz-txt-tag">*</span>type constructor<span class="moz-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 class="">Could we use a mechanism
similar to instance resolution (with
FlexibleInstances) for the checker to
return matching COMPLETE sets instead?</p>
<pre class="">--Sylvain
[1] <a class="moz-txt-link-freetext" href="https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html" moz-do-not-send="true">https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html</a>
<span class="p"></span></pre>
</div>
_______________________________________________<br class="">
ghc-devs mailing list<br class="">
<a href="mailto:ghc-devs@haskell.org"
class="" moz-do-not-send="true">ghc-devs@haskell.org</a><br
class="">
<a class="moz-txt-link-freetext"
href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs"
moz-do-not-send="true">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br
class="">
</div>
</blockquote>
</div>
<br class="">
</div>
</blockquote>
</div>
</div>
</blockquote>
</div>
<br class="">
</div>
</div>
</blockquote>
</body>
</html>