Superclasses of type families returning constraints?
lexi.lambda at gmail.com
Sun Jan 12 03:54:32 UTC 2020
> On Jan 6, 2020, at 15:41, Simon Peyton Jones <simonpj at microsoft.com> 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.
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. :)
More information about the ghc-devs