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

[CASANOVA Juan]

Thanks Richard,

I'll try to stay as short as possible.

"Did you try using the normal pair constructor?"

No, I didn't. I didn't even know it existed. I think now I've seen it before. This is a kind pair, which is different from a pair type, is this correct? So, what I am saying, the ' in the front relevantly changes what it means for the type checker. It's not as simple as using a tuple type (I'm pretty sure I even tried this and the type checker looked at me in confusion).

I must complain, though, that I've looked for "kind pair Haskell", "type pair Haskell", "multiple kinds Haskell", "tuple kinds Haskell" and "kind tuples Haskell", and found zero references to this particular construct, so I can't really feel like it's my fault for not knowing about it!

About partial application, you are absolutely right, and I actually knew this, but it sort of went out of my mind when I wrote that. The way that I tend to write Haskell, I do use partial type synonyms quite a bit, and I try to keep type synonyms as high-kinded as possible. That is why I forgot about this. So instead of type List a = [a], it's better to use type List = [] because then you can do a lot more with it. But this is besides the point.

The reasons your solution seems to work and mine doesn't are both the kind pair construct, and the usage of a type family. I've looked into type families before, but never used them in practice, mostly because they didn't actually allow me to do what I looked them up for. This might be the first time that type families are actually the answer for me. I'm still a bit scared of them and not understanding what you can / cannot do with them. This relates to "giving the kind of the result I want": Without type families you cannot do any sort of "computation" at the type level, just syntactic things. I thought this would be enough for Curry / Uncurry, but it obviously isn't.

In practice, however, this was me trying to save myself some work by implementing a high-level solution that I could reuse several times. When I failed, I wrote the email to try and learn from it, but then moved forward with implementing it in a more mundane way (but more redundant). At this point, I think I'm going to keep going with this implementation. I even think I would not have gotten so much from the curry / uncurry now that I think back. But this was definitely very instructive.

Thanks again.
Juan.




________________________________
From: Richard Eisenberg <rae at richarde.dev>
Sent: 12 February 2021 20:04
To: CASANOVA Juan <Juan.Casanova at ed.ac.uk>
Cc: haskell-cafe at haskell.org <haskell-cafe at haskell.org>
Subject: Re: [Haskell-cafe] Kind pairs and kind currying/uncurrying

This email was sent to you by someone outside the University.
You should only click on links or attachments if you are certain that the email is genuine and the content is safe.
Hi Juan,



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