[Haskell-cafe] Kind pairs and kind currying/uncurrying

[CASANOVA Juan]

Hello again,

At this point, I think what I am trying to do is simply not possible in Haskell, not even with as many extensions as I would want. Perhaps with template Haskell, but that's ground that I am still afraid to tread. But I thought I would ask anyway.

(All the code in the rest of the email assumes as many extensions as GHC asks me to compile).

The background is more complicated and controversial than the question itself, but I'll give a little bit of it so that you know why I'm trying to do this.

I am trying to define a type class that takes other type classes as arguments. That is fairly straightforward by itself. A single parameter type-class has kind

(k -> Constraint).

So I can write my class

SecondOrderClass (cl :: k -> Constraint)

The problem, however, is that I want to use this class for multi-parameter type classes as well. A two parameter type class has kind

(k1 -> k2 -> Constraint)

The most general unifier of these two kinds is, unfortunately, a free kind (k), which thus includes kinds that are not type classes (like types). Therefore, it is not possible to directly specify a class that takes as parameter a type class with any number of arguments.

So, thus I thought: I've seen this before. This is currying and uncurrying. Except I'm doing it with kinds except of with types. A brief search didn't yield me any library that would do this. So I thought: This should be fairly easy to do by myself if I throw enough extensions at it.

Well, I failed. I tried two variations and neither worked. To be clear, what I tried to do is to

  *   Define a type synonym that would produce a kind representing a pair of two given kinds.
  *   Define type synonyms for currying and uncurrying kinds using the pair kind.

The first variation I tried I feel is the most semantically accurate, as it is clear from the beginning of what I am trying to do. The main "insight" I used was using/assuming extensionality of kinds (and partial application of type synonyms) to define a kind pair:

type KindPair (a :: ka) (b :: kb) (f :: ka -> kb -> *) = f a b

A pair of kinds is simply anything that "owes the two kinds to the type checker". Thus, if given anything expecting those two kinds, it would feed them to it. This by itself compiles fine. But then when trying to define currying and uncurrying, it won't type check:

type KCurry (tf :: (KindPair ka kb) -> kc) (ta :: ka) (tb :: kb) = kc
type KUncurry (tf :: ka -> kb -> kc) (tp :: (KindPair ka kb)) = kc

The error I get is: The type synonym ‘KindPair’ should have 3 arguments, but has been given 2

Partial application of type synonyms is fine, I use it all the time. But it seems it is not fine when it is "kind synonyms"??? It is not even asking me for any extension to allow it.

So I tried a more syntactic approach, abusing the notion that GHC treats kinds and types very similarly:

type KindPair (a :: ka) (b :: kb) = ((ka -> kb -> *) -> *)

type KCurry (tf :: (KindPair ka kb) -> kc) = ka -> kb -> kc
type KUncurry (tf :: ka -> kb -> kc) = (KindPair ka kb) -> kc

This type checks, but it is just a mirage. If you check the kinds of KCurry and KUncurry it does not look good:

(KindPair ka kb -> kc) -> *

Uhh... that's not what I said. It's taking the right hand side entirely as a type, not as a kind.

This becomes obvious when we try to use them:

ftest :: KCurry (KUncurry (,)) Int Int -> (Int, Int)

This does not type check, regardless of the definition (ideally ftest = id would work, but we do not even get that far).

The error is:

Expected kind ‘* -> * -> *’, but ‘KCurry (KUncurry (,))’ has kind ‘*’

So, my question is: Is what I am trying to do possible in Haskell?

Is what I am trying to do completely absurd? I do not think it is, but maybe I am being naive?

Thanks in advance, and sorry for the long email (again). I tried to be as straight to the point as possible.
Juan.
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210212/b278f3d9/attachment.html>