Re: Optimizing "counting" GADTs

[David Feuer]

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" 
wrote:

could this be simulated/modeled with pattern synonyms?

On Wed, May 25, 2016 at 7:51 PM, David Feuer  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@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Optimizing "counting" GADTs

[David Feuer]

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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: instances for closed type families

[Alan & Kim Zimmerman]

Ryan

The discussion was in this thread [1], but went off list at some point.

The relevant part of the off-list discussion, quoting Philip Hölzenspies  is

"UndecidableInstances comes from having to constrain the type that the
PostTcType-family projects to, besides the arguments of the AST-types;

instance (Data (PostTcType id), Data id) => Data (HsIPBinds id) where ...

If we could derive that from the definition of PostTcType (and I don't see
why we couldn't from a closed family; not sure about the open ones), we
would only need to constrain "id" and, thus, we could actually just use
"deriving".

Of the diff, btw, I don't get why PendingRnSplice is suddenly
parameterised... Thoughts?

Ph."

and SimonPJ responded

"

Why do we need UndecidableInstances?



I still (currently) think we can use open type families perfectly well.
Why won’t that work?  (Could switch to closed after GHC’s bootstrap caught
up.)



Simon

 "

So basically there is a mention that it may be possible.

Alan





[1] https://mail.haskell.org/pipermail/ghc-devs/2014-July/005808.html

On Wed, May 25, 2016 at 9:09 PM, Ryan Scott  wrote:

> > I recall there was some discussion when the PostRn/PostTc stuff went in
> around the closed type family solution being better, and I thought it was
> that the Data instances would be more easy to define.
>
> Do you happen to know where this discussion can be found online? To be
> honest, I'm not sure whether closed vs. open type families is even a
> relevant distinction in this case. Regardless of where NameOrRdrName
> is open or closed, the following code won't compile:
>
> data Foo a = Foo (NameOrRdrName a) deriving Data
>
> And that's simply because GHC hasn't enough information to know
> whether Foo a will always resolve to something that's a Data instance.
> Even if NameOrRdrName is closed, someone could still use types like
> NameOrRdrName Char.
>
> If NameOrRdrName were somehow made to be injective, then it'd be a
> different story. But I doubt that such a thing is possible in this
> case (based on the definition of NameOrRdrName you gave), so I think
> we'll just have to settle for turning on UndecidableInstances and
> writing code that we know won't throw the typechecker into a loop.
>
> Ryan S.
>
> On Wed, May 25, 2016 at 2:52 PM, Alan & Kim Zimmerman
>  wrote:
> > Ryan / Simon, thanks.
> >
> > I have been working it in the way the PostRn stuff was done, but then it
> > struck me there may be an easier way.
> >
> > I recall there was some discussion when the PostRn/PostTc stuff went in
> > around the closed type family solution being better, and I thought it was
> > that the Data instances would be more easy to define.
> >
> > And I also seem to recall that the closed type families should be able to
> > get rid of the UndecidableInstances pragma, but I do not recall the
> details.
> >
> > We are now able to use closed type families in GHC source, as it is
> > supported from GHC 7.8 onwards
> >
> > Regards
> >   Alan
> >
> >
> > On Wed, May 25, 2016 at 8:42 PM, Ryan Scott 
> wrote:
> >>
> >> Simon is right, you cannot use a type family as an instance head. But
> why
> >> do you need to? Typically, if you're deriving a Data instance that
> involves
> >> type families, the type families would be inside another data type. A
> >> real-world example is HsBindLR [1]:
> >>
> >> data HsBindLR idL idR
> >>   = FunBind {
> >>   ...
> >>   bind_fvs :: PostRn idL NameSet,
> >>   ...
> >> } | ...
> >>
> >> where PostRn is a type family [2]. Now, you can't simply derive Data for
> >> HsBindLR, because GHC has no way of knowing what PostRn will evaluate
> to!
> >> But you can use standalone deriving to get what you want:
> >>
> >> deriving instance (Data (PostRn idL NameSet), ...) => Data (HsBindLR
> >> idL idR)
> >>
> >> And in fact, this is what GHC does [3], using a convenient type synonyms
> >> for the long, sprawling context you need [4].
> >>
> >> So in your example, while you can't directly create a Data instance for
> >> NameOrRdrName itself, you can quite easily create Data instances for
> >> anything that might use NameOrRdrName. Does that work for your use
> cases?
> >>
> >> Ryan S.
> >> -
> >> [1]
> >>
> http://git.haskell.org/ghc.git/blob/bdc555885b8898684549eca70053c9ce0ec7fa39:/compiler/hsSyn/HsBinds.hs#l111
> >> [2]
> >>
> http://git.haskell.org/ghc.git/blob/bdc555885b8898684549eca70053c9ce0ec7fa39:/compiler/hsSyn/PlaceHolder.hs#l47
> >> [3]
> >>
> http://git.haskell.org/ghc.git/blob/bdc555885b8898684549eca70053c9ce0ec7fa39:/compiler/hsSyn/HsBinds.hs#l264
> >> [4]
> >>
> http://git.haskell.org/ghc.git/blob/bdc555885b8898684549eca70053c9ce0ec7fa39:/compiler/hsSyn/PlaceHolder.hs#l102
> >>
> >> ___
> >> ghc-devs mailing list
> >> ghc-devs@haskell.org
> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> >>
> >
>

Re: Unpacking single-field, single-strict-constructor GADTs and existentials

[David Feuer]

I've started a wiki page at
https://ghc.haskell.org/trac/ghc/wiki/NewtypeOptimizationForGADTS

On Wed, May 25, 2016 at 3:27 AM, Simon Peyton Jones
 wrote:
> I'm not following the details of this discussion.  Would it be possible to 
> write a compact summary, with the key examples, in the appropriate ticket?
>
> I think that https://ghc.haskell.org/trac/ghc/ticket/10016 is one such 
> ticket, but I think there may be more than one issue at stake here.  For 
> example, #10016 can be done in a strongly typed way in Core; but #1965 cannot 
> (so far as I know).
>
> It could also help to have a wiki page to summarise the cluster of issues, 
> pointing to the appropriate tickets for individual cases.
>
> An articulate summary will make it much more likely that progress is made! 
> Thanks.
>
> Simon
>
> | -Original Message-
> | From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of David 
> Feuer
> | Sent: 24 May 2016 23:14
> | To: Carter Schonwald 
> | Cc: ghc-devs 
> | Subject: Re: Unpacking single-field, single-strict-constructor GADTs and
> | existentials
> |
> | Unboxing, per se, is not required; only newtype optimization. I
> | believe Ed would probably have mentioned something when I discussed
> | the issue with him if he'd already had an idea for hacking around it.
> | Instead, he said he wanted the feature too.
> |
> | On Tue, May 24, 2016 at 6:03 PM, Carter Schonwald
> |  wrote:
> | > Phrased differently: there's a subclass of existential data types which
> | have
> | > a well behaved unboxed memory layout?
> | >
> | > @ David : have you tried simulating this in userland using eds structs /
> | > structures lib?
> | >
> | > On Tuesday, May 24, 2016, David Feuer  wrote:
> | >>
> | >> I should mention that while this does not require UNPACKing sum types (or
> | >> any of the difficult trade-offs that involves), it lets programmers
> | >> accomplish such unpacking by hand under sufficiently general conditions 
> to
> | >> be quite useful in practice. As long as the set of types involved is
> | closed,
> | >> it'll do.
> | >>
> | >> David Feuer  writes:
> | >>
> | >> > Given
> | >> >
> | >> > data Big a = B1 !(Small1 a) | B2 !(Small2 a) | B3 !(Small3 a), where 
> the
> | >> > Small types are (possibly recursive) sums, it's generally possible to
> | >> > express that as something like
> | >> >
> | >> > data Selector = One | Two | Three
> | >> > data Big a = forall (x :: Selector) .
> | >> >Big !(BigG x a)
> | >> > data BigG x a where
> | >> >   GB1a :: some -> fields -> BigG 'One a
> | >> >   GB1b :: fields -> BigG 'One a
> | >> >   GB2a :: whatever -> BigG 'Two a
> | >> >   GB3a :: yeah -> BigG 'Three a
> | >> >
> | >> > Making one big GADT from all the constructors of the "small" types, and
> | >> > then wrapping it up in an existential. That's what I meant about
> | >> > "unpacking". But for efficiency purposes, that wrapper needs the 
> newtype
> | >> > optimization.
> | >>
> | >> Yes, but you'd need to unbox a sum in this case, no? I think this is the
> | >> first issue that you need to solve before you can talk about dealing
> | >> with the polymorphism issue (although hopefully Ömer will make progress
> | >> on this for 8.2).
> | >>
> | >> Cheers,
> | >>
> | >> - Ben
> | ___
> | ghc-devs mailing list
> | ghc-devs@haskell.org
> | 
> https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell.
> | org%2fcgi-bin%2fmailman%2flistinfo%2fghc-
> | 
> devs=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce98f7b01dbeb47cc8d3908
> | 
> d38420b38b%7c72f988bf86f141af91ab2d7cd011db47%7c1=gFnWAB1of%2fp%2b0IXkD
> | CgcBbyxHkS7%2b4BusMl%2fs0rUySM%3d
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Unpacking single-field, single-strict-constructor GADTs and existentials

[David Feuer]

#1965 *as modified by comments #7 and #9* is pretty much what I'm hoping for.

On Wed, May 25, 2016 at 3:27 AM, Simon Peyton Jones
 wrote:
> I'm not following the details of this discussion.  Would it be possible to 
> write a compact summary, with the key examples, in the appropriate ticket?
>
> I think that https://ghc.haskell.org/trac/ghc/ticket/10016 is one such 
> ticket, but I think there may be more than one issue at stake here.  For 
> example, #10016 can be done in a strongly typed way in Core; but #1965 cannot 
> (so far as I know).
>
> It could also help to have a wiki page to summarise the cluster of issues, 
> pointing to the appropriate tickets for individual cases.
>
> An articulate summary will make it much more likely that progress is made! 
> Thanks.
>
> Simon
>
> | -Original Message-
> | From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of David 
> Feuer
> | Sent: 24 May 2016 23:14
> | To: Carter Schonwald 
> | Cc: ghc-devs 
> | Subject: Re: Unpacking single-field, single-strict-constructor GADTs and
> | existentials
> |
> | Unboxing, per se, is not required; only newtype optimization. I
> | believe Ed would probably have mentioned something when I discussed
> | the issue with him if he'd already had an idea for hacking around it.
> | Instead, he said he wanted the feature too.
> |
> | On Tue, May 24, 2016 at 6:03 PM, Carter Schonwald
> |  wrote:
> | > Phrased differently: there's a subclass of existential data types which
> | have
> | > a well behaved unboxed memory layout?
> | >
> | > @ David : have you tried simulating this in userland using eds structs /
> | > structures lib?
> | >
> | > On Tuesday, May 24, 2016, David Feuer  wrote:
> | >>
> | >> I should mention that while this does not require UNPACKing sum types (or
> | >> any of the difficult trade-offs that involves), it lets programmers
> | >> accomplish such unpacking by hand under sufficiently general conditions 
> to
> | >> be quite useful in practice. As long as the set of types involved is
> | closed,
> | >> it'll do.
> | >>
> | >> David Feuer  writes:
> | >>
> | >> > Given
> | >> >
> | >> > data Big a = B1 !(Small1 a) | B2 !(Small2 a) | B3 !(Small3 a), where 
> the
> | >> > Small types are (possibly recursive) sums, it's generally possible to
> | >> > express that as something like
> | >> >
> | >> > data Selector = One | Two | Three
> | >> > data Big a = forall (x :: Selector) .
> | >> >Big !(BigG x a)
> | >> > data BigG x a where
> | >> >   GB1a :: some -> fields -> BigG 'One a
> | >> >   GB1b :: fields -> BigG 'One a
> | >> >   GB2a :: whatever -> BigG 'Two a
> | >> >   GB3a :: yeah -> BigG 'Three a
> | >> >
> | >> > Making one big GADT from all the constructors of the "small" types, and
> | >> > then wrapping it up in an existential. That's what I meant about
> | >> > "unpacking". But for efficiency purposes, that wrapper needs the 
> newtype
> | >> > optimization.
> | >>
> | >> Yes, but you'd need to unbox a sum in this case, no? I think this is the
> | >> first issue that you need to solve before you can talk about dealing
> | >> with the polymorphism issue (although hopefully Ömer will make progress
> | >> on this for 8.2).
> | >>
> | >> Cheers,
> | >>
> | >> - Ben
> | ___
> | ghc-devs mailing list
> | ghc-devs@haskell.org
> | 
> https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell.
> | org%2fcgi-bin%2fmailman%2flistinfo%2fghc-
> | 
> devs=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce98f7b01dbeb47cc8d3908
> | 
> d38420b38b%7c72f988bf86f141af91ab2d7cd011db47%7c1=gFnWAB1of%2fp%2b0IXkD
> | CgcBbyxHkS7%2b4BusMl%2fs0rUySM%3d
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs