Optimizing "counting" GADTs

[Matthew Pickering]

David, Carter,

It would be nice to use pattern synonyms for this task but they do not
work quite as expected as they don't cause type refinement.

I quickly assembled this note to explain why.

http://mpickering.github.io/posts/2016-06-18-why-no-refinement.html

Matt

On Fri, May 27, 2016 at 4:50 AM, David Feuer <david.feuer at gmail.com> wrote:
> Scratch that. I think you might be right.
>
> On May 25, 2016 8:40 PM, "David Feuer" <david.feuer at gmail.com> wrote:
>>
>> Partially. Unfortunately, bidirectional pattern synonyms tie the types of
>> the pattern synonyms to the types of the smart constructors for no good
>> reason, making them (currently) inappropriate. But fixing that problem would
>> offer one way to this optimization, I think.
>>
>> On May 25, 2016 8:37 PM, "Carter Schonwald" <carter.schonwald at gmail.com>
>> wrote:
>>
>> could this be simulated/modeled with pattern synonyms?
>>
>> On Wed, May 25, 2016 at 7:51 PM, David Feuer <david.feuer at gmail.com>
>> wrote:
>>>
>>> I've started a wiki page,
>>> https://ghc.haskell.org/trac/ghc/wiki/OptimizeCountingGADTs , to consider
>>> optimizing GADTs that look like natural numbers but that possibly have
>>> "heavy zeros". Please take a look.
>>>
>>>
>>> _______________________________________________
>>> ghc-devs mailing list
>>> ghc-devs at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>>
>>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>