New implementation for `ImpredicativeTypes`

[John Ericson]

On 9/7/21 8:41 PM, Richard Eisenberg wrote:
>
>
>> On Sep 6, 2021, at 11:21 AM, John Ericson 
>> <john.ericson at obsidian.systems 
>> <mailto:john.ericson at obsidian.systems>> wrote:
>>
>> On 9/2/21 11:04 PM, Richard Eisenberg wrote:
>>
>>> On Sep 2, 2021, at 2:56 PM, john.ericson 
>>> <john.ericson at obsidian.systems 
>>> <mailto:john.ericson at obsidian.systems>> 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`.
>>
>> Morally, sure, but GHC doesn't know about this.
>>
>
> Sure it does -- GHC doesn't include an equality constraint as one of 
> the fields of MkSome. This isn't about extensions -- it's about the 
> way the data constructor is interpreted.

Oops, agreed. I guess meant extensions didn't seem to check for this in 
a really syntax-driven way. But yes deciding the cases apart is not hard 
once the data definition is compiled.

>>>
>>> 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.
>>
>> The syntax I wrote is already basically valid?
>>
>> data Some f = forall a. Some (f a)
>> data Some f where MkSome :: forall a f. f a -> Some f
>>
>> Is accepted
>>
>> newtype Some f = forall a. Some (f a)
>> newtype Some f where MkSome :: forall a f. f a -> Some f
>>
>> Is not with "A newtype constructor cannot have existential type 
>> variables"
>>
>> I propose we teach GHC how these "GADTs" in fact merely have 
>> existential variables, and not the FC constraints that require the 
>> extra evaluation for soundness. Than we can get the 
>> operational/runtime benefits of what you propose for cheap. Don't get 
>> me wrong -- the other aspects in the paper this doesn't address are 
>> still quite valuable, but I think this is a useful stepping stone / 
>> removal of artificial restrictions we should do first.
>>
>> This sort of thing is brought up in #1965, where it is alleged this 
>> is in fact more difficult than it sounds. All more reason it is a 
>> good stepping stone, I say!
>>
>
> This is more difficult than it sounds. :) Newtypes are implemented via 
> coercions in Core, and coercions are inherently bidirectional. The 
> appearance of an existential in this way requires one-way conversions, 
> which are currently not supported. So, to get what you want, we'd have 
> to modify the core language as in the existentials paper, along with 
> some extra work to automatically add `pack` and `open` -- rather 
> similar to the type inference described in the existentials paper. The 
> bottom line for me is that this seems just as hard as implementing the 
> whole thing, so I see no value in having the stepping stone. If we 
> always wrote out the newtype constructor, then maybe we could use its 
> appearance to guide the `pack` and `open` but we don't: sometimes, we 
> just use `coerce`. So I really don't think this is any easier than 
> implementing the paper as written. Once that's done, we can come back 
> and add this new feature relatively easily (I think).
Makes sense. That route is indeed harder than I was thinking.

There was a time before coercions when I gather newtypes were mostly 
implemented with a special-case lowering to STG. I imagine it would be 
quite easy to implement this that way, but that door is now mostly shut.

I had a few more thoughts, but I am not sure if I should trouble the 
list with them as they are still a bit rough around the edges. Suffice 
to say, I hope we could sort of "smooth out" the feature space a bit so 
that these and GADTs are not completely different, e.g. I think all 
existential variables can be projected like this (I opened #20337 for 
this), and perhaps connect GADTs to the existentials with evidence you 
mention in the "future work" section, so "true" GADTs also have 
structural counterparts in a similar way.

Happy to just continue mulling on it until a proposal or something, 
however. :)

John

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210908/44be3355/attachment.html>