Make Constraint not apart from Type

[goldfirere]

This proposal describes a change to separate Constraint from Type.

Rendered

[simonpj]

I'm strongly favour of this proposal.

I don't think it's abusing RuntimeRep in the slightest. We already have reps that are distinguished even though they may be passed in the same register (IntRep, WordRep)

Simon

[int-index]

I don't think it's abusing RuntimeRep in the slightest.

I think it is, because whether a value can be a constraint (i.e. appear to the left of =>) has nothing to do with its runtime representation - it has to do with coherency. It is entirely orthogonal.

Having a separate flag data Coherency = Coherent | Incoherent would be better, with TYPE :: Coherency -> RuntimeRep -> Type, because then tuples could be coherency-polymorphic:

() :: TYPE c LiftedRep
(,) :: TYPE c LiftedRep -> TYPE c LiftedRep -> TYPE c LiftedRep
(,,) :: TYPE c LiftedRep -> TYPE c LiftedRep -> TYPE c LiftedRep -> TYPE c LiftedRep

This solution is originally from https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes (search for "Constraintiness" in Proposal B2).

Coherency polymorphism for tuples would solve the issue around their kind inference:

type family F x where
  F Char = ()
  F x = Num x

this code is currently rejected with this error:

    • Expected a type, but ‘Num x’ has kind ‘Constraint’
    • In the type ‘Num x’
      In the type family declaration for ‘F’

but is accepted if I write () :: Constraint in the first clause. AFAIK there's some ad-hoc code to detect whether () refers to () :: Type or () :: Constraint, hopefully it could be removed. And I wasn't able to get (,) (Num Int) (Ord Int) to compile at all, although (Num Int, Ord Int) works fine.

Another point in favor of separate Coherency parameter to TYPE is that it would then make sense to talk about unboxed/unlifted constraints (TYPE Coherent IntRep, for example). Provided that one-method classes without superclasses are desugared to newtypes, and that there's a long-standing ticket to make unboxed newtypes possible (https://ghc.haskell.org/trac/ghc/ticket/1311), the separation would open a possibility to think about passing some constraints as unboxed data:

newtype TaggedInt# t = TaggedInt# Int#

-- In theory, the dictionary for this class could be passed
-- as an unboxed integer.
class C t where
  n :: TaggedInt# t 

The proposed design makes sense provided that currently constraints are forced to have LiftedRep. But I believe we can do better!

Other than that, I'm very much in favor of this proposal. Especially since it's a blocker for the new Typeable design. Thank you Richard for the write-up and extra thanks for volunteering to implement! With separate Coherency flag or not, it's better than the status quo.

[Icelandjack]

Do we need to consider extensibility and backwards compatibility? Idris encodes uniqueness types in its kinds (Type* stands for a regular Type or UniqueType), in the future maybe we want

TYPE :: Uniqueness -> Coherency -> RuntimeRep -> Type

+ the various ideas discussed in UnliftedDataTypes (unlifted / boxed levity polymorphism), is this a concern?

[Ericson2314]

@int-index Can I check if I understand you correctly? In the PR @goldfirere alludes to an argument of yours for conflating Type and Constraint everywhere, but what you wrote above is not that but rather a different way of separating Type and Constraint in Core and Haskell alike, right?

If so, I quite like the TYPE :: Coherency -> RuntimeRep -> Type solution. I'm reminded of #29 (comment) --- maybe someday we'll have a 3rd (or forth with liftedness!) mustEliminate argument or similar?

[int-index]

@Ericson2314 Yes, your understanding is correct.

In the comments to the Trac ticket I advocated for an alternative solution, which is to abolish the difference between Type and Constraint. My main arguments were that it would allow us to get rid of Dict and make the internals of reflection prettier (removing unsafeCoerce).

But I do see value in keeping Type and Constraint separate. Lots of code relies on coherency, so it's good to keep track of this in the type system. And I have some thoughts on how to achieve the same results (getting rid of Dict and improving reflection) while keeping the separation if we express coherency as a separate parameter to TYPE and allow coherency-polymorphic definitions. So there might be a way to have our cake and eat it too :)

[simonpj]

int-index's suggestion is quite cool. Rather than "coherence" I thnk it might be better to think in terms of singleton types. So if ty :: TYPE Singleton rep, then ty is a signleton type with only one inhabitant (otehr than bottom if rep is lifted. The more common case is ty :: TYPE Multi rep, meaning that ty` can have many inhabitants.

The point about singletons is that we can infer them... that's what type classes do. To the left of an arrow we'd use a =>.

It's nice that we could use polymorphism to re-unite class and term tuples. And the point about () is a good one.

Whether is is worth dong this for all reps (as proposed) or only for LiftedPtrRep, I'm not sure. The former is more general, but a bit more faff. But I suippose the common case is the lifted one anyway.

[int-index]

Rather than "coherence" I thnk it might be better to think in terms of singleton types

I don't think that class dictionaries can be considered singleton types... For example, Ord Bool has at least two possible implementations, one with True > False and one with False > True. So there are multiple inhabitants of the Ord Bool type. However, what matters is that whenever we get a dictionary for Ord Bool, we know it's the same one as everywhere else - that's coherency.

Constrains (as in "things to the left of =>") exhibit the property that their only identification is the type. That's because (a, a) => x is the same as a => x - we cannot meaningfully distinguish multiple values of the same type. But it's not important to us whether a has only one possible inhabitant - what matters is that it's the same inhabitant - we rely on coherency.

Singleton types are intrinsically coherent, but the inverse is not true. For this reason, I think "coherency" is a better name for the property in question.

[goldfirere]

Do we need to consider extensibility and backwards compatibility?

I think we're better off if we don't. What I mean here is that I would want this feature to evolve over time, much in the spirit of many suggestions on this Issue. I don't think we're going to get this right in one go, so we need flexibility to maneuver. Accordingly, I would not want to guarantee to clients that the interface around RuntimeRep is stable across major releases. Clients have to import GHC.Exts, so they know they're playing with fire.

I don't think that class dictionaries can be considered singleton types

I agree with your observations here. It makes me wonder if we want

data Coherency = Singleton | Coherent | Multiple

where Singleton and Coherent classify types that are expected to be singletons (only one possible value) or coherent (multiple values, but only one that appears in a program). However, how would the type system distinguish between singletons and coherents? Both seem like sensible candidates to the left of =>. So, while I agree that singletons and coherents are distinguishable concepts, it's unclear to me how this will affect Haskell programs.

[int-index]

However, how would the type system distinguish between singletons and coherents? Both seem like sensible candidates to the left of =>.

Well, as long as we want type classes to go to the left of =>, it seems that we want coherency to be the defining property. Whether a type is a singleton type or not is another orthogonal question, which is a special case of "how many inhabitants a type has". I'd express it as

data Size = Finite Nat | Infinite

with Finite (S Z) denoting singleton types.

There's somewhat of a functional dependency here: Finite (S Z) implies Coherent. But it's a separate thing.

What would be the practical benefit of giving singleton types (and in general, types of a known size) a separate kind? It probably could be used in some cool ways (e.g. proving two types isomorphic) but it seems to be way out of scope of this proposal.

Since the goal is to distinguish Type and Constraint, coherency looks to me as the right distinguishing factor between them.

[simonpj]

On reflection I propose that FOR NOW we go ahead with the proposal as originally posed. That sovles our immedaite problem.

There are more alaborate things we could do, but it's not yet clear exactly what the best is; they are more far-reaching (eg combining tuples kinds). I'm keen to get the basic separation of Constraint and * done for 8.2 (ie within the next week or two). We can work on something more ambitious later. We can specifically advertise the the details of RuntimeRep may change in the future.

[simonpj]

PS

I don't think that class dictionaries can be considered singleton types.

You are absolutely right about this. My bad.

[Ericson2314]

Hmm I did like thinking about coherency as a special variety of singleton or uninhabited types. The record type representing a type class dictionary would not be singleton and be in *, but there's a wrapper sending * types to the coherent lifted kind in which types are by fiat only inhabited by their wrapped canonical value (if there is one).

We don't need Dict because it's fine to pass around that wrapped canonical value by hand, and convert it back to the plain old record value too, but GHC must infer the single wrapped field if we wish to construct the wrapper value.

[rwbarton]

I haven't been following this closely, but as I understand it an implicit parameter (?x :: Bool) is a Constraint, and it doesn't seem to be "coherent". Do implicit parameters need to be accounted for in this?

[int-index]

@rwbarton That's exactly the reason implicit parameters are considered a design mistake. Their incoherence compromises the thinness of Constraint as a category (with objects=constraints and arrows=entailment).

Not only are implicit parameters incoherent, they also have undocumented shadowing semantics (unlike all other constraints) and interact weirdly with GADTs:

Prelude> :set -XImplicitParams -XGADTs
Prelude> data X where X :: (?x :: Int) => X
Prelude> f :: X -> X -> Int; f X X = ?x
Prelude> let a :: X; a = let ?x=1 in X
Prelude> let b :: X; b = let ?x=2 in X
Prelude> f a b
2
Prelude> f b a
1

Notice how GHC picks the second instance with ?x = 2. If we violate the coherency using the reflection trickery, we can see that normally GHC picks the first available instance (although it is free to pick any, really):

Prelude> :set -XGADTs -XFlexibleContexts
Prelude> import Data.Reflection
Prelude Data.Reflection> data X where X :: Given Int => X
Prelude Data.Reflection> f X X = given :: Int
Prelude Data.Reflection> a = give (1 :: Int) X
Prelude Data.Reflection> b = give (2 :: Int) X
Prelude Data.Reflection> f a b
1
Prelude Data.Reflection> f b a
2

@goldfirere says this may not even be reliable. Fortunately, implicit parameters can't "spread" their incoherence to classes because they are not allowed to appear in superclass/instance contexts.

In context of this proposal I think it means that we're not making things worse by pretending implicit parameters are coherent, because we already do. It's a broken extension.

[bgamari]

Note that this proposal is now half-way through its four week discussion period. At the end of this period we ask @goldfirere to summarize the discussion and bring the proposal to the GHC committee for consideration. Thanks to everyone who has contributed thusfar!

[simonpj]

As I said above, I move to adopt the proposal. It may be imrpoved later in the light of experience, but I think we want the basic thing, as proposed, in GHC 8.2

[treeowl]

I haven't been following this closely, but note that I have also been hashing out with @simonpj how we might provide special support for reflection. I have no interest in the shady incoherent Given, but I am very interested in the beautiful and coherent Reifies. Thanks to the rank-2 type of reify (and the somewhat-unfortunately-necessary existence of certain concrete instances), Reifies gives us coherence with "local instances" without singletons. As I understand it, Simon thinks what we'll need is the ability to get coercions between Coercion and * types in at least the simple case of a 1-method class.

See https://ghc.haskell.org/trac/ghc/wiki/MagicalReflectionSupport for further discussion. The data family variant there seems especially promising as an API.

[int-index]

I have no interest in the shady incoherent Given

@treeowl As much as I'd want to be agree, sometimes unsafe features are necessary due to the weaknesses of the type system. E.g. unsafeCoerce would be unnecessary if the type system was perfect. unsafePerformIO would be unnecessary if GHC could analyze that there are really no observable side effects in a piece of IO code. unsafeFreeze would be unnecessary with a perfect linear/uniqueness type system. And similarly, incoherentReify (known as give in reflection) would be unnecessary if it would be always possible to check that an implicit parameter is used coherently.

Unfortunately, we don't live in a world with perfect machine checking of desired properties - sometimes the programmer has to override the safety mechanisms because he knows that a piece of code is safe, but the compiler doesn't.

I fully support your efforts to devise a safe reflection mechanism. But make sure that there's an incoherentReify as well - the safe interface can be built on top.

As an example of the things that Reifies-style reflection doesn't cover, consider singleton-types: by virtue of having only one non-bottom value, they are intrinsically coherent (see discussion above). However, there's no notion of a singleton value in the compiler, and the design is not clear at all. The singletons library defines SingI for this purpose, which, sure enough, is dirty and unsafe under the hood.

@simonpj has said "There is a long tradition in Haskell of doing things the Right Way and using the pain to drive innovation." I agree! But we can do it gradually. Let's first cover all use cases of all styles of reflection (Reifies, Given and SingI) with a function like incoherentReify - it'll be a definite improvement over unsafeCoerce. Then we can start thinking about getting rid of incoherentReify.

[treeowl]

The proposed reflection magic will also cover the shady cases. But it will need coercion from Richard or some other type hacker.

[simonpj]

The reificiation story is only tangentially related to this proposal. It's interesting and useful but needs its own proposal.

[goldfirere]

I have changed this proposal significantly, going essentially for what was suggested in @int-index 's first comment in this thread. The reason for the change is in the Alternatives section of the updated proposal, repeated here:

The main alternative is a previous version of this proposal, where we would add a new constructor of RuntimeRep called ConstraintRep. We would then distinguish Type from Constraint via the choice of RuntimeRep. However, this runs into a major problem: we have a hard time rejecting Eq a -> a -> Bool. (Note the -> instead of =>.) Seeing Eq a -> a -> Bool, GHC would happily accept, because anything of the form TYPE r to the left of an arrow should be OK. We can only be sure something is wrong after zonking, and by then, we've lost the original Haskell AST that the user wrote, so we can't tell whether they wrote => or ->. Of course, this problem could be avoided by engineering, but there is another wrinkle. Consider the type forall (r :: RuntimeRep) (a :: TYPE r). a -> a. Forget for a moment that this is unimplementable. The problem is that the type is sensible only for most choices of r, not all of them: choosing r to be ConstraintRep makes the type bogus. So something is really quite smelly with this design.

[simonpj]

I'm good with this. Thank you int-index for originally suggesting the coherence-flag idea.

Let's do it!

Simon

[nomeata]

What is the status of this proposal?

[goldfirere]

Honestly, it's awaiting more feedback (which I suppose I should try to solicit -- hopefully these posts will get that feedback). The most recent version lists several alternative solutions, none of which makes me very happy. I do think we need to do one of them by 8.4, though. I'm currently leaning toward Alternative (4) (just fix the bugs that motivated the proposal, without actually separating Constraint from Type), if only because what we really want is Alternative (3), which needs more time to mature.

[nomeata]

Marking this as dormant for now, for lack of active discussion.

[goldfirere]

I've updated the proposal to propose what I think is the best alternative. The old, much heavier alternatives are kept at the bottom of the current proposal text. In the absence of recent community contributions to this discussion, I'd like to submit to the committee, @nomeata. The text of the proposal reflects the general discussion here that the original proposal was a bit of a Rube Goldberg machine designed to remove an unsightly blemish. This new proposal basically declares the blemish as a feature and moves on.

[Ericson2314]

What's the forward compatability of this?!?!? I'd hate to grandfather in the wart, especially if the some pending research on kind coersions can give us the nice solution.

[goldfirere]

Forward compatibility is preserved. If we make Type and Constraint to be apart in the future (which I very much hope we will), then simply more programs will be accepted. The more types that are apart (while still obeying the apartness properties as detailed in the Closed Type Families paper), the better.

The temporal-compatibility problem is really backward-compatibility. Today, you can write

type instance F Type = Int
type instance F Constraint = Bool

and perhaps someone has done so. With this proposal, you would no longer be able to write that. Then, strangely, in the future (when the kind coercion research is complete), you will be able to write it again. That's surely annoying to users, but I think this is a dark enough corner that we can get away with it. And what we have now is just plain unsound!

[simonpj]

I can see that the new proposal fixes (1) under "Motivation". But how does it fix (2) and (3)? (Indeed I don't understand how (3) arises in the first place.)

[simonpj]

Motivators (2)-(3) are all to do with Typeable. We could fix this by teaching the Typeable solver to offer up one TypeRep for Type and a different one for Constraint. These TypeReps would compare as different. Indeed, in retrospect, I'm not sure why we haven't already done this.

This sounds like part of the proposal. Can you move it to the Specification and specify the change?

[Ericson2314]

@goldfirere Whew, thanks!

[goldfirere]

The Typeable stuff doesn't really belong in the proposal. They are just bugs that need to be fixed -- a red herring.

I've updated the proposal to remove them (saving them at the bottom for posterity).

[RyanGlScott]

They are just bugs that need to be fixed -- a red herring.

Interesting—are you claiming that we could fix #11715 independently of making Constraint apart from Type? I was under the impression that it was a hard prerequisite. Moreover, there are several other bugs that also result from confusing Constraint and Type, such as:

• #11621 and #13742: GHC thinks Constraint-kinded things are Type-kinded in closed type family RHSes

• #14048: GHC currently accepts:

  data Bot1 :: Constraint
  data family Bot2 :: Constraint

• RyanGlScott/eliminators#4 (comment) / #14869: reifying a type family with Constraint as the return kind gives you Type instead:

  λ> type family Foo :: Constraint
  λ> putStrLn $(reify ''Foo >>= stringE . pprint)
  type family Ghci3.Foo :: *
  

How feasible would it be to fix these without making Constraint and Type apart?

[goldfirere]

Without looking at the tickets themselves, your summaries seem fixable without fully separating Constraint from Type. The last one, about TH reification, seems harder. Maybe, but no promises there.

[RyanGlScott]

I'm at least reassured that you think the first two are fixable, as those were the ones I was least certain of! And I'm now more confident that we can fix the last one (about TH reification) too—see my comment on the Trac ticket.

[nomeata]

Accepted and merged.