
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