New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Unboxed coercions #116
Unboxed coercions #116
Conversation
26ab598
to
ebc7139
Compare
Offer access to unboxed coercions.
ebc7139
to
396aa15
Compare
Forget coersions, I want unboxed constraints in general! In the discussion of #32 the very natural |
Some comments:
|
I'm usually in favour of exposing in the source language the stuff you can do in Core. But as Ryan points out, this proposal bumps into the uneasy Constraint-vs-* debate, which is far from settled. (All we havew now is an unsatisfactory compromise.) One thought. For a long time I've wanted to experiment with making GHC be strict in all constraint arguments. They are always non-bottom. If we did that, then I'd love someone to explore this. |
@RyanGlScott, now that GHC Trac 14978 is fixed (thanks, @simonpj), we can unpack equalities into datatypes just fine, although I suppose we still can't pass them directly to functions. That works because GADTs already offer a certain amount of access to unboxed equalities. We have nothing similar for representational coercions. As for tuple constraints, what I mean is that it seems a bit odd to have a "tuple" that contains unboxed things. If we have unboxed equalities, we might write |
I'll respond to each of your points separately. After reading your first point, it seems that your primary use case here is to unpack GADTs with equality/ data a :~: b where
Refl :: a ~ b => a :~: b
type family Foo a b
data Goof a b where
Goof :: !(Foo a b :~: Int) -> Goof a b And I presume you also want to do something like this? data Coercion a b where
Coercion :: Coercible a b => Coercion a b
data Bidoof a b where
Bidoof :: !(Coercion (Foo a b) Int) -> Bidoof a b Does this work? If not, is your motivation for introducing unboxed coercions to support code like this? Or do you want unboxed coercions for the sake of having them be a first-class programming construct? (Or something in between?) As for your second point, yes, I agree that As @simonpj notes, it would be nice if unboxed constraints Just Worked™ without needing to change the surface syntax to support them. I'm not qualified enough to say how much of GHC would need to be altered to make this happen, but perhaps others can chime in here. |
@RyanGlScott, a key point is that data a :~: b where
Refl :: a :~: a which is actually represented differently! There's nothing like the latter (in surface Haskell) to express coercibility. |
Oh, so you're saying that |
Refl ends up unary instead of nullary. This is because explicit constraints
are always boxed.
…On Wed, Apr 11, 2018, 11:29 AM Ryan Scott ***@***.***> wrote:
Oh, so you're saying that (:~:) unpacks differently if you have Refl :: a
:~: a as opposed to Refl :: a ~ b => a :~: b? How does this manifest?
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
<#116 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/ABzi_Ya94jDetvxftsInpUX_5Vwrdu9jks5tniFJgaJpZM4S7nop>
.
|
That's stunning. I would expect them to unbox the same, since they desugar to the same thing in Core! Maybe this should be another Trac ticket in itself. |
I don't think they desugar to the same thing. Unless I'm reading it write
wrong.
…On Wed, Apr 11, 2018, 11:34 AM Ryan Scott ***@***.***> wrote:
That's stunning. I would expect them to unbox the same, since they desugar
to the same thing in Core! Maybe this should be another Trac ticket in
itself.
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
<#116 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/ABzi_TDG2hZEh2Q6Fq5Sc3MK2IueaDlCks5tniJogaJpZM4S7nop>
.
|
They most certainly do! The surface syntax is the slightly different, but GHC generates a wrapper function for the {-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
data a :~: b where
Refl :: a :~: a With:
|
For the sake of transparency, I'll mention that I have another ulterior motive for wanting unboxed equalities in addition to unboxed coercions. There's a slew of Trac tickets (#12677 being one of them) which demonstrate surprising behavior of equality constraints. A simple program which demonstrates this is: foo :: forall k (a :: k). k ~ Type => a -> a
foo x = x It turns out that the type signature of
This is despite the fact that we've constrained In theory, unboxed equalities fix this problem. With unboxed equality, one could write this: foo' :: forall k (a :: k). k ~# Type => a -> a
foo' x = x And have it kind-check, since there is no way for I want to put emphasis on the "in theory" part, since I've severely downplaying the amount of work needed to actually expose unboxed equalities. @goldfirere has some notes here about how one might implement this, and while I don't understand all of the details, one thing is very clear: it's not going to be a walk in the park. What this means is that implementing unboxed coercions will likely be equally challenging. I'm not writing this down to discourage you from pursuing this, since I do think it would be extremely worthwhile to add to GHC, but it is worth keeping in mind that it's a sticky wicket. An alternative approach would be avoiding the use of unboxed equalities/coercions entirely and allow data constructors with lifted equality or data Equal' a b where
Equal' :: (a ~ b) => Equal' a b
data Coercion a b where
Coercion :: Coercible a b => Coercion a b |
Did you resolve this? I didn't understand all the dialogue. If not, might someone open a ticket with a free-standing explanation of the problem? |
Yes, that was exactly my point in #116 (comment). I think this avenue is really worth pursuing. |
What part was confusing? The problem is quite simple: this unboxes: data Equal a b where
Equal :: Equal a a But this doesn't: data Equal' a b where
Equal' :: (a ~ b) => Equal' a b (And similarly when The questions that this brings up are:
I don't feel like we can properly turn this into a Trac ticket until we get a better sense of @treeowl's overarching goals. If simply unpacking data types with equalty/ |
Thanks, that is helpful. But what precisely does "this unboxes" mean? |
"Unboxes" in the sense that putting an {-# LANGUAGE GADTs #-}
module Foo where
data Equal a b where
Equal :: Equal a a
data Equal' a b where
Equal' :: (a ~ b) => Equal' a b
data Goof a where
Goof :: {-# UNPACK #-} !(Equal a Int) -> Goof a
data Bidoof a where
Bidoof :: {-# UNPACK #-} !(Equal' a Int) -> Bidoof a
foo :: Goof Int
foo = Goof Equal
bar :: Bidoof Int
bar = Bidoof Equal'
Here, |
Ah, now I see, thanks. The problem is not in the unpacking into Goof or Bidoof. It's that
So an Possible solutions:
I really think the former is worth a try. It'd make lots of pograms faster. |
Would making evidence strict cause trouble for |
This has been quiet for a while. Whither this proposal? |
What is the status of this proposal (especially in light of https://mail.haskell.org/pipermail/ghc-devs/2018-September/016191.html)? |
6b33e58
to
e7fdbc7
Compare
Closing this due to inactivity, but it can be reopened when necessary. |
N.B. as "A Role for Dependent Types in Haskell" resolves the constraint-type separation problem, I think we know how to have unboxed constraints properly now. |
Offer access to unboxed coercions.
Rendered