Optimizing "counting" GADTs

[David Feuer]

I would think the provided equalities could be constructed in a view
pattern, possibly using unsafeCoerce. Dictionaries are harder to come by,
but reflection might be an option. My two biggest gripes about pattern
synonyms are really

1. The constraints for "constructor" application are forced to be much
tighter than necessary. This is very sad because there doesn't seem to be
anything inherently difficult about fixing it--just allow the user to
specify the desired type signature for the synonym used as a constructor.
2. The exhaustivity check doesn't work yet.
On Jun 18, 2016 10:07 PM, "Matthew Pickering" <matthewtpickering at gmail.com>
wrote:

> 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
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160618/2ad07ae4/attachment.html>