A comment by user 2426021684 led me to investigate whether it was possible to come up with a type function F
such that F c1 c2 fa
demonstrates that for some f
and a
:
fa ~ f a
c1 f
c2 a
It turns out that the simplest form of this is quite easy. However, I found it rather difficult to work out how to write a poly-kinded version. Fortunately, I managed to find a way as I was writing this question.
First, some boilerplate:
Now type families to deconstruct applications at arbitrary kinds.
Now an extremely general type function, more general than necessary to answer the question. But this allows a constraint involving both components of the application.
I don't like offering constraint functions without classes to match, so here's a first-class version of
G
.It's possible to express
F
usingG
and an auxiliary class:Here are some sample uses of
F
: