RE: Avoiding construction of dead dictionaries

2021-08-09 Thread Simon Peyton Jones via Glasgow-haskell-users
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 sper...@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-
|  usersdata=04%7C01%7Csimonpj%40microsoft.com%7C301c6f15cc1142fc645908d95
|  8dc725a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637638526127543532%7CUn
|  known%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJX
|  VCI6Mn0%3D%7C2000sdata=fh2YiJ5NuDMPzpzzxsAL0MyceMFH0MuveNgvTo7ZNow%3D
|  mp;reserved=0
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


Re: Avoiding construction of dead dictionaries

2021-08-09 Thread Claude Heiland-Allen

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


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


Re: Avoiding construction of dead dictionaries

2021-08-09 Thread Brandon Allbery
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 ;
> sper...@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 < sper...@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
> 

RE: Avoiding construction of dead dictionaries

2021-08-09 Thread Simon Peyton Jones via Glasgow-haskell-users
> . 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 ; sper...@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 < 
sper...@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.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
allber...@gmail.com
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


Re: Avoiding construction of dead dictionaries

2021-08-09 Thread Brandon Allbery
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 < sper...@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
allber...@gmail.com
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


Re: Avoiding construction of dead dictionaries

2021-08-09 Thread Tom Smeding
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 < sper...@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


Re: Avoiding construction of dead dictionaries

2021-08-09 Thread Michael Sperber

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