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 Sent: 12 February 2021 20:04 To: CASANOVA Juan Cc: haskell-cafe@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 mailto:Juan.Casanova@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.

On Feb 12, 2021, at 5:57 PM, CASANOVA Juan wrote:

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 wouldn't call it a kind pair. I think of '(..., ...) just as the normal pair constructor, but used in a type. The reason for the ' is to disambiguate it with (..., ...), which is the type of pairs. It might be helpful to see the kinds of these constructions: '(,) :: forall a b. a -> b -> (a, b) (,) :: Type -> Type -> Type

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!

I'm not surprised this information is hard to find. On the one hand, I think the Haskell community (myself included) does a mediocre job of clarifying these sorts of things. On the other, '(,) isn't a special case at all: it behaves in an exactly analogous manner to using any other constructor in a type. (For what it's worth, I don't have a good name for this idea, beyond "the pair constructor used in a type".)

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.

I agree completely that `type List = []` is better than `type List a = [a]`, because the former allows List to be used on its own; the latter would require the argument at all usage sites. It seems you understand this. (Small pointer: I didn't at first understand your meaning from "as high-kinded as possible". I would say "as eta-reduced as possible", but that's perhaps even more opaque if you don't know the term.)

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.

The problem is that, for Uncurry, we need to pattern-match on a pair. Pattern-matching requires a type family. Type families are not particularly hard to work with, though: think of them simply as functions written in types. The only "gotcha" is that they always must be saturated.

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.

Glad to be of service! Richard

Thanks again. Juan.

From: Richard Eisenberg mailto:rae@richarde.dev> Sent: 12 February 2021 20:04 To: CASANOVA Juan mailto:Juan.Casanova@ed.ac.uk> Cc: haskell-cafe@haskell.org mailto:haskell-cafe@haskell.org mailto:haskell-cafe@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 mailto:Juan.Casanova@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._______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.