On 9/7/21 8:41 PM, Richard Eisenberg wrote:
On Sep 6, 2021, at 11:21 AM, John Ericson
<john.ericson@obsidian.systems
<mailto:john.ericson@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@obsidian.systems
<mailto:john.ericson@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
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
