[prev in list] [next in list] [prev in thread] [next in thread] 

List:       haskell-cafe
Subject:    Re: [Haskell-cafe] Pattern matching with singletons
From:       Paul Brauner <polux2001 () gmail ! com>
Date:       2013-03-27 12:45:53
Message-ID: CAJ32BF4H0rxJM0s3UHHZx3gjUjcc3u7P73cwB0_kOhN+-SVphw () mail ! gmail ! com
[Download RAW message or body]

[Attachment #2 (multipart/alternative)]


Very helpful, thanks! I may come back with more singleton/type families
questions :)


On Tue, Mar 26, 2013 at 6:41 PM, Richard Eisenberg <eir@cis.upenn.edu>wrote:

> Hello Paul,
>
> > ----- Forwarded message from Paul Brauner <polux2001@gmail.com> -----
>
> <snip>
>
> >   - is a ~ ('CC ('Left 'CA)) a consequence of the definitions of SCC,
> >   SLeft, ... (in which case GHC could infer it but for some reason can't)
> >   - or are these pattern + definitions not sufficient to prove that a
> >   ~ ('CC ('Left 'CA)) no matter what?
>
> The first one. GHC can deduce that (a ~ ('CC ('Left b))), for some fresh
> variable (b :: TA), but it can't yet take the next step and decide that,
> because TA has only one constructor, b must in fact be 'CA. In type-theory
> lingo, this deduction is called eta-expansion. There have been on-and-off
> debates about how best to add this sort of eta-expansion into GHC, but all
> seem to agree that it's not totally straightforward. For example, see GHC
> bug #7259. There's a non-negligible chance I will be taking a closer look
> into this at some point, but not for a few months, so don't hold your
> breath. I'm not aware of anyone else currently focusing on this problem
> either, I'm afraid.
>
> I'm glad you're finding use in the singletons package! Let me know if I
> can be of further help.
>
> Richard

[Attachment #5 (text/html)]

<div dir="ltr">Very helpful, thanks! I may come back with more singleton/type \
families questions :)</div><div class="gmail_extra"><br><br><div \
class="gmail_quote">On Tue, Mar 26, 2013 at 6:41 PM, Richard Eisenberg <span \
dir="ltr">&lt;<a href="mailto:eir@cis.upenn.edu" \
target="_blank">eir@cis.upenn.edu</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc \
solid;padding-left:1ex">Hello Paul,<br> <br>
&gt; ----- Forwarded message from Paul Brauner &lt;<a \
href="mailto:polux2001@gmail.com">polux2001@gmail.com</a>&gt; -----<br> <br>
&lt;snip&gt;<br>
<br>
&gt;   - is a ~ (&#39;CC (&#39;Left &#39;CA)) a consequence of the definitions of \
SCC,<br> <div class="im">&gt;   SLeft, ... (in which case GHC could infer it but for \
some reason can&#39;t)<br> </div>&gt;   - or are these pattern + definitions not \
sufficient to prove that a<br> <div class="im">&gt;   ~ (&#39;CC (&#39;Left &#39;CA)) \
no matter what?<br> <br>
</div>The first one. GHC can deduce that (a ~ (&#39;CC (&#39;Left b))), for some \
fresh variable (b :: TA), but it can&#39;t yet take the next step and decide that, \
because TA has only one constructor, b must in fact be &#39;CA. In type-theory lingo, \
this deduction is called eta-expansion. There have been on-and-off debates about how \
best to add this sort of eta-expansion into GHC, but all seem to agree that it&#39;s \
not totally straightforward. For example, see GHC bug #7259. There&#39;s a \
non-negligible chance I will be taking a closer look into this at some point, but not \
for a few months, so don&#39;t hold your breath. I&#39;m not aware of anyone else \
currently focusing on this problem either, I&#39;m afraid.<br>


<br>
I&#39;m glad you&#39;re finding use in the singletons package! Let me know if I can \
be of further help.<br> <span class="HOEnZb"><font color="#888888"><br>
Richard</font></span></blockquote></div><br></div>



_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[prev in list] [next in list] [prev in thread] [next in thread]