Skip to content
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

Closed
wants to merge 1 commit into from
Closed

Conversation

treeowl
Copy link
Contributor

@treeowl treeowl commented Mar 26, 2018

Offer access to unboxed coercions.

Rendered

Offer access to unboxed coercions.
@Ericson2314
Copy link
Contributor

Ericson2314 commented Mar 26, 2018

Forget coersions, I want unboxed constraints in general! In the discussion of #32 the very natural TYPE :: RuntimeRep -> Coherence -> Type approach came up. Yes, @goldfirere points out more research on kind-level coercion is required. Well, I'd love to see a looming GHC release expedite that. 😂

@RyanGlScott
Copy link
Contributor

Some comments:

  1. The scope of this proposal feels a tad limited. Why not also include unboxed equalities as well? They do use the same machinery as your proposed unboxed coercion, after all (just with a different role).

  2. You allude to potential issues with tuple constraints that I didn't follow. Can you go into more detail on this aspect?

  3. Another potentially troublesome aspect of "banged constraints"/exposing ~R# directly is coming up with a kind signature for them. At one point, I was curious and tried exposing ~R# myself (through Template Haskell hackery) and discovered that internally, GHC thinks the kind of ~R# is:

    (~R#) :: forall k. k -> k -> TYPE (TupleRep '[])

    This is sufficiently weird enough that GHC didn't know how to handle it if I tried using ~R# as an actual constraint, as it wouldn't kind-check (it expected something of kind Constraint, but was given something of kind TYPE (TupleRep '[]) instead.

    To make these options truly usable, we might need to invent another kind to describe it. (CONSTRAINT :: RuntimeRep -> Type, where type Constraint = CONSTRAINT LiftedRep and (~R#) :: forall k. k -> k -> CONSTRAINT (TupleRep '[])?)

@simonpj
Copy link
Contributor

simonpj commented Apr 2, 2018

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 One would evaluate and unbox its Coercible constraint, and that would make it much more efficient. No language change would be needed at all. And it might make lots of programs run a bit faster.

I'd love someone to explore this. -XStrictDicts is the flag, but it's atrophied.

@treeowl
Copy link
Contributor Author

treeowl commented Apr 11, 2018

@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 (Num a, Coercible# a b), which makes me a bit nervous.

@RyanGlScott
Copy link
Contributor

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/Coercible constraints, yes? In other words, you want to be able to do something like the example program from Trac #14978:

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 (Num a, Coercible# a b) is rather intriguing. On one hand, we could just say that that's an OK thing to do, since we could treat (Num a, Coercible# a b) => r as Num a => Coercible# a b => r, which isn't problematic (AFAICT). But if we do thing, would we need to generalize the kind signature of constraint tuples from Constraint -> Constraint -> ... -> Constraint to something more inclusive? I'm not sure.

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.

@treeowl
Copy link
Contributor Author

treeowl commented Apr 11, 2018

@RyanGlScott, a key point is that :~: is defined

data a :~: b where
  Refl :: a :~: a

which is actually represented differently! There's nothing like the latter (in surface Haskell) to express coercibility.

@RyanGlScott
Copy link
Contributor

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?

@treeowl
Copy link
Contributor Author

treeowl commented Apr 11, 2018 via email

@RyanGlScott
Copy link
Contributor

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.

@treeowl
Copy link
Contributor Author

treeowl commented Apr 11, 2018 via email

@RyanGlScott
Copy link
Contributor

They most certainly do! The surface syntax is the slightly different, but GHC generates a wrapper function for the Refl :: a :~: a version which converts it into the form that Core expects (i.e., with explicit equality constraints). You can verify this for yourself by compiling this:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Foo where

data a :~: b where
  Refl :: a :~: a

With:

$ ghc Foo.hs -ddump-simpl -dsuppress-module-prefixes -dsuppress-uniques -dsuppress-idinfo 
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )

==================== Tidy Core ====================
Result size of Tidy Core
  = {terms: 58, types: 29, coercions: 1, joins: 0/0}

-- RHS size: {terms: 2, types: 4, coercions: 1, joins: 0/0}
$WRefl :: forall a. a :~: a
$WRefl = \ (@ a) -> Refl @ a @ a @~ (<a>_N :: (a :: *) ~# (a :: *))

@RyanGlScott
Copy link
Contributor

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 foo does not kind-check:

    • Expected a type, but ‘a’ has kind ‘k’
    • In the type signature:
        foo :: forall k (a :: k). k ~ Type => a -> a

This is despite the fact that we've constrained k to be Type! Well, almost. Because (~) is lifted equality, it can (in principle) be inhabited by , so we can't use k ~ Type in type-level casts (lest the evidence it uses happens to be ).

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 k ~# Type to be inhabited by .

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 Coercible constraints to be unpacked, such as:

data Equal' a b where
  Equal' :: (a ~ b) => Equal' a b

data Coercion a b where
  Coercion :: Coercible a b => Coercion a b

@simonpj
Copy link
Contributor

simonpj commented Apr 18, 2018

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.

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?

@simonpj
Copy link
Contributor

simonpj commented Apr 18, 2018

An alternative approach would be avoiding the use of unboxed equalities/coercions entirely and allow data constructors with lifted equality or Coercible constraints to be unpacked, such as:

Yes, that was exactly my point in #116 (comment). I think this avenue is really worth pursuing.

@RyanGlScott
Copy link
Contributor

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 (~) is replaced with Coercible.)

The questions that this brings up are:

  1. Is this intended? (I would think not, for the reasons I articulate in Unboxed coercions #116 (comment).)
  2. Can this restriction be relaxed? I would hope so, but the method by which we accomplish this is unclear. @treeowl proposes several options, with varying degrees of complexity.

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/Coercible constraints is the heart of the matter, then I think this is just a matter of improving the existing implementation of isUnpackableType. If having access to unboxed coercions themselves is the end goal, then we'd need to flesh out the proposal more.

@simonpj
Copy link
Contributor

simonpj commented Apr 18, 2018

Thanks, that is helpful. But what precisely does "this unboxes" mean?

@RyanGlScott
Copy link
Contributor

"Unboxes" in the sense that putting an {-# UNPACK #-} pragma in front of it as a data type field does the expected thing. You can observe this for yourself in this program:

{-# 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'
$ ~/Software/ghc/inplace/bin/ghc-stage2 -O2 Foo.hs -ddump-simpl -fforce-recomp -dsuppress-module-prefixes -dsuppress-uniques -dsuppress-idinfo
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )

==================== Tidy Core ====================
Result size of Tidy Core
  = {terms: 221, types: 139, coercions: 10, joins: 0/0}

...

-- RHS size: {terms: 1, types: 1, coercions: 1, joins: 0/0}
foo :: Goof Int
foo = Goof @ Int @~ (<Int>_N :: (Int :: *) ~# (Int :: *))

...

-- RHS size: {terms: 1, types: 6, coercions: 1, joins: 0/0}
bar1 :: (Int :: *) ~~ (Int :: *)
bar1
  = Eq# @ * @ * @ Int @ Int @~ (<Int>_N :: (Int :: *) ~# (Int :: *))

-- RHS size: {terms: 2, types: 1, coercions: 6, joins: 0/0}
bar :: Bidoof Int
bar
  = Bidoof
      @ Int
      (bar1
       `cast` (Sym (N:~[0] <*>_N) <Int>_N <Int>_N
               :: ((Int :: *) ~~ (Int :: *) :: Constraint)
                  ~R# ((Int :: *) ~ (Int :: *) :: Constraint)))

Here, foo uses unboxed equality, but bar uses boxed equality.

@simonpj
Copy link
Contributor

simonpj commented Apr 18, 2018

Ah, now I see, thanks.

The problem is not in the unpacking into Goof or Bidoof. It's that

Equal :: (a ~# b) => Equal a b
Equal' :: (a ~ b) => Equal' a b

So an Equal constructor has a zero-width equality field, while Equal' has a full word pointer to evidence for a~b.

Possible solutions:

  • Make all evidence strict, as I suggest above, and by-default unbox equalities because they are zero width when unpacked.

  • Allow bangs on constraints to make them strict.

I really think the former is worth a try. It'd make lots of pograms faster.

@treeowl
Copy link
Contributor Author

treeowl commented Apr 19, 2018

Would making evidence strict cause trouble for UndecidableInstances or UndecidableSuperClasses? If not, it sounds like a good idea.

@nomeata
Copy link
Contributor

nomeata commented Jun 23, 2018

This has been quiet for a while. Whither this proposal?

@RyanGlScott
Copy link
Contributor

What is the status of this proposal (especially in light of https://mail.haskell.org/pipermail/ghc-devs/2018-September/016191.html)?

@bravit bravit removed the Proposal label Dec 3, 2018
@nomeata nomeata added the Dormant The proposal is not being actively discussed, but can be revived label May 4, 2019
@nomeata nomeata force-pushed the master branch 3 times, most recently from 6b33e58 to e7fdbc7 Compare June 11, 2019 12:04
@nomeata
Copy link
Contributor

nomeata commented Aug 20, 2019

Closing this due to inactivity, but it can be reopened when necessary.

@nomeata nomeata closed this Aug 20, 2019
@Ericson2314
Copy link
Contributor

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Dormant The proposal is not being actively discussed, but can be revived
Development

Successfully merging this pull request may close these issues.

None yet

6 participants