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 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.

On Jan 4, 2020, at 20:38, Richard Eisenberg 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

On Jan 6, 2020, at 05:29, Richard Eisenberg wrote:

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.

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:

Could closed type families move beyond injectivity and functional dependencies by applying closed-world reasoning that derives solutions of arbitrary equalities, provided a unique solution exists? Consider this example:

type family J a where J Int = Char J Bool = Char J Double = Float

One might reasonably expect that if we wish to prove (J a ∼ Float), we will simplify to (a ∼ Double). Yet GHC does not do this as neither injectivity nor functional dependencies can discover this solution.

This is not quite the same as what we’re talking about here, but it’s clearly in the same ballpark. 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

On Jan 6, 2020, at 2:52 PM, Simon Peyton Jones via ghc-devs wrote:

| 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.

But how could you possibly have evidence for (F a b) without (a ~ b)? 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.

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

On Jan 6, 2020, at 12:05, Alexis King 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.)

On Jan 6, 2020, at 15:41, Simon Peyton Jones 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