Re: New implementation for `ImpredicativeTypes`

[Richard Eisenberg]

> On Sep 2, 2021, at 2:56 PM, john.ericson  
> wrote:
> 
> Does the most basic e.g.
> 
> newtype Some f where
>   MkSome :: forall a. f a -> Some f
> 
> Have one of those problematic equalities?

No. That's not a GADT -- the constructor doesn't restrict anything about `f`.

I think you're after newtype existentials. I think these should indeed be 
possible, because what you propose appears to be the same as

newtype Some f = MkSome (exists a. f a)

We can probably support the syntax you wrote, too, but I don't want to commit 
to that right now.

Richard

> 
> 
>  On Thu, 02 Sep 2021 14:33:40 -0400 li...@richarde.dev wrote 
> 
> 
> 
> On Sep 2, 2021, at 2:10 PM, Alex Rozenshteyn  > wrote:
> 
> Oh, I see. That's because this would need to introduce `pack ... as ...` and 
> `open ...` into the core term language, right?
> 
> Exactly, yes.
> 
> 
> My sense is that it shouldn't negatively affect runtime performance of 
> programs without existentials even if implemented naively; does that seem 
> accurate? Not that implementing it, even naively, is a small task. 
> 
> I would agree with this, too.
> 
> On Sep 2, 2021, at 2:21 PM, john.ericson  > wrote:
> 
> This reminds me...can we do newtype GADTs in certain situations as a stepping 
> stone? I would think that would be purely easier — more nominal, no nice 
> projections but only `case` and skolems which cannot escape.
> 
> Newtype GADTs we're long deemed impossible IIRC, but surely the paper 
> demonstrates that at least some cases should work?
> 
> I don't quite see how this relates to existentials. Note that the paper does 
> not address e.g. packing equalities in existentials, which would be needed 
> for interacting with GADTs.
> 
> Glad folks are enjoying the paper! :)
> 
> Richard
> 
> 
> 
>  On Thu, 02 Sep 2021 14:10:34 -0400 rpglove...@gmail.com 
>  wrote 
> 
> Oh, I see. That's because this would need to introduce `pack ... as ...` and 
> `open ...` into the core term language, right?
> 
> My sense is that it shouldn't negatively affect runtime performance of 
> programs without existentials even if implemented naively; does that seem 
> accurate? Not that implementing it, even naively, is a small task. 
> 
> On Thu, Sep 2, 2021 at 1:44 PM Simon Peyton Jones  > wrote:
> Of course not. The same was true for QuickLook, though, wasn't it?
> 
> No, not at all.   QuickLook required zero changes to GHC’s intermediate 
> language – it impacted only the type inference system.   Adding existentials 
> will entail a substantial change to the intermediate language, affecting 
> every optimisation pass.
> 
>  
> 
> Simon
> 
>  
> 
> From: Alex Rozenshteyn mailto:rpglove...@gmail.com>> 
> Sent: 02 September 2021 18:13
> To: Simon Peyton Jones mailto:simo...@microsoft.com>>
> Cc: GHC developers mailto:ghc-devs@haskell.org>>
> Subject: Re: New implementation for `ImpredicativeTypes`
> 
>  
> 
> So it’s not just a question of saying “just add that paper to GHC and voila 
> job done”. 
> 
>  
> 
> Of course not. The same was true for QuickLook, though, wasn't it?
> 
>  
> 
> On Thu, Sep 2, 2021 at 12:42 PM Simon Peyton Jones  > wrote:
> 
> If I understand correctly, the recent ICFP paper "An Existential Crisis 
> Resolved 
> "
>  finally enables this; is that right?
> 
> It describes one way to include existentials in GHC’s intermediate language, 
> which is a real contribution. But it is not a small change.  So it’s not just 
> a question of saying “just add that paper to GHC and voila job done”.
> 
>  
> 
> Simon
> 
>  
> 
> From: Alex Rozenshteyn mailto:rpglove...@gmail.com>> 
> Sent: 02 September 2021 17:10
> To: Simon Peyton Jones mailto:simo...@microsoft.com>>
> Cc: GHC developers mailto:ghc-devs@haskell.org>>
> Subject: Re: New implementation for `ImpredicativeTypes`
> 
>  
> 
> If I understand correctly, the recent ICFP paper "An Existential Crisis 
> Resolved 
> "
>  finally enables this; is that right?
> 
>  
> 
> On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones  > wrote:
> 
> Suppose 

Re: Potential improvement in compacting GC

[Ben Gamari]

Ömer Sinan Ağacan  writes:

> Here's another improvement that fixes a very old issue in GHC's compacting GC
> [1].
>
> To summarize the problem: when untreading an object we update references to 
> the
> object that we've seen so far to the object's new location. But to get the
> object's new location we need to know the object's size, because depending on
> the size we may need to move the object to a new block (when the current block
> does not have enough space for the object).
>
> For this we currently walk the thread twice, once to get the info table (used
> to get the size), then again to update references to the object. Ideally we
> want to do just one pass when unthreading.
>
> The solution is explained in The GC Handbook, section 3.4. Instead of using 
> one
> bit to mark an object, we use two bits: one for the first word of the object,
> one for the last word. Using two bits is not a problem in GHC because heap
> objects are at least 2 words. For example, an object with two words is marked
> with `11`, 3 words is marked with `101` and so on.
>
> Now we can scan the bitmap to find object size, and unthread it without having
> to find the info table first.
>
Thanks Ömer! I have plopped all of these ideas into a ticket, #20328.
Hopefully someone will come along to implement.

Cheers,

- Ben



signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: New implementation for `ImpredicativeTypes`

[john.ericson]

Does the most basic e.g.newtype Some f where  MkSome :: forall a. f a -> Some 
fHave one of those problematic equalities?  On Thu, 02 Sep 2021 14:33:40 
-0400  li...@richarde.dev  wrote On Sep 2, 2021, at 2:10 PM, Alex 
Rozenshteyn  wrote:Oh, I see. That's because this would 
need to introduce `pack ... as ...` and `open ...` into the core term language, 
right?Exactly, yes.My sense is that it shouldn't negatively affect runtime 
performance of programs without existentials even if implemented naively; does 
that seem accurate? Not that implementing it, even naively, is a small task. I 
would agree with this, too.On Sep 2, 2021, at 2:21 PM, john.ericson 
 wrote:This reminds me...can we do newtype GADTs 
in certain situations as a stepping stone? I would think that would be purely 
easier — more nominal, no nice projections but only `case` and skolems which 
cannot escape.Newtype GADTs we're long deemed impossible IIRC, but surely the 
paper demonstrates that at least some cases should work?I don't quite see how 
this relates to existentials. Note that the paper does not address e.g. packing 
equalities in existentials, which would be needed for interacting with 
GADTs.Glad folks are enjoying the paper! :)Richard On Thu, 02 Sep 2021 
14:10:34 -0400 rpglove...@gmail.com wrote Oh, I see. That's because this 
would need to introduce `pack ... as ...` and `open ...` into the core term 
language, right?My sense is that it shouldn't negatively affect runtime 
performance of programs without existentials even if implemented naively; does 
that seem accurate? Not that implementing it, even naively, is a small task. On 
Thu, Sep 2, 2021 at 1:44 PM Simon Peyton Jones  wrote:Of 
course not. The same was true for QuickLook, though, wasn't it?No, not at all.  
 QuickLook required zero changes to GHC’s intermediate language – it impacted 
only the type inference system.   Adding existentials will entail a substantial 
change to the intermediate language, affecting every optimisation pass. Simon 
From: Alex Rozenshteyn  Sent: 02 September 2021 18:13To: 
Simon Peyton Jones Cc: GHC developers 
Subject: Re: New implementation for `ImpredicativeTypes` 
So it’s not just a question of saying “just add that paper to GHC and voila job 
done”.  Of course not. The same was true for QuickLook, though, wasn't it? On 
Thu, Sep 2, 2021 at 12:42 PM Simon Peyton Jones  
wrote:If I understand correctly, the recent ICFP paper "An Existential Crisis 
Resolved" finally enables this; is that right?It describes one way to include 
existentials in GHC’s intermediate language, which is a real contribution. But 
it is not a small change.  So it’s not just a question of saying “just add that 
paper to GHC and voila job done”. Simon From: Alex Rozenshteyn 
 Sent: 02 September 2021 17:10To: Simon Peyton Jones 
Cc: GHC developers Subject: Re: 
New implementation for `ImpredicativeTypes` If I understand correctly, the 
recent ICFP paper "An Existential Crisis Resolved" finally enables this; is 
that right? On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones 
 wrote:Suppose Haskell did have existentials; Yes, I 
think that’s an interesting thing to work on!  I’m not sure what the 
implications would be.  At very least we’d need to extend System FC (GHC’s 
intermediate language) with existential types and the corresponding pack and 
unpack syntactic forms. I don’t know of any work studying that question 
specifically, but others may have pointers. simon From: Alex Rozenshteyn 
 Sent: 06 September 2019 15:21To: Simon Peyton Jones 
Cc: Alejandro Serrano Mena ; GHC 
developers Subject: Re: New implementation for 
`ImpredicativeTypes` Hi Simon, You're exactly right, of course. My example is 
confusing, so let me see if I can clarify. What I want in the ideal is map show 
[1, 'a', "b"]. That is, minimal syntactic overhead to mapping a function over 
multiple values of distinct types that results in a homogeneous list. As the 
reddit thread points out, there are workarounds involving TH or wrapping each 
element in a constructor or using bespoke operators, but when it comes down to 
it, none of them actually allows me to say what I mean; the TH one is closest, 
but I reach for TH only in times of desperation. I had thought that one of the 
things preventing this was lack of impredicative instantiation, but now I'm not 
sure. Suppose Haskell did have existentials; would map show @(exists a. Show a 
=> a) [1, 'a', "b"] work in current Haskell and/or in quick-look? Tangentially, 
do you have a reference for what difficulties arise in adding existentials to 
Haskell? I have a feeling that it would make working with GADTs more ergonomic. 
On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones  
wrote:I’m confused.   Char does not have the type (forall a. Show a =>a), so 
our example is iill-typed in System F, never mind about type inference.  
Perhaps there’s a typo?   I think you may have ment   exists a. 
Show a => awhich doesn’t exist in 

Re: New implementation for `ImpredicativeTypes`

[Richard Eisenberg]

> On Sep 2, 2021, at 2:10 PM, Alex Rozenshteyn  wrote:
> 
> Oh, I see. That's because this would need to introduce `pack ... as ...` and 
> `open ...` into the core term language, right?

Exactly, yes.

> 
> My sense is that it shouldn't negatively affect runtime performance of 
> programs without existentials even if implemented naively; does that seem 
> accurate? Not that implementing it, even naively, is a small task. 

I would agree with this, too.

> On Sep 2, 2021, at 2:21 PM, john.ericson  
> wrote:
> 
> This reminds me...can we do newtype GADTs in certain situations as a stepping 
> stone? I would think that would be purely easier — more nominal, no nice 
> projections but only `case` and skolems which cannot escape.
> 
> Newtype GADTs we're long deemed impossible IIRC, but surely the paper 
> demonstrates that at least some cases should work?

I don't quite see how this relates to existentials. Note that the paper does 
not address e.g. packing equalities in existentials, which would be needed for 
interacting with GADTs.

Glad folks are enjoying the paper! :)

Richard

> 
> 
>  On Thu, 02 Sep 2021 14:10:34 -0400 rpglove...@gmail.com wrote 
> 
> Oh, I see. That's because this would need to introduce `pack ... as ...` and 
> `open ...` into the core term language, right?
> 
> My sense is that it shouldn't negatively affect runtime performance of 
> programs without existentials even if implemented naively; does that seem 
> accurate? Not that implementing it, even naively, is a small task. 
> 
> On Thu, Sep 2, 2021 at 1:44 PM Simon Peyton Jones  > wrote:
> Of course not. The same was true for QuickLook, though, wasn't it?
> 
> No, not at all.   QuickLook required zero changes to GHC’s intermediate 
> language – it impacted only the type inference system.   Adding existentials 
> will entail a substantial change to the intermediate language, affecting 
> every optimisation pass.
> 
>  
> 
> Simon
> 
>  
> 
> From: Alex Rozenshteyn mailto:rpglove...@gmail.com>> 
> Sent: 02 September 2021 18:13
> To: Simon Peyton Jones mailto:simo...@microsoft.com>>
> Cc: GHC developers mailto:ghc-devs@haskell.org>>
> Subject: Re: New implementation for `ImpredicativeTypes`
> 
>  
> 
> So it’s not just a question of saying “just add that paper to GHC and voila 
> job done”. 
> 
>  
> 
> Of course not. The same was true for QuickLook, though, wasn't it?
> 
>  
> 
> On Thu, Sep 2, 2021 at 12:42 PM Simon Peyton Jones  > wrote:
> 
> If I understand correctly, the recent ICFP paper "An Existential Crisis 
> Resolved 
> "
>  finally enables this; is that right?
> 
> It describes one way to include existentials in GHC’s intermediate language, 
> which is a real contribution. But it is not a small change.  So it’s not just 
> a question of saying “just add that paper to GHC and voila job done”.
> 
>  
> 
> Simon
> 
>  
> 
> From: Alex Rozenshteyn mailto:rpglove...@gmail.com>> 
> Sent: 02 September 2021 17:10
> To: Simon Peyton Jones mailto:simo...@microsoft.com>>
> Cc: GHC developers mailto:ghc-devs@haskell.org>>
> Subject: Re: New implementation for `ImpredicativeTypes`
> 
>  
> 
> If I understand correctly, the recent ICFP paper "An Existential Crisis 
> Resolved 
> "
>  finally enables this; is that right?
> 
>  
> 
> On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones  > wrote:
> 
> Suppose Haskell did have existentials;
> 
>  
> 
> Yes, I think that’s an interesting thing to work on!  I’m not sure what the 
> implications would be.  At very least we’d need to extend System FC (GHC’s 
> intermediate language) with existential types and the corresponding pack and 
> unpack syntactic forms.
> 
>  
> 
> I don’t know of any work studying that question specifically, but others may 
> have pointers.
> 
>  
> 
> simon
> 
>  
> 
> From: Alex Rozenshteyn mailto:rpglove...@gmail.com>> 
> Sent: 06 September 2019 15:21
> To: Simon Peyton Jones mailto:simo...@microsoft.com>>
> Cc: Alejandro Serrano Mena mailto:trup...@gmail.com>>; 
> GHC developers mailto:ghc-devs@haskell.org>>
> Subject: Re: New implementation for `ImpredicativeTypes`
> 
>  
> 
> Hi Simon,
> 
>  
> 
> 

Re: New implementation for `ImpredicativeTypes`

[john.ericson]

This reminds me...can we do newtype GADTs in certain situations as a stepping 
stone? I would think that would be purely easier — more nominal, no nice 
projections but only `case` and skolems which cannot escape.Newtype GADTs we're 
long deemed impossible IIRC, but surely the paper demonstrates that at least 
some cases should work?  On Thu, 02 Sep 2021 14:10:34 -0400  
rpglove...@gmail.com  wrote Oh, I see. That's because this would need to 
introduce `pack ... as ...` and `open ...` into the core term language, 
right?My sense is that it shouldn't negatively affect runtime performance of 
programs without existentials even if implemented naively; does that seem 
accurate? Not that implementing it, even naively, is a small task. On Thu, Sep 
2, 2021 at 1:44 PM Simon Peyton Jones  wrote:








Of course not. The same was true for QuickLook, though, wasn't it?
No, not at all.   QuickLook required zero changes to GHC’s intermediate 
language – it impacted only the type inference system.   Adding existentials 
will entail a substantial change to the intermediate
 language, affecting every optimisation pass.
 
Simon
 



From: Alex Rozenshteyn 

Sent: 02 September 2021 18:13
To: Simon Peyton Jones 
Cc: GHC developers 
Subject: Re: New implementation for `ImpredicativeTypes`


 



So it’s not just a question of saying “just add that paper to GHC and voila job 
done”. 



 



Of course not. The same was true for QuickLook, though, wasn't it?



 



On Thu, Sep 2, 2021 at 12:42 PM Simon Peyton Jones  
wrote:





If I understand correctly, the recent ICFP paper "An
 Existential Crisis Resolved" finally enables this; is that right?
It describes one way to include existentials in GHC’s intermediate language, 
which is a real contribution.
But it is not a small change.  So it’s not just a question of saying “just add 
that paper to GHC and voila job done”.
 
Simon
 



From: Alex Rozenshteyn 

Sent: 02 September 2021 17:10
To: Simon Peyton Jones 
Cc: GHC developers 
Subject: Re: New implementation for `ImpredicativeTypes`


 

If I understand correctly, the recent ICFP paper "An
 Existential Crisis Resolved" finally enables this; is that right?

 


On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones  
wrote:





Suppose Haskell did have existentials;
 
Yes, I think that’s an interesting thing to work on!  I’m not sure what the 
implications would be.  At very least we’d need to extend System FC (GHC’s 
intermediate language) with
 existential types and the corresponding pack and unpack syntactic forms.
 
I don’t know of any work studying that question specifically, but others may 
have pointers.
 
simon
 



From: Alex Rozenshteyn 

Sent: 06 September 2019 15:21
To: Simon Peyton Jones 
Cc: Alejandro Serrano Mena ; GHC developers 

Subject: Re: New implementation for `ImpredicativeTypes`


 


Hi Simon,


 


You're exactly right, of course. My example is confusing, so let me see if I 
can clarify.


 


What I want in the ideal is
map show [1, 'a', "b"]. That is, minimal syntactic overhead to mapping a 
function over multiple values of distinct types that results in a homogeneous 
list. As the reddit thread points out, there are workarounds
 involving TH or wrapping each element in a constructor or using bespoke 
operators, but when it comes down to it, none of them actually allows me to say 
what I
mean; the TH one is closest, but I reach for TH only in times of desperation.


 


I had thought that one of the things preventing this was lack of impredicative 
instantiation, but now I'm not sure. Suppose Haskell
did have existentials; would map show @(exists a. Show a => a) [1, 'a', "b"] 
work in current Haskell and/or in quick-look?


 


Tangentially, do you have a reference for what difficulties arise in adding 
existentials to Haskell? I have a feeling that it would make working with GADTs 
more ergonomic.


 


On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones  
wrote:




I’m confused.   Char does not have the type (forall a. Show a =>a), so our 
example is iill-typed in System F, never mind about type inference.  Perhaps 
there’s a typo?   I think
 you may have ment
   exists a. Show a => a
which doesn’t exist in Haskell.  You can write existentials with a data type
 
data Showable where
   S :: forall a. Show a => a -> Showable
 
Then
   map show [S 1, S ‘a’, S “b”]
works fine today (without our new stuff), provided you say
 
   instance Show Showable where
     show (S x) = show x
 
Our new system can only type programs that can be written in System F.   (The 
tricky bit is inferring the impredicative instantiations.)
 
Simon
 



From: ghc-devs 
On Behalf Of Alex Rozenshteyn
Sent: 06 September 2019 03:31
To: Alejandro Serrano Mena 
Cc: GHC developers 
Subject: Re: New implementation for `ImpredicativeTypes`


 


I didn't say anything when you were requesting use cases, so I have no right to 
complain, but I'm still a little disappointed that 

Re: New implementation for `ImpredicativeTypes`

[Alex Rozenshteyn]

Oh, I see. That's because this would need to introduce `pack ... as ...`
and `open ...` into the core term language, right?

My sense is that it shouldn't negatively affect runtime performance of
programs without existentials even if implemented naively; does that seem
accurate? Not that implementing it, even naively, is a small task.

On Thu, Sep 2, 2021 at 1:44 PM Simon Peyton Jones 
wrote:

> Of course not. The same was true for QuickLook, though, wasn't it?
>
> No, not at all.   QuickLook required zero changes to GHC’s intermediate
> language – it impacted only the type inference system.   Adding
> existentials will entail a substantial change to the intermediate language,
> affecting every optimisation pass.
>
>
>
> Simon
>
>
>
> *From:* Alex Rozenshteyn 
> *Sent:* 02 September 2021 18:13
> *To:* Simon Peyton Jones 
> *Cc:* GHC developers 
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> So it’s not just a question of saying “just add that paper to GHC and
> voila job done”.
>
>
>
> Of course not. The same was true for QuickLook, though, wasn't it?
>
>
>
> On Thu, Sep 2, 2021 at 12:42 PM Simon Peyton Jones 
> wrote:
>
> If I understand correctly, the recent ICFP paper "An Existential Crisis
> Resolved
> "
> finally enables this; is that right?
>
> It describes one way to include existentials in GHC’s intermediate
> language, which is a real contribution. *But it is not a small change*.
> So it’s not just a question of saying “just add that paper to GHC and voila
> job done”.
>
>
>
> Simon
>
>
>
> *From:* Alex Rozenshteyn 
> *Sent:* 02 September 2021 17:10
> *To:* Simon Peyton Jones 
> *Cc:* GHC developers 
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> If I understand correctly, the recent ICFP paper "An Existential Crisis
> Resolved
> "
> finally enables this; is that right?
>
>
>
> On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones 
> wrote:
>
> Suppose Haskell *did* have existentials;
>
>
>
> Yes, I think that’s an interesting thing to work on!  I’m not sure what
> the implications would be.  At very least we’d need to extend System FC
> (GHC’s intermediate language) with existential types and the corresponding
> pack and unpack syntactic forms.
>
>
>
> I don’t know of any work studying that question specifically, but others
> may have pointers.
>
>
>
> simon
>
>
>
> *From:* Alex Rozenshteyn 
> *Sent:* 06 September 2019 15:21
> *To:* Simon Peyton Jones 
> *Cc:* Alejandro Serrano Mena ; GHC developers <
> ghc-devs@haskell.org>
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> Hi Simon,
>
>
>
> You're exactly right, of course. My example is confusing, so let me see if
> I can clarify.
>
>
>
> What I want in the ideal is map show [1, 'a', "b"]. That is, minimal
> syntactic overhead to mapping a function over multiple values of distinct
> types that results in a homogeneous list. As the reddit thread points out,
> there are workarounds involving TH or wrapping each element in a
> constructor or using bespoke operators, but when it comes down to it, none
> of them actually allows me to say what I *mean*; the TH one is closest,
> but I reach for TH only in times of desperation.
>
>
>
> I had thought that one of the things preventing this was lack of
> impredicative instantiation, but now I'm not sure. Suppose Haskell *did*
> have existentials; would map show @(exists a. Show a => a) [1, 'a', "b"]
> work in current Haskell and/or in quick-look?
>
>
>
> Tangentially, do you have a reference for what difficulties arise in
> adding existentials to Haskell? I have a feeling that it would make working
> with GADTs more ergonomic.
>
>
>
> On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones 
> wrote:
>
> I’m confused.   Char does not have the type (forall a. Show a =>a), so our
> example is iill-typed in System F, never mind about type inference.
> Perhaps there’s a typo?   I think you may have ment
>
>exists a. Show a => a
>
> which doesn’t exist in Haskell.  You can write existentials with a data
> type
>
>
>
> data Showable where
>
>S :: forall a. Show a => a -> Showable
>
>
>
> Then
>
>map show [S 1, S ‘a’, S “b”]
>
> works fine today (without 

Re: Potential improvement in compacting GC

[Sebastian Graf]

Hey Ömer,

Just in case you are wondering whether you are talking into the void: you 
aren't! Keep the good suggestions coming, someone will eventually be able to 
get around to implementing them!
Thanks for your write-ups.

Cheers,
Sebastian

Von: ghc-devs  im Auftrag von Ömer Sinan Ağacan 

Gesendet: Thursday, September 2, 2021 5:47:08 PM
An: ghc-devs 
Betreff: Re: Potential improvement in compacting GC

Here's another improvement that fixes a very old issue in GHC's compacting GC
[1].

To summarize the problem: when untreading an object we update references to the
object that we've seen so far to the object's new location. But to get the
object's new location we need to know the object's size, because depending on
the size we may need to move the object to a new block (when the current block
does not have enough space for the object).

For this we currently walk the thread twice, once to get the info table (used
to get the size), then again to update references to the object. Ideally we
want to do just one pass when unthreading.

The solution is explained in The GC Handbook, section 3.4. Instead of using one
bit to mark an object, we use two bits: one for the first word of the object,
one for the last word. Using two bits is not a problem in GHC because heap
objects are at least 2 words. For example, an object with two words is marked
with `11`, 3 words is marked with `101` and so on.

Now we can scan the bitmap to find object size, and unthread it without having
to find the info table first.

Ömer

[1]: 
https://github.com/ghc/ghc/blob/922c6bc8dd8d089cfe4b90ec2120cb48959ba2b5/rts/sm/Compact.c#L844-L848

Ömer Sinan Ağacan , 14 Tem 2021 Çar, 09:27
tarihinde şunu yazdı:
>
> Two other ideas that should improve GHC's compacting GC much more
> significantly. I've implemented both of these in another project and the
> results were great. In a GC benchmark (mutator does almost no work other than
> allocating data using a bump allocator), first one reduced Wasm instructions
> executed by 14%, second one 19.8%.
>
> Both of these ideas require pushing object headers to the mark stack with the
> objects, which means larger mark stacks. This is the only downside of these
> algorithms.
>
> - Instead of marking and then threading in the next pass, mark phase threads
>   all fields when pushing the fields to the mark stack. We still need two 
> other
>   passes: one to unthread headers, another to move the objects. (we can't do
>   both in one pass, let me know if you're curious and I can elaborate)
>
>   This has the same number of passes as the current implementation, but it 
> only
>   visits object fields once. Currently, we visit fields once when marking, to
>   mark fields, then again in `update_fwd`. This implementation does both in 
> one
>   pass over the fields. `update_fwd` does not visit fields.
>
>   This reduced Wasm instructions executed by 14% in my benchmark.
>
> - Marking phase threads backwards pointers (ignores forwards pointers). Then 
> we
>   do one pass instead of two: for a marked object, unthread it (update
>   forwards pointers to the object's new location), move it to its new 
> location,
>   then thread its forwards pointers. This completely eliminates one of the 3
>   passes, but fields need to be visited twice as before (unlike the algorithm
>   above).
>
>   I think this one is originally described in "An Efficient Garbage Compaction
>   Algorithm", but I found that paper to be difficult to follow. A short
>   description of the same algorithm exists in "High-Performance Garbage
>   Collection for Memory-Constrained Environments" in section 5.1.2.
>
>   This reduced Wasm instructions executed by 19.8% in my benchmark.
>
>   In this algorithm, fields that won't be moved can be threaded any time 
> before
>   the second pass (pointed objects need to be marked and pushed to the mark
>   stack with headers before threading a field). For example, in GHC, mut list
>   entries can be threaded before or after marking (but before the second pass)
>   as IIRC mut lists are not moved. Same for fields of large objects.
>
> As far as I can see, mark-compact GC is still the default when max heap size 
> is
> specified and the oldest generation size is (by default) more than 30% of the
> max heap size. I'm not sure if max heap size is specified often (it's off by
> default), so not sure what would be the impact of these improvements be, but 
> if
> anyone would be interested in funding me to implement these ideas (second
> algorithm above, and the bitmap iteration in the previous email) I could try 
> to
> allocate one or two days a week to finish in a few months.
>
> Normally these are simple changes, but it's difficult to test and debug GHC's
> RTS as we don't have a test suite readily available and the code is not easily
> testable. In my previous implementations of these algorithms I had unit tests
> for the GC where I could easily generate arbitrary graphs (with 

RE: New implementation for `ImpredicativeTypes`

[Simon Peyton Jones via ghc-devs]

Of course not. The same was true for QuickLook, though, wasn't it?
No, not at all.   QuickLook required zero changes to GHC's intermediate 
language - it impacted only the type inference system.   Adding existentials 
will entail a substantial change to the intermediate language, affecting every 
optimisation pass.

Simon

From: Alex Rozenshteyn 
Sent: 02 September 2021 18:13
To: Simon Peyton Jones 
Cc: GHC developers 
Subject: Re: New implementation for `ImpredicativeTypes`

So it's not just a question of saying "just add that paper to GHC and voila job 
done".

Of course not. The same was true for QuickLook, though, wasn't it?

On Thu, Sep 2, 2021 at 12:42 PM Simon Peyton Jones 
mailto:simo...@microsoft.com>> wrote:
If I understand correctly, the recent ICFP paper "An Existential Crisis 
Resolved"
 finally enables this; is that right?
It describes one way to include existentials in GHC's intermediate language, 
which is a real contribution. But it is not a small change.  So it's not just a 
question of saying "just add that paper to GHC and voila job done".

Simon

From: Alex Rozenshteyn mailto:rpglove...@gmail.com>>
Sent: 02 September 2021 17:10
To: Simon Peyton Jones mailto:simo...@microsoft.com>>
Cc: GHC developers mailto:ghc-devs@haskell.org>>
Subject: Re: New implementation for `ImpredicativeTypes`

If I understand correctly, the recent ICFP paper "An Existential Crisis 
Resolved"
 finally enables this; is that right?

On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones 
mailto:simo...@microsoft.com>> wrote:
Suppose Haskell did have existentials;

Yes, I think that's an interesting thing to work on!  I'm not sure what the 
implications would be.  At very least we'd need to extend System FC (GHC's 
intermediate language) with existential types and the corresponding pack and 
unpack syntactic forms.

I don't know of any work studying that question specifically, but others may 
have pointers.

simon

From: Alex Rozenshteyn mailto:rpglove...@gmail.com>>
Sent: 06 September 2019 15:21
To: Simon Peyton Jones mailto:simo...@microsoft.com>>
Cc: Alejandro Serrano Mena mailto:trup...@gmail.com>>; GHC 
developers mailto:ghc-devs@haskell.org>>
Subject: Re: New implementation for `ImpredicativeTypes`

Hi Simon,

You're exactly right, of course. My example is confusing, so let me see if I 
can clarify.

What I want in the ideal is map show [1, 'a', "b"]. That is, minimal syntactic 
overhead to mapping a function over multiple values of distinct types that 
results in a homogeneous list. As the reddit thread points out, there are 
workarounds involving TH or wrapping each element in a constructor or using 
bespoke operators, but when it comes down to it, none of them actually allows 
me to say what I mean; the TH one is closest, but I reach for TH only in times 
of desperation.

I had thought that one of the things preventing this was lack of impredicative 
instantiation, but now I'm not sure. Suppose Haskell did have existentials; 
would map show @(exists a. Show a => a) [1, 'a', "b"] work in current Haskell 
and/or in quick-look?

Tangentially, do you have a reference for what difficulties arise in adding 
existentials to Haskell? I have a feeling that it would make working with GADTs 
more ergonomic.

On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones 
mailto:simo...@microsoft.com>> wrote:
I'm confused.   Char does not have the type (forall a. Show a =>a), so our 
example is iill-typed in System F, never mind about type inference.  Perhaps 
there's a typo?   I think you may have ment
   exists a. Show a => a
which doesn't exist in Haskell.  You can write existentials with a data type

data Showable where
   S :: forall a. Show a => a -> Showable

Then
   map show [S 1, S 'a', S "b"]
works fine today (without our new stuff), provided you say

   instance Show Showable where
 show (S x) = show x

Our new system can only type programs that can be written in System F.   (The 
tricky bit is inferring the impredicative instantiations.)

Simon

From: ghc-devs 
mailto:ghc-devs-boun...@haskell.org>> On Behalf 
Of Alex Rozenshteyn
Sent: 06 September 2019 03:31
To: Alejandro Serrano Mena 

Re: New implementation for `ImpredicativeTypes`

[Alex Rozenshteyn]

>
> So it’s not just a question of saying “just add that paper to GHC and
> voila job done”.


Of course not. The same was true for QuickLook, though, wasn't it?

On Thu, Sep 2, 2021 at 12:42 PM Simon Peyton Jones 
wrote:

> If I understand correctly, the recent ICFP paper "An Existential Crisis
> Resolved
> "
> finally enables this; is that right?
>
> It describes one way to include existentials in GHC’s intermediate
> language, which is a real contribution. *But it is not a small change*.
> So it’s not just a question of saying “just add that paper to GHC and voila
> job done”.
>
>
>
> Simon
>
>
>
> *From:* Alex Rozenshteyn 
> *Sent:* 02 September 2021 17:10
> *To:* Simon Peyton Jones 
> *Cc:* GHC developers 
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> If I understand correctly, the recent ICFP paper "An Existential Crisis
> Resolved
> "
> finally enables this; is that right?
>
>
>
> On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones 
> wrote:
>
> Suppose Haskell *did* have existentials;
>
>
>
> Yes, I think that’s an interesting thing to work on!  I’m not sure what
> the implications would be.  At very least we’d need to extend System FC
> (GHC’s intermediate language) with existential types and the corresponding
> pack and unpack syntactic forms.
>
>
>
> I don’t know of any work studying that question specifically, but others
> may have pointers.
>
>
>
> simon
>
>
>
> *From:* Alex Rozenshteyn 
> *Sent:* 06 September 2019 15:21
> *To:* Simon Peyton Jones 
> *Cc:* Alejandro Serrano Mena ; GHC developers <
> ghc-devs@haskell.org>
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> Hi Simon,
>
>
>
> You're exactly right, of course. My example is confusing, so let me see if
> I can clarify.
>
>
>
> What I want in the ideal is map show [1, 'a', "b"]. That is, minimal
> syntactic overhead to mapping a function over multiple values of distinct
> types that results in a homogeneous list. As the reddit thread points out,
> there are workarounds involving TH or wrapping each element in a
> constructor or using bespoke operators, but when it comes down to it, none
> of them actually allows me to say what I *mean*; the TH one is closest,
> but I reach for TH only in times of desperation.
>
>
>
> I had thought that one of the things preventing this was lack of
> impredicative instantiation, but now I'm not sure. Suppose Haskell *did*
> have existentials; would map show @(exists a. Show a => a) [1, 'a', "b"]
> work in current Haskell and/or in quick-look?
>
>
>
> Tangentially, do you have a reference for what difficulties arise in
> adding existentials to Haskell? I have a feeling that it would make working
> with GADTs more ergonomic.
>
>
>
> On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones 
> wrote:
>
> I’m confused.   Char does not have the type (forall a. Show a =>a), so our
> example is iill-typed in System F, never mind about type inference.
> Perhaps there’s a typo?   I think you may have ment
>
>exists a. Show a => a
>
> which doesn’t exist in Haskell.  You can write existentials with a data
> type
>
>
>
> data Showable where
>
>S :: forall a. Show a => a -> Showable
>
>
>
> Then
>
>map show [S 1, S ‘a’, S “b”]
>
> works fine today (without our new stuff), provided you say
>
>
>
>instance Show Showable where
>
>  show (S x) = show x
>
>
>
> Our new system can only type programs that can be written in System F.
> (The tricky bit is inferring the impredicative instantiations.)
>
>
>
> Simon
>
>
>
> *From:* ghc-devs  *On Behalf Of *Alex
> Rozenshteyn
> *Sent:* 06 September 2019 03:31
> *To:* Alejandro Serrano Mena 
> *Cc:* GHC developers 
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> I didn't say anything when you were requesting use cases, so I have no
> right to complain, but I'm still a little disappointed that this doesn't
> fix my (admittedly very minor) issue:
> https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8=9
> 

RE: New implementation for `ImpredicativeTypes`

[Simon Peyton Jones via ghc-devs]

If I understand correctly, the recent ICFP paper "An Existential Crisis 
Resolved"
 finally enables this; is that right?
It describes one way to include existentials in GHC's intermediate language, 
which is a real contribution. But it is not a small change.  So it's not just a 
question of saying "just add that paper to GHC and voila job done".

Simon

From: Alex Rozenshteyn 
Sent: 02 September 2021 17:10
To: Simon Peyton Jones 
Cc: GHC developers 
Subject: Re: New implementation for `ImpredicativeTypes`

If I understand correctly, the recent ICFP paper "An Existential Crisis 
Resolved"
 finally enables this; is that right?

On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones 
mailto:simo...@microsoft.com>> wrote:
Suppose Haskell did have existentials;

Yes, I think that's an interesting thing to work on!  I'm not sure what the 
implications would be.  At very least we'd need to extend System FC (GHC's 
intermediate language) with existential types and the corresponding pack and 
unpack syntactic forms.

I don't know of any work studying that question specifically, but others may 
have pointers.

simon

From: Alex Rozenshteyn mailto:rpglove...@gmail.com>>
Sent: 06 September 2019 15:21
To: Simon Peyton Jones mailto:simo...@microsoft.com>>
Cc: Alejandro Serrano Mena mailto:trup...@gmail.com>>; GHC 
developers mailto:ghc-devs@haskell.org>>
Subject: Re: New implementation for `ImpredicativeTypes`

Hi Simon,

You're exactly right, of course. My example is confusing, so let me see if I 
can clarify.

What I want in the ideal is map show [1, 'a', "b"]. That is, minimal syntactic 
overhead to mapping a function over multiple values of distinct types that 
results in a homogeneous list. As the reddit thread points out, there are 
workarounds involving TH or wrapping each element in a constructor or using 
bespoke operators, but when it comes down to it, none of them actually allows 
me to say what I mean; the TH one is closest, but I reach for TH only in times 
of desperation.

I had thought that one of the things preventing this was lack of impredicative 
instantiation, but now I'm not sure. Suppose Haskell did have existentials; 
would map show @(exists a. Show a => a) [1, 'a', "b"] work in current Haskell 
and/or in quick-look?

Tangentially, do you have a reference for what difficulties arise in adding 
existentials to Haskell? I have a feeling that it would make working with GADTs 
more ergonomic.

On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones 
mailto:simo...@microsoft.com>> wrote:
I'm confused.   Char does not have the type (forall a. Show a =>a), so our 
example is iill-typed in System F, never mind about type inference.  Perhaps 
there's a typo?   I think you may have ment
   exists a. Show a => a
which doesn't exist in Haskell.  You can write existentials with a data type

data Showable where
   S :: forall a. Show a => a -> Showable

Then
   map show [S 1, S 'a', S "b"]
works fine today (without our new stuff), provided you say

   instance Show Showable where
 show (S x) = show x

Our new system can only type programs that can be written in System F.   (The 
tricky bit is inferring the impredicative instantiations.)

Simon

From: ghc-devs 
mailto:ghc-devs-boun...@haskell.org>> On Behalf 
Of Alex Rozenshteyn
Sent: 06 September 2019 03:31
To: Alejandro Serrano Mena mailto:trup...@gmail.com>>
Cc: GHC developers mailto:ghc-devs@haskell.org>>
Subject: Re: New implementation for `ImpredicativeTypes`

I didn't say anything when you were requesting use cases, so I have no right to 
complain, but I'm still a little disappointed that this doesn't fix my 
(admittedly very minor) issue: 

Re: New implementation for `ImpredicativeTypes`

[Alex Rozenshteyn]

If I understand correctly, the recent ICFP paper "An Existential Crisis
Resolved " finally enables
this; is that right?

On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones 
wrote:

> Suppose Haskell *did* have existentials;
>
>
>
> Yes, I think that’s an interesting thing to work on!  I’m not sure what
> the implications would be.  At very least we’d need to extend System FC
> (GHC’s intermediate language) with existential types and the corresponding
> pack and unpack syntactic forms.
>
>
>
> I don’t know of any work studying that question specifically, but others
> may have pointers.
>
>
>
> simon
>
>
>
> *From:* Alex Rozenshteyn 
> *Sent:* 06 September 2019 15:21
> *To:* Simon Peyton Jones 
> *Cc:* Alejandro Serrano Mena ; GHC developers <
> ghc-devs@haskell.org>
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> Hi Simon,
>
>
>
> You're exactly right, of course. My example is confusing, so let me see if
> I can clarify.
>
>
>
> What I want in the ideal is map show [1, 'a', "b"]. That is, minimal
> syntactic overhead to mapping a function over multiple values of distinct
> types that results in a homogeneous list. As the reddit thread points out,
> there are workarounds involving TH or wrapping each element in a
> constructor or using bespoke operators, but when it comes down to it, none
> of them actually allows me to say what I *mean*; the TH one is closest,
> but I reach for TH only in times of desperation.
>
>
>
> I had thought that one of the things preventing this was lack of
> impredicative instantiation, but now I'm not sure. Suppose Haskell *did*
> have existentials; would map show @(exists a. Show a => a) [1, 'a', "b"]
> work in current Haskell and/or in quick-look?
>
>
>
> Tangentially, do you have a reference for what difficulties arise in
> adding existentials to Haskell? I have a feeling that it would make working
> with GADTs more ergonomic.
>
>
>
> On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones 
> wrote:
>
> I’m confused.   Char does not have the type (forall a. Show a =>a), so our
> example is iill-typed in System F, never mind about type inference.
> Perhaps there’s a typo?   I think you may have ment
>
>exists a. Show a => a
>
> which doesn’t exist in Haskell.  You can write existentials with a data
> type
>
>
>
> data Showable where
>
>S :: forall a. Show a => a -> Showable
>
>
>
> Then
>
>map show [S 1, S ‘a’, S “b”]
>
> works fine today (without our new stuff), provided you say
>
>
>
>instance Show Showable where
>
>  show (S x) = show x
>
>
>
> Our new system can only type programs that can be written in System F.
> (The tricky bit is inferring the impredicative instantiations.)
>
>
>
> Simon
>
>
>
> *From:* ghc-devs  *On Behalf Of *Alex
> Rozenshteyn
> *Sent:* 06 September 2019 03:31
> *To:* Alejandro Serrano Mena 
> *Cc:* GHC developers 
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> I didn't say anything when you were requesting use cases, so I have no
> right to complain, but I'm still a little disappointed that this doesn't
> fix my (admittedly very minor) issue:
> https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8=9
> 
>
>
>
> For those who don't want to click on the reddit link: I would like to be
> able to write something like map show ([1, 'a', "b"] :: [forall a. Show a
> => a]), and have it work.
>
>
>
> On Wed, Sep 4, 2019 at 8:13 AM Alejandro Serrano Mena 
> wrote:
>
> Hi all,
>
> As I mentioned some time ago, we have been busy working on a new
> implementation of `ImpredicativeTypes` for GHC. I am very thankful to
> everybody who back then sent us examples of impredicativity which would be
> nice to support, as far as we know this branch supports all of them! :)
>
>
>
> If you want to try it, at
> https://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8062a4cc0a5/pipelines?ref=quick-look-build
> 
> you can find the result of the pipeline, which includes builds for several
> platforms (click on the "Artifacts" button, the one which looks like a
> cloud, to get them). The code is being 

Re: Potential improvement in compacting GC

[Ömer Sinan Ağacan]

Here's another improvement that fixes a very old issue in GHC's compacting GC
[1].

To summarize the problem: when untreading an object we update references to the
object that we've seen so far to the object's new location. But to get the
object's new location we need to know the object's size, because depending on
the size we may need to move the object to a new block (when the current block
does not have enough space for the object).

For this we currently walk the thread twice, once to get the info table (used
to get the size), then again to update references to the object. Ideally we
want to do just one pass when unthreading.

The solution is explained in The GC Handbook, section 3.4. Instead of using one
bit to mark an object, we use two bits: one for the first word of the object,
one for the last word. Using two bits is not a problem in GHC because heap
objects are at least 2 words. For example, an object with two words is marked
with `11`, 3 words is marked with `101` and so on.

Now we can scan the bitmap to find object size, and unthread it without having
to find the info table first.

Ömer

[1]: 
https://github.com/ghc/ghc/blob/922c6bc8dd8d089cfe4b90ec2120cb48959ba2b5/rts/sm/Compact.c#L844-L848

Ömer Sinan Ağacan , 14 Tem 2021 Çar, 09:27
tarihinde şunu yazdı:
>
> Two other ideas that should improve GHC's compacting GC much more
> significantly. I've implemented both of these in another project and the
> results were great. In a GC benchmark (mutator does almost no work other than
> allocating data using a bump allocator), first one reduced Wasm instructions
> executed by 14%, second one 19.8%.
>
> Both of these ideas require pushing object headers to the mark stack with the
> objects, which means larger mark stacks. This is the only downside of these
> algorithms.
>
> - Instead of marking and then threading in the next pass, mark phase threads
>   all fields when pushing the fields to the mark stack. We still need two 
> other
>   passes: one to unthread headers, another to move the objects. (we can't do
>   both in one pass, let me know if you're curious and I can elaborate)
>
>   This has the same number of passes as the current implementation, but it 
> only
>   visits object fields once. Currently, we visit fields once when marking, to
>   mark fields, then again in `update_fwd`. This implementation does both in 
> one
>   pass over the fields. `update_fwd` does not visit fields.
>
>   This reduced Wasm instructions executed by 14% in my benchmark.
>
> - Marking phase threads backwards pointers (ignores forwards pointers). Then 
> we
>   do one pass instead of two: for a marked object, unthread it (update
>   forwards pointers to the object's new location), move it to its new 
> location,
>   then thread its forwards pointers. This completely eliminates one of the 3
>   passes, but fields need to be visited twice as before (unlike the algorithm
>   above).
>
>   I think this one is originally described in "An Efficient Garbage Compaction
>   Algorithm", but I found that paper to be difficult to follow. A short
>   description of the same algorithm exists in "High-Performance Garbage
>   Collection for Memory-Constrained Environments" in section 5.1.2.
>
>   This reduced Wasm instructions executed by 19.8% in my benchmark.
>
>   In this algorithm, fields that won't be moved can be threaded any time 
> before
>   the second pass (pointed objects need to be marked and pushed to the mark
>   stack with headers before threading a field). For example, in GHC, mut list
>   entries can be threaded before or after marking (but before the second pass)
>   as IIRC mut lists are not moved. Same for fields of large objects.
>
> As far as I can see, mark-compact GC is still the default when max heap size 
> is
> specified and the oldest generation size is (by default) more than 30% of the
> max heap size. I'm not sure if max heap size is specified often (it's off by
> default), so not sure what would be the impact of these improvements be, but 
> if
> anyone would be interested in funding me to implement these ideas (second
> algorithm above, and the bitmap iteration in the previous email) I could try 
> to
> allocate one or two days a week to finish in a few months.
>
> Normally these are simple changes, but it's difficult to test and debug GHC's
> RTS as we don't have a test suite readily available and the code is not easily
> testable. In my previous implementations of these algorithms I had unit tests
> for the GC where I could easily generate arbitrary graphs (with cycles,
> backwards ptrs, forwards ptrs, ptrs from/to roots etc.) and test GC in
> isolation. Implementation of (2) took less than a day, and I didn't have to
> debug it more once the tests passed. It's really unfortunate that GHC's RTS
> makes this kind of thing difficult..
>
> Ömer
>
> Ömer Sinan Ağacan , 7 Oca 2021 Per, 20:42
> tarihinde şunu yazdı:
> >
> > Hello,
> >
> > I recently implemented the algorithm used by GHC's compacting GC