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
Make Constraint not apart from Type #32
Conversation
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 |
I think it is, because whether a value can be a constraint (i.e. appear to the left of Having a separate flag
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:
this code is currently rejected with this error:
but is accepted if I write Another point in favor of separate
The proposed design makes sense provided that currently constraints are forced to have Other than that, I'm very much in favor of this proposal. Especially since it's a blocker for the new |
Do we need to consider extensibility and backwards compatibility? Idris encodes uniqueness types in its kinds ( TYPE :: Uniqueness -> Coherency -> RuntimeRep -> Type + the various ideas discussed in UnliftedDataTypes (unlifted / boxed levity polymorphism), is this a concern? |
@int-index Can I check if I understand you correctly? In the PR @goldfirere alludes to an argument of yours for conflating If so, I quite like the |
@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 But I do see value in keeping |
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 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 Whether is is worth dong this for all reps (as proposed) or only for |
I don't think that class dictionaries can be considered singleton types... For example, Constrains (as in "things to the left of 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. |
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
I agree with your observations here. It makes me wonder if we want
where |
Well, as long as we want type classes to go to the left of
with There's somewhat of a functional dependency here: 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 |
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. |
PS
You are absolutely right about this. My bad. |
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 We don't need |
I haven't been following this closely, but as I understand it an implicit parameter |
@rwbarton That's exactly the reason implicit parameters are considered a design mistake. Their incoherence compromises the thinness of Not only are implicit parameters incoherent, they also have undocumented shadowing semantics (unlike all other constraints) and interact weirdly with GADTs:
Notice how GHC picks the second instance with
@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. |
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! |
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 |
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 See https://ghc.haskell.org/trac/ghc/wiki/MagicalReflectionSupport for further discussion. The data family variant there seems especially promising as an API. |
@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. 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 As an example of the things that @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 ( |
The proposed reflection magic will also cover the shady cases. But it will
need coercion from Richard or some other type hacker.
|
The reificiation story is only tangentially related to this proposal. It's interesting and useful but needs its own proposal. |
See a new paragraph in Alternatives for a discussion of the motivation for this change.
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 |
I'm good with this. Thank you int-index for originally suggesting the coherence-flag idea. Let's do it! Simon |
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. |
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. |
Forward compatibility is preserved. If we make The temporal-compatibility problem is really backward-compatibility. Today, you can write
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! |
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.) |
This sounds like part of the proposal. Can you move it to the Specification and specify the change? |
@goldfirere Whew, thanks! |
The I've updated the proposal to remove them (saving them at the bottom for posterity). |
Interesting—are you claiming that we could fix #11715 independently of making
How feasible would it be to fix these without making |
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. |
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. |
Accepted and merged. |
@goldfirere, this proposal has no GHC ticket associated with it. What's it status? Already implemented? Far from it? |
I have made a ticket and updated the proposal text accordingly. Should be easy. |
I believe this should PR should have an "Implemented" label |
The proposal has been accepted; the following discussion is mostly of historic interest.
This proposal describes a change to separate
Constraint
fromType
.Rendered