Hello all,
I recently noticed that GHC rejects the following program: type family F a b :: Constraint where F a a = () eq :: F a b => a :~: b eq = Refl This is certainly not shocking, but it is a little unsatisfying: as far as I can tell, accepting this program would be entirely sound. That is, `a ~ b` is morally a “superclass” of `F a b`. In this example the type family is admittedly rather pointless, as `a ~ b` could be used instead, but it is possible to construct more sophisticated examples that cannot be so straightforwardly expressed in other ways. I am therefore curious: has this kind of scenario ever been discussed before? If yes, is there a paper/GitLab issue/email thread somewhere that discusses it? And if no, is there any fundamental reason that GHC does not propagate such information (i.e. it’s incompatible with some aspect of the type system or constraint solver), or is it simply something that has not been explored? (Maybe you think the above program is horrible and *shouldn’t* be accepted even if it were possible, but that is a different question entirely. :)) Thanks, Alexis _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Hi Alexis,
I'm not aware of any work in this direction. It's an interesting idea to think about. A few such disconnected thoughts: - You could refactor the type family equation to be `F a b = a ~ b`. Then your program would be accepted. And -- assuming the more sophisticated example is also of kind constraint -- any non-linear pattern could be refactored similarly, so perhaps this observation would carry over. - If we had constrained type families (paper: https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1075&context=compsci_pubs, proposal:https://github.com/ghc-proposals/ghc-proposals/pull/177), you could express a superclass constraint on the enclosing type family, which would likely work very much in the way you would want. Richard
_______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Hi Richard,
Thanks for the pointer to constrained type families—that’s helpful to clarify some of my thoughts about this, and it is indeed relevant! One example I had in my real code seems difficult to express even with constrained type families, however; here is a stripped-down version of it: type family F a b :: Constraint where F '[] (A _) = () F (B a ': b) (C c d) = (a ~ c, F b d) With the above type family, if we have the given `F (B a ': b) c`, we’d really like GHC to be able to derive `c ~ C t1 t2` so that the type family can continue to reduce, yielding the givens `a ~ t1` and `F b t2`. But we can’t use your trick of moving the equality into the RHS because we need to procure two fresh unification variables, something we are unable to do. The family is simply stuck, and there isn’t much we can do to cajole GHC into believing otherwise. In the above example, what the “superclasses” of F are is much less clear. We end up with a few different implications: F '[] a :- a ~ A t1 F a (A b) :- a ~ '[] F (B a ': b) c :- c ~ C t1 t2 F a (C b c) :- a ~ (B t1 ': t2) I don’t know if there is a way to encode those using the constraint language available in source Haskell today. If I understand correctly, I don’t think they can be expressed using quantified constraints. Maybe it’s more trouble than it’s worth, but I find it a little interesting to think about. Anyway, thank you for the response; I think my original question has been answered. :) Alexis > On Dec 29, 2019, at 21:02, Richard Eisenberg <[hidden email]> wrote: > > Hi Alexis, > > I'm not aware of any work in this direction. It's an interesting idea to think about. A few such disconnected thoughts: > > - You could refactor the type family equation to be `F a b = a ~ b`. Then your program would be accepted. And -- assuming the more sophisticated example is also of kind constraint -- any non-linear pattern could be refactored similarly, so perhaps this observation would carry over. > > - If we had constrained type families (paper: https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1075&context=compsci_pubs, proposal:https://github.com/ghc-proposals/ghc-proposals/pull/177), you could express a superclass constraint on the enclosing type family, which would likely work very much in the way you would want. _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
I gave it a good try, but failed. The trick I was hoping to leverage was *partial improvement*. Here is an example of partial improvement: > class FD1 a b | a -> b > class FD2 a b | a -> b > > instance FD1 a b => FD2 (Maybe a) (Maybe b) > > f :: FD2 a b => a -> b > f = undefined > > x = f (Just True) This program will require solving [W] FD2 (Maybe Bool) beta, where the [W] indicates that we have a "wanted" constraint (a goal we are trying to satisfy) and beta is a unification variable. GHC can figure out from the fundep on FD2 that the only FD2 instance that can apply is the one we see above. It thus knows that beta must be Maybe beta2 (for some fresh beta2). This is the essence of partial improvement, when we solve one unification variable with an expression involving another (but is more informative somehow). I thought that, maybe, we could use partial improvement to give you what you want, by replacing the RHSs of the type family with expressions involving classes with fundeps. (Injective type families work very analogously, but it's not worthwhile showing the translation of this idea to that domain here.) I couldn't quite get it to work out, though. Maybe you can, armed with this description... but I doubt it. The problem is that partial improvement must always be a shadow of some "total" improvement process. In the example above, note that I haven't written down an instance of FD1. Clearly, we'll need to satisfy the FD1 constraint in order to satisfy the FD2 constraint. The problem is that, in your example, we really only want partial improvement... and I don't think there's a way to state that. What's tantalizing is that GHC already does all this partial improvement stuff -- it's just that we can't seem to write the instance declarations the way we want to satisfy your use case. I don't know if this really moves us forward at all, but maybe a description of my failure can lead to someone's success. Or perhaps it will lead to a language improvement that will allow us to express what you want. Richard _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
> On Jan 4, 2020, at 20:38, Richard Eisenberg <[hidden email]> wrote:
> > I thought that, maybe, we could use partial improvement to give you what you want I think that improvement alone cannot possibly be enough here, as improvement by its nature does not provide evidence. Improvement allows us to take a set of constraints like [G] FD2 a Bool [W] FD2 a b and derive [WD] b ~ Bool, but importantly this does not produce a new given! This only works if b is a metavariable, since we can solve the new wanted by simply taking b := Bool, but if b is rigid, we are just as stuck as before. In other words, improvement only helps resolve ambiguities, not derive any new information. That’s why I think the “superclass” characterization is more useful. If instead we express your FD2 class as class b ~ B a => FD2 a b where type B a then if we have [G] FD2 a Bool, we can actually derive [G] B a ~ Bool, which is much stronger than what we were able to derive using improvement. I imagine you are aware of all of the above already, but it’s not immediately clear to me from your description why you need functional dependencies (and therefore improvement) rather than this kind of approximation using superclasses and type families. Would modeling things with that approximation help at all? If not, why not? I think that would help me understand what you’re saying a little better. Thanks, Alexis _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
You're absolutely right that improvement doesn't solve your problem. But what I didn't say is that there is no real reason (I think) that we can't improve improvement to produce givens. This would likely require a change to the coercion language in Core (and thus not to be taken lightly), but if we can identify a class of programs that clearly benefits from that work, it is more likely to happen. The thoughts about improvement were just a very basic proof-of-concept. Sadly, the proof-of-concept failed, so I think a first step in this direction would be to somehow encode these partial improvements, and then work on changing Core. That road seems too long, though, so in the end, I think constrained type families (with superclass constraints) might be a more fruitful direction.
Richard > On Jan 5, 2020, at 6:02 PM, Alexis King <[hidden email]> wrote: > >> On Jan 4, 2020, at 20:38, Richard Eisenberg <[hidden email]> wrote: >> >> I thought that, maybe, we could use partial improvement to give you what you want > > I think that improvement alone cannot possibly be enough here, as improvement by its nature does not provide evidence. Improvement allows us to take a set of constraints like > > [G] FD2 a Bool > [W] FD2 a b > > and derive [WD] b ~ Bool, but importantly this does not produce a new given! This only works if b is a metavariable, since we can solve the new wanted by simply taking b := Bool, but if b is rigid, we are just as stuck as before. In other words, improvement only helps resolve ambiguities, not derive any new information. > > That’s why I think the “superclass” characterization is more useful. If instead we express your FD2 class as > > class b ~ B a => FD2 a b where > type B a > > then if we have [G] FD2 a Bool, we can actually derive [G] B a ~ Bool, which is much stronger than what we were able to derive using improvement. > > I imagine you are aware of all of the above already, but it’s not immediately clear to me from your description why you need functional dependencies (and therefore improvement) rather than this kind of approximation using superclasses and type families. Would modeling things with that approximation help at all? If not, why not? I think that would help me understand what you’re saying a little better. > > Thanks, > Alexis _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by Alexis King
I've read this thread, superficially so far. But I'm puzzled about the goal.
| type family F a b :: Constraint where | F a a = () | | eq :: F a b => a :~: b | eq = Refl This is rejected, and it's not in the least bit puzzling! You have evidence for (F a b) and you need to prove (a~b) -- for any a and b. Obviously you can't. And in Core you could write (eq @Int @Bool (error "urk")) and you jolly well don’t want it to return Refl. So what's the goal? Simon | -----Original Message----- | From: ghc-devs <[hidden email]> On Behalf Of Alexis King | Sent: 28 December 2019 00:17 | To: ghc-devs <[hidden email]> | Subject: Superclasses of type families returning constraints? | | Hello all, | | I recently noticed that GHC rejects the following program: | | type family F a b :: Constraint where | F a a = () | | eq :: F a b => a :~: b | eq = Refl | | This is certainly not shocking, but it is a little unsatisfying: as far as | I can tell, accepting this program would be entirely sound. That is, `a ~ | b` is morally a “superclass” of `F a b`. In this example the type family is | admittedly rather pointless, as `a ~ b` could be used instead, but it is | possible to construct more sophisticated examples that cannot be so | straightforwardly expressed in other ways. | | I am therefore curious: has this kind of scenario ever been discussed | before? If yes, is there a paper/GitLab issue/email thread somewhere that | discusses it? And if no, is there any fundamental reason that GHC does not | propagate such information (i.e. it’s incompatible with some aspect of the | type system or constraint solver), or is it simply something that has not | been explored? (Maybe you think the above program is horrible and | *shouldn’t* be accepted even if it were possible, but that is a different | question entirely. :)) | | Thanks, | Alexis | _______________________________________________ | ghc-devs mailing list | [hidden email] | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haske | ll.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc- | devs&data=02%7C01%7Csimonpj%40microsoft.com%7C38bb107c30c94853b4b008d78 | b2b37b0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637130890051710518& | ;sdata=z1ag%2BkXBxUbQSc7cY8wTWvEyo%2FxLzxh9tGfAXrabATo%3D&reserved=0 _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
But how could you possibly have evidence for (F a b) without (a ~ b)? You can't.
Why not? > eq = /\ a b. \ (d :: F a b). case d of Something (co :: a ~# b) -> Refl @a @b co This would obviously require extensions to Core and Haskell, but it's not a priori wrong to do so. Richard _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by GHC - devs mailing list
> On Jan 6, 2020, at 08:52, Simon Peyton Jones <[hidden email]> wrote:
> > This is rejected, and it's not in the least bit puzzling! You have evidence for (F a b) and you need to prove (a~b) -- for any a and b. Obviously you can't. And in Core you could write (eq @Int @Bool (error "urk")) and you jolly well don’t want it to return Refl. I’m not sure I totally understand your complaint. If I were to write eq :: a ~ b => a :~: b eq = Refl then in core I could still write `eq @Int @Bool (error "urk")`, and that would be entirely well-typed. It would not really return Refl at runtime, of course, but neither would the example I gave in my original email. Perhaps a better way to phrase my original example is to write it this way: type family F a b where F a b = () -- regular (), not (() :: Constraint) eq :: F a b ~ () => a :~: b eq = Refl In this case, in core, we receive an argument of type `F a b ~ ()`, and we can force that to obtain a coercion of type `F a b ~# ()`. For reasons similar to the mechanisms behind injective type families, that equality really does imply `a ~# b`. The fact that the type family returns an empty constraint tuple is really incidental, and perhaps unnecessarily misleading. Does that clear up your confusion? Or have I misunderstood your concern? Alexis _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
> On Jan 6, 2020, at 12:05, Alexis King <[hidden email]> wrote:
> > type family F a b where > F a b = () -- regular (), not (() :: Constraint) (Err, sorry, this should be `F a a = ()`. But I think you can understand what I’m getting at.) _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by Richard Eisenberg-5
On Jan 6, 2020, at 05:29, Richard Eisenberg <[hidden email]> wrote:
Thanks, this all makes sense to me. I actually went back and re-read the injective type families paper after responding to your previous email, and I discovered it actually alludes to the issue we’re discussing! At the end of the paper, in section 7.3, it provides the following example:
I think what you’re describing makes a lot of sense, and it would be interesting to explore what it would take to encode into core. After thinking a little more on the topic, I think that probably makes by far the most sense from the core side of things. But I agree it seems like a significant change, and I don’t know enough about the formalism to know how difficult it would be to prove soundness. (I haven’t done much formal proving of anything!) Alexis _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by Alexis King
| In this case, in core, we receive an argument of type `F a b ~ ()`, and we
| can force that to obtain a coercion of type `F a b ~# ()`. For reasons | similar to the mechanisms behind injective type families, that equality | really does imply `a ~# b`. Ah, I see a bit better now. So you want a way to get from evidence that co1 :: F a b ~# () to evidence that co2 :: a ~# b So you'd need some coercion form like co2 = runBackwards co1 or something, where runBackwards is some kind of coercion form, like sym or trans, etc. I don't know what a design for this would look like. And even if we had it, would it pay its way, by adding substantial and useful new programming expressiveness? I now see better the connection with improvement. Currently functional dependencies and injectivity are (in GHC) used *only* to improve unification and type inference; they have zero impact on the forms of evidence. (That is a big difference between fundeps and type functions.) Maybe that could be changed, but again we'd lack a design. Simon | -----Original Message----- | From: Alexis King <[hidden email]> | Sent: 06 January 2020 18:05 | To: Simon Peyton Jones <[hidden email]> | Cc: ghc-devs <[hidden email]> | Subject: Re: Superclasses of type families returning constraints? | | > On Jan 6, 2020, at 08:52, Simon Peyton Jones <[hidden email]> | wrote: | > | > This is rejected, and it's not in the least bit puzzling! You have | evidence for (F a b) and you need to prove (a~b) -- for any a and b. | Obviously you can't. And in Core you could write (eq @Int @Bool (error | "urk")) and you jolly well don’t want it to return Refl. | | I’m not sure I totally understand your complaint. If I were to write | | eq :: a ~ b => a :~: b | eq = Refl | | then in core I could still write `eq @Int @Bool (error "urk")`, and that | would be entirely well-typed. It would not really return Refl at runtime, | of course, but neither would the example I gave in my original email. | | Perhaps a better way to phrase my original example is to write it this way: | | type family F a b where | F a b = () -- regular (), not (() :: Constraint) | | eq :: F a b ~ () => a :~: b | eq = Refl | | In this case, in core, we receive an argument of type `F a b ~ ()`, and we | can force that to obtain a coercion of type `F a b ~# ()`. For reasons | similar to the mechanisms behind injective type families, that equality | really does imply `a ~# b`. The fact that the type family returns an empty | constraint tuple is really incidental, and perhaps unnecessarily | misleading. | | Does that clear up your confusion? Or have I misunderstood your concern? | | Alexis _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
> On Jan 6, 2020, at 15:41, Simon Peyton Jones <[hidden email]> wrote:
> > Ah, I see a bit better now. So you want a way to get from evidence that > co1 :: F a b ~# () > to evidence that > co2 :: a ~# b > > So you'd need some coercion form like > co2 = runBackwards co1 > > or something, where runBackwards is some kind of coercion form, like sym or trans, etc. Precisely. I’ve begun to feel there’s something markedly GADT-like going on here. Consider this similar but slightly different example: type family F1 a where F1 () = Bool Given this definition, this function is theoretically well-typed: f1 :: F1 a -> a f1 !_ = () Since we have access to closed-world reasoning, we know that matching on a term of type `F1 a` implies `a ~ ()`. But it gets more interesting with more complicated examples: type family F2 a b where F2 () () = Bool F2 (Maybe a) a = Int These equations theoretically permit the following definitions: f2a :: F2 () b -> b f2a !_ = () f2b :: F2 (Maybe ()) b -> b f2b !_ = () That is, matching on a term of type `F2 a b` gives rise to a set of *implications.* This is sort of interesting, since we can’t currently write implications in source Haskell. Normally we avoid this problem by using GADTs, so F2 would instead be written like this: data T2 a b where T2A :: Bool -> T2 () () T2B :: Int -> T2 (Maybe a) a But these have different representations: `T2` is tagged, so if we had a value of type `T2 a ()`, we could branch on it to find out if `a` is `()` or `Maybe ()` (and if we had a `Bool` or an `Int`, for that matter). `F2`, on the other hand, is just a synonym, so we cannot do that. In this case, arguably, the right answer is “just use a GADT.” In my case, however, I cannot, because I actually want to write something like type family F2' a b where F2' () () = Void# F2' (Maybe a) a = Void# so that the term has no runtime representation at all. Even if we had `UnliftedData` (and we don’t), and even if it supported GADTs (seems unlikely), this still couldn’t be encoded using it because the term would still have to be represented by an `Int#` for the same reason `(# Void# | Void# #)` is. On the other hand, if this worked as above, `F2'` would really just be a funny-looking way of encoding a proof of a set of implications in source Haskell. > I don't know what a design for this would look like. And even if we had it, would it pay its way, by adding substantial and useful new programming expressiveness? For the latter question, I definitely have no idea! In my time writing Haskell, I have never personally found myself wanting this until now, so it may be of limited practical use. I have no idea how to express my `F2'` term in Haskell today, and I’d very much like to be able to, but of course this is not the only mechanism by which it could be expressed. Still, I find the relationship interesting, and I wonder if this particular connection between type families and GADTs is well-known. If it isn’t, I wonder whether or not it’s useful more generally. Of course, it might not be... but then maybe someone else besides me will also find it interesting, at least. :) Alexis _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Free forum by Nabble | Edit this page |