Re: New implementation for `ImpredicativeTypes`

> 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

Re: Potential improvement in compacting GC

Ö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

Re: New implementation for `ImpredicativeTypes`

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

Re: New implementation for `ImpredicativeTypes`

> 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

Re: New implementation for `ImpredicativeTypes`

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

Re: New implementation for `ImpredicativeTypes`

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

Re: Potential improvement in compacting GC

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

RE: New implementation for `ImpredicativeTypes`

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

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 >

RE: New implementation for `ImpredicativeTypes`

If I understand correctly, the recent ICFP paper "An Existential Crisis

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

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,