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

[Richard Eisenberg]

Hi Juan,



> On Feb 12, 2021, at 1:50 PM, CASANOVA Juan <Juan.Casanova at ed.ac.uk> wrote:
> 
> 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

Did you try using the normal pair constructor?

> type KindPair a b = '(a, b)

That would seem to meet your needs, but perhaps I'm missing something.
> 
> 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.

Partial application of type synonyms is not fine. Try it out. (GHC does allow this in the definition of other type synonyms, as long as it works out in the end. But it won't work in e.g. type signatures.) I think this is the crux of the problem.

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

My definitions of these look like this:

> type Curry :: ((a, b) -> c) -> a -> b -> c
> type Curry f x y = f '(x, y)
> 
> type Uncurry :: (a -> b -> c) -> (a, b) -> c
> type family Uncurry f xy where
>   Uncurry f '(x, y) = f x y

where I've also used -XStandaloneKindSignatures (in GHC 8.10 and up), but you don't need to.

I think part of the problem is that your definitions appear "one level off", unless I'm misunderstanding: you're giving the kind of the result you want, not the actual result you want.

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

No, not absurd. I do think that currying/uncurrying in types is problematic because of the saturation condition on type synonyms and type families. But my guess is that there is a way of addressing your root problem, with class constraints, but I'd need more information to suggest a concrete next step.

I hope this helps!
Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210212/f7621dda/attachment.html>