Avoiding construction of dead dictionaries

newer
-dinline-check for symbolic names?

Michael Sperber

6 Aug 2021 6 Aug '21

9:06 a.m.

I have another optimization problem. ConCat includes this definition: (<+) :: Con a => (Con b => r) -> (a |- b) -> r r <+ Entail (Sub Dict) = r The right-hand argument of <+ leads to a dictionary construction that is a proof of a certain property, but the dictionary itself ends up being dead, like so: case $w$dOpCon_r2kGJ ... of { (# ww1_s27L3 #) -> ... } ^^^^^^^^^ never used Yet, ghc (8.10.4) never elides this code. (I'm naively assuming because of the unboxed tuple, but actually have no clue.) Is there any chance of convincing ghc of erasing the dictionary construction? Help would be much appreciated! -- Regards, Mike

Show replies by date

Tom Smeding

6 Aug 6 Aug

10:55 a.m.

Would it not be unsound for ghc to elide dictionary construction here? After all, the right-hand side might actually be a bottom (e.g. undefined) at run-time, in which case the pattern match cannot succeed according to the semantics of Haskell. I suspect that if you make the pattern match lazy (i.e. ~(Entail (Sub Dict))) or ignore the argument altogether (i.e. _), dictionary construction will be elided. - Tom -------- Original Message -------- On 6 Aug 2021, 15:06, Michael Sperber wrote:

...

I have another optimization problem. ConCat includes this definition:

(<+) :: Con a => (Con b => r) -> (a |- b) -> r r <+ Entail (Sub Dict) = r

The right-hand argument of <+ leads to a dictionary construction that is a proof of a certain property, but the dictionary itself ends up being dead, like so:

case $w$dOpCon_r2kGJ ... of { (# ww1_s27L3 #) -> ... } ^^^^^^^^^ never used

Yet, ghc (8.10.4) never elides this code. (I'm naively assuming because of the unboxed tuple, but actually have no clue.)

Is there any chance of convincing ghc of erasing the dictionary construction?

Help would be much appreciated!

-- Regards, Mike

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Michael Sperber

9 Aug 9 Aug

9:24 a.m.

Thanks for thinking about this one! On Fri, Aug 06 2021, Tom Smeding wrote:

...

Would it not be unsound for ghc to elide dictionary construction here? After all, the right-hand side might actually be a bottom (e.g. undefined) at run-time, in which case the pattern match cannot succeed according to the semantics of Haskell.

But wouldn't that imply that ghc can build dictionary-construction code that evaluates to bottom? Can that happen?

...

I suspect that if you make the pattern match lazy (i.e. ~(Entail (Sub Dict))) or ignore the argument altogether (i.e. _), dictionary construction will be elided.

Thanks for the hint! ghc gives me this unfortunately, implying that it agreed with your first comment: src/ConCat/Category.hs:190:29: error: • Could not deduce: Con b arising from a use of ‘r’ from the context: Con a bound by the type signature for: (<+) :: forall a b r. Con a => (Con b => r) -> (a |- b) -> r at src/ConCat/Category.hs:189:1-46 • In the expression: r In an equation for ‘<+’: r <+ ~(Entail (Sub Dict)) = r • Relevant bindings include r :: Con b => r (bound at src/ConCat/Category.hs:190:1) (<+) :: (Con b => r) -> (a |- b) -> r (bound at src/ConCat/Category.hs:190:3) | 190 | r <+ ~(Entail (Sub Dict)) = r | ^ Other ideas welcome! -- Regards, Mike

Tom Smeding

11:26 a.m.

Hi Mike,

...

But wouldn't that imply that ghc can build dictionary-construction code

...

that evaluates to bottom? Can that happen?

I assume no, but here the dictionary is embedded as a field in the GADT, right? So if the data value is bottom, there is not even a dictionary to be found, let alone not-bottom. This assumes that the Dict in `Entail (Sub Dict)` is a GADT like Dict :: Con b => Dict something where the Con dictionary is contained in the GADT. Remember that in Core, dictionaries are values, and there is no difference between => and ->. - Tom -------- Original Message -------- On 9 Aug 2021, 15:24, Michael Sperber < sperber@deinprogramm.de> wrote: Thanks for thinking about this one! On Fri, Aug 06 2021, Tom Smeding wrote:

...

Would it not be unsound for ghc to elide dictionary construction here?

...

After all, the right-hand side might actually be a bottom

...

(e.g. undefined) at run-time, in which case the pattern match cannot

...

succeed according to the semantics of Haskell.

But wouldn't that imply that ghc can build dictionary-construction code that evaluates to bottom? Can that happen?

...

I suspect that if you make the pattern match lazy (i.e. ~(Entail (Sub

...

Dict))) or ignore the argument altogether (i.e. _), dictionary

...

construction will be elided.

Brandon Allbery

11:31 a.m.

We haven't figured out what they did, but the other day we had someone in #haskell with an infinite loop evaluating a dictionary. So apparently it is possible for a dictionary to be bottom somehow. On Mon, Aug 9, 2021 at 11:27 AM Tom Smeding wrote:

...

Hi Mike,

...
But wouldn't that imply that ghc can build dictionary-construction code

...
that evaluates to bottom? Can that happen?

I assume no, but here the dictionary is embedded as a field in the GADT, right? So if the data value is bottom, there is not even a dictionary to be found, let alone not-bottom.

This assumes that the Dict in `Entail (Sub Dict)` is a GADT like

Dict :: Con b => Dict something

where the Con dictionary is contained in the GADT. Remember that in Core, dictionaries are values, and there is no difference between => and ->.

- Tom

-------- Original Message --------

On 9 Aug 2021, 15:24, Michael Sperber < sperber@deinprogramm.de> wrote:

Thanks for thinking about this one!

On Fri, Aug 06 2021, Tom Smeding wrote:

...
Would it not be unsound for ghc to elide dictionary construction here?

...
After all, the right-hand side might actually be a bottom

...
(e.g. undefined) at run-time, in which case the pattern match cannot

...
succeed according to the semantics of Haskell.

But wouldn't that imply that ghc can build dictionary-construction code

that evaluates to bottom? Can that happen?

...
I suspect that if you make the pattern match lazy (i.e. ~(Entail (Sub

...
Dict))) or ignore the argument altogether (i.e. _), dictionary

...
construction will be elided.

Thanks for the hint! ghc gives me this unfortunately, implying that it

agreed with your first comment:

src/ConCat/Category.hs:190:29: error:

• Could not deduce: Con b arising from a use of ‘r’

from the context: Con a

bound by the type signature for:

(<+) :: forall a b r. Con a => (Con b => r) -> (a |- b) -> r

at src/ConCat/Category.hs:189:1-46

• In the expression: r

In an equation for ‘<+’: r <+ ~(Entail (Sub Dict)) = r

• Relevant bindings include

r :: Con b => r (bound at src/ConCat/Category.hs:190:1)

(<+) :: (Con b => r) -> (a |- b) -> r

(bound at src/ConCat/Category.hs:190:3)

|

190 | r <+ ~(Entail (Sub Dict)) = r

| ^

Other ideas welcome!

--

Regards,

Mike

_______________________________________________

Glasgow-haskell-users mailing list

Glasgow-haskell-users@haskell.org

http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

-- brandon s allbery kf8nh allbery.b@gmail.com

Simon Peyton Jones

11:56 a.m.

...

. So apparently it is possible for a dictionary to be bottom somehow. That should not happen.

Except in the case of single-method dictionaries like class C a where op :: a -> a In these cases the "dictionary" is represented by a newtype, like this newtype C a = MkC (a->a) Then you could say instance C Int where op = bottom and now a (C Int) dictionary is simply bottom. It would be easy to change this decision, and use a data constructor even for single-method classes. Some programs would become slightly less efficient, but things would be a bit more uniform. If there was a real advantage to doing this, it'd definitely be worth measuring the perf cost (if any). Simon From: Glasgow-haskell-users On Behalf Of Brandon Allbery Sent: 09 August 2021 16:32 To: Tom Smeding Cc: GHC users ; sperber@deinprogramm.de Subject: Re: Avoiding construction of dead dictionaries We haven't figured out what they did, but the other day we had someone in #haskell with an infinite loop evaluating a dictionary. So apparently it is possible for a dictionary to be bottom somehow. On Mon, Aug 9, 2021 at 11:27 AM Tom Smeding mailto:x@tomsmeding.com> wrote: Hi Mike,

...

But wouldn't that imply that ghc can build dictionary-construction code

...

that evaluates to bottom? Can that happen?

I assume no, but here the dictionary is embedded as a field in the GADT, right? So if the data value is bottom, there is not even a dictionary to be found, let alone not-bottom. This assumes that the Dict in `Entail (Sub Dict)` is a GADT like Dict :: Con b => Dict something where the Con dictionary is contained in the GADT. Remember that in Core, dictionaries are values, and there is no difference between => and ->. - Tom -------- Original Message -------- On 9 Aug 2021, 15:24, Michael Sperber < sperber@deinprogramm.demailto:sperber@deinprogramm.de> wrote: Thanks for thinking about this one! On Fri, Aug 06 2021, Tom Smeding mailto:x@tomsmeding.com> wrote:

...

Would it not be unsound for ghc to elide dictionary construction here?

...

After all, the right-hand side might actually be a bottom

...

(e.g. undefined) at run-time, in which case the pattern match cannot

...

succeed according to the semantics of Haskell.

But wouldn't that imply that ghc can build dictionary-construction code that evaluates to bottom? Can that happen?

...

I suspect that if you make the pattern match lazy (i.e. ~(Entail (Sub

...

Dict))) or ignore the argument altogether (i.e. _), dictionary

...

construction will be elided.

Thanks for the hint! ghc gives me this unfortunately, implying that it agreed with your first comment: src/ConCat/Category.hs:190:29: error: * Could not deduce: Con b arising from a use of 'r' from the context: Con a bound by the type signature for: (<+) :: forall a b r. Con a => (Con b => r) -> (a |- b) -> r at src/ConCat/Category.hs:189:1-46 * In the expression: r In an equation for '<+': r <+ ~(Entail (Sub Dict)) = r * Relevant bindings include r :: Con b => r (bound at src/ConCat/Category.hs:190:1) (<+) :: (Con b => r) -> (a |- b) -> r (bound at src/ConCat/Category.hs:190:3) | 190 | r <+ ~(Entail (Sub Dict)) = r | ^ Other ideas welcome! -- Regards, Mike _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.orgmailto:Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-users&data=04%7C01%7Csimonpj%40microsoft.com%7C7bf3769704884ed6592e08d95b4aeb26%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637641199636853840%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=ix06XQPvpu%2B1PLzoc5rRQM6cMv8yPF6o87uVwD0sUwQ%3D&reserved=0 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.orgmailto:Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-users&data=04%7C01%7Csimonpj%40microsoft.com%7C7bf3769704884ed6592e08d95b4aeb26%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637641199636863837%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=sQDTBnklNv7YLRvhiY5CEtbZgcZT8p7RR%2Bw57sCqFJk%3D&reserved=0 -- brandon s allbery kf8nh allbery.b@gmail.commailto:allbery.b@gmail.com

Brandon Allbery

11:59 a.m.

They didn't show code (this is sadly common), so we had only speculation. :( On Mon, Aug 9, 2021 at 11:56 AM Simon Peyton Jones wrote:

...

...
. So apparently it is possible for a dictionary to be bottom somehow.

That should not happen.

Except in the case of single-method dictionaries like

class C a where op :: a -> a

In these cases the “dictionary” is represented by a newtype, like this

newtype C a = MkC (a->a)

Then you could say

instance C Int where

op = bottom

and now a (C Int) dictionary is simply bottom.

It would be easy to change this decision, and use a data constructor even for single-method classes. Some programs would become slightly less efficient, but things would be a bit more uniform. If there was a real advantage to doing this, it’d definitely be worth measuring the perf cost (if any).

Simon

*From:* Glasgow-haskell-users *On Behalf Of *Brandon Allbery *Sent:* 09 August 2021 16:32 *To:* Tom Smeding *Cc:* GHC users ; sperber@deinprogramm.de *Subject:* Re: Avoiding construction of dead dictionaries

We haven't figured out what they did, but the other day we had someone in #haskell with an infinite loop evaluating a dictionary. So apparently it is possible for a dictionary to be bottom somehow.

On Mon, Aug 9, 2021 at 11:27 AM Tom Smeding wrote:

Hi Mike,

...
But wouldn't that imply that ghc can build dictionary-construction code

...
that evaluates to bottom? Can that happen?

I assume no, but here the dictionary is embedded as a field in the GADT, right? So if the data value is bottom, there is not even a dictionary to be found, let alone not-bottom.

This assumes that the Dict in `Entail (Sub Dict)` is a GADT like

Dict :: Con b => Dict something

where the Con dictionary is contained in the GADT. Remember that in Core, dictionaries are values, and there is no difference between => and ->.

- Tom

-------- Original Message --------

On 9 Aug 2021, 15:24, Michael Sperber < sperber@deinprogramm.de> wrote:

Thanks for thinking about this one!

On Fri, Aug 06 2021, Tom Smeding wrote:

...
Would it not be unsound for ghc to elide dictionary construction here?

...
After all, the right-hand side might actually be a bottom

...
(e.g. undefined) at run-time, in which case the pattern match cannot

...
succeed according to the semantics of Haskell.

But wouldn't that imply that ghc can build dictionary-construction code

that evaluates to bottom? Can that happen?

...
I suspect that if you make the pattern match lazy (i.e. ~(Entail (Sub

...
Dict))) or ignore the argument altogether (i.e. _), dictionary

...
construction will be elided.

Thanks for the hint! ghc gives me this unfortunately, implying that it

agreed with your first comment:

src/ConCat/Category.hs:190:29: error:

• Could not deduce: Con b arising from a use of ‘r’

from the context: Con a

bound by the type signature for:

(<+) :: forall a b r. Con a => (Con b => r) -> (a |- b) -> r

at src/ConCat/Category.hs:189:1-46

• In the expression: r

In an equation for ‘<+’: r <+ ~(Entail (Sub Dict)) = r

• Relevant bindings include

r :: Con b => r (bound at src/ConCat/Category.hs:190:1)

(<+) :: (Con b => r) -> (a |- b) -> r

(bound at src/ConCat/Category.hs:190:3)

|

190 | r <+ ~(Entail (Sub Dict)) = r

| ^

Other ideas welcome!

--

Regards,

Mike

_______________________________________________

Glasgow-haskell-users mailing list

Glasgow-haskell-users@haskell.org

http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-users&data=04%7C01%7Csimonpj%40microsoft.com%7C7bf3769704884ed6592e08d95b4aeb26%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637641199636853840%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=ix06XQPvpu%2B1PLzoc5rRQM6cMv8yPF6o87uVwD0sUwQ%3D&reserved=0

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-users&data=04%7C01%7Csimonpj%40microsoft.com%7C7bf3769704884ed6592e08d95b4aeb26%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637641199636863837%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=sQDTBnklNv7YLRvhiY5CEtbZgcZT8p7RR%2Bw57sCqFJk%3D&reserved=0

--

brandon s allbery kf8nh

allbery.b@gmail.com

-- brandon s allbery kf8nh allbery.b@gmail.com

Claude Heiland-Allen

noon

Hi all, On 09/08/2021 16:31, Brandon Allbery wrote:

...

We haven't figured out what they did, but the other day we had someone in #haskell with an infinite loop evaluating a dictionary. So apparently it is possible for a dictionary to be bottom somehow.

I managed to do something like this once: I was using type level natural numbers to parameterize my type, and through carelessness my dictionary for `T n` depended on the dictionary for `T (Succ n)`. My heap profile was a triangular wedge with space taken up by dictionaries growing linearly without bound. Claude -- https://mathr.co.uk

Simon Peyton Jones

12:05 p.m.

Hi Mike | The right-hand argument of <+ leads to a dictionary construction that is a | proof of a certain property, but the dictionary itself ends up being dead, | like so: | | case $w$dOpCon_r2kGJ ... | of | { (# ww1_s27L3 #) -> ... } | ^^^^^^^^^ | never used GHC needs to figure out that $w$dOpCon_r2kGJ always terminates, without throwing an exception etc. That can't be too hard, and Sebastian Graf has thought about it quite a bit. Could you offer a small repro case, with a pointer to evidence that it matters in practice, and open a ticket? Thanks Simon | -----Original Message----- | From: Glasgow-haskell-users On | Behalf Of Michael Sperber | Sent: 06 August 2021 14:06 | To: glasgow-haskell-users@haskell.org | Subject: Avoiding construction of dead dictionaries | | [You don't often get email from sperber@deinprogramm.de. Learn why this is | important at http://aka.ms/LearnAboutSenderIdentification.] | | I have another optimization problem. ConCat includes this definition: | | (<+) :: Con a => (Con b => r) -> (a |- b) -> r r <+ Entail (Sub Dict) = r | | The right-hand argument of <+ leads to a dictionary construction that is a | proof of a certain property, but the dictionary itself ends up being dead, | like so: | | case $w$dOpCon_r2kGJ ... | of | { (# ww1_s27L3 #) -> ... } | ^^^^^^^^^ | never used | | Yet, ghc (8.10.4) never elides this code. (I'm naively assuming because of | the unboxed tuple, but actually have no clue.) | | Is there any chance of convincing ghc of erasing the dictionary | construction? | | Help would be much appreciated! | | -- | Regards, | Mike | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskel | l.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell- | users&data=04%7C01%7Csimonpj%40microsoft.com%7C301c6f15cc1142fc645908d95 | 8dc725a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637638526127543532%7CUn | known%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJX | VCI6Mn0%3D%7C2000&sdata=fh2YiJ5NuDMPzpzzxsAL0MyceMFH0MuveNgvTo7ZNow%3D&a | mp;reserved=0

Michael Sperber

12 Aug 12 Aug

5:15 a.m.

On Mon, Aug 09 2021, Simon Peyton Jones wrote:

...

Could you offer a small repro case, with a pointer to evidence that it matters in practice, and open a ticket?

I'll try my best, but I'm unsure how I would generate evidence. Could you give me a hint? Is there any way to see how far evaluates the dictionary construction to be able to match on that unboxed tuple? -- Regards, Mike

Simon Peyton Jones

8:01 a.m.

Hi Mike Repro case is something like * Here is a source or files * Compile like this * Look at the generated Core...observe silly thing happening Evidence of importance could be as simple as "in my application I'm seeing a lot of these redundant dictionaries being built for no reason". Or, stronger "this is slowing my application down by 5%". TL;DR: is this just a curiosity that you noticed, or is it something that matters to you, and if so why? | Is there any way to see how far evaluates the dictionary construction to be | able to match on that unboxed tuple? Not sure what you mean here, but once we have a repro case we can discuss. Worth opening a ticket too -- email is easily lost. Thanks Simon | -----Original Message----- | From: Michael Sperber | Sent: 12 August 2021 10:15 | To: Simon Peyton Jones | Cc: Sebastian Graf ; glasgow-haskell-users@haskell.org | Subject: Re: Avoiding construction of dead dictionaries | | | On Mon, Aug 09 2021, Simon Peyton Jones wrote: | | > Could you offer a small repro case, with a pointer to evidence that it | matters in practice, and open a ticket? | | I'll try my best, but I'm unsure how I would generate evidence. Could you | give me a hint? | | Is there any way to see how far evaluates the dictionary construction to be | able to match on that unboxed tuple? | | -- | Regards, | Mike