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

Fri Feb 12 23:33:02 UTC 2021

Pair kinds come with DataKinds. If you write

  data Pair a b = MkPair a b

then you get two types:

  type Pair :: Type -> Type -> Type
  type 'MkPair :: j -> k -> Pair j k

The built-in tuples work similarly, but with a bit of special syntax, and
they use punning. So

  type (,) :: Type -> Type -> Type
  type '(,) :: j -> k -> (j, k)

So, for example, the type '( 'True, Int) has kind (Bool, Type).

On Fri, Feb 12, 2021, 5:57 PM CASANOVA Juan <Juan.Casanova at ed.ac.uk> 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 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> 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
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210212/ccbf67f9/attachment.html>