Superclasses of type families returning constraints?

[Alexis King]

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

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