<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
Thanks Richard,<br>
<br>
I'll try to stay as short as possible.<br>
<br>
"Did you try using the normal pair constructor?"<br>
<br>
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).<br>
<br>
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!<br>
<br>
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,
<b>and I try to keep type synonyms as high-kinded as possible<i>. </i></b>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.<br>
<br>
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.<br>
<br>
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.<br>
<br>
Thanks again.<br>
Juan.<br>
<br>
<br>
<br>
<br>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Richard Eisenberg <rae@richarde.dev><br>
<b>Sent:</b> 12 February 2021 20:04<br>
<b>To:</b> CASANOVA Juan <Juan.Casanova@ed.ac.uk><br>
<b>Cc:</b> haskell-cafe@haskell.org <haskell-cafe@haskell.org><br>
<b>Subject:</b> Re: [Haskell-cafe] Kind pairs and kind currying/uncurrying</font>
<div> </div>
</div>
<div class="" style="word-wrap:break-word; line-break:after-white-space">
<div style="background-color:#fff2e6; border:2px dotted #ff884d"><span style="font-size:12pt; font-family:sans-serif; color:black; font-weight:bold; padding:.2em">This email was sent to you by someone outside the University.</span>
<div style="font-size:10pt; font-family:sans-serif; font-style:normal; padding:.2em">
You should only click on links or attachments if you are certain that the email is genuine and the content is safe.</div>
</div>
<div>Hi Juan,
<div class=""><br class="">
</div>
<div class=""><br class="">
<div><br class="">
<blockquote type="cite" class="">
<div class="">On Feb 12, 2021, at 1:50 PM, CASANOVA Juan <<a href="mailto:Juan.Casanova@ed.ac.uk" class="">Juan.Casanova@ed.ac.uk</a>> wrote:</div>
<br class="x_Apple-interchange-newline">
<div class="">
<div class="" style="font-style:normal; font-variant-caps:normal; font-weight:normal; letter-spacing:normal; text-align:start; text-indent:0px; text-transform:none; white-space:normal; word-spacing:0px; text-decoration:none; font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; background-color:rgb(255,255,255)">
<span class="" style="font-size:12pt">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:</span></div>
</div>
</blockquote>
<blockquote type="cite" class="">
<div class="">
<div class="" style="font-style:normal; font-variant-caps:normal; font-weight:normal; letter-spacing:normal; text-align:start; text-indent:0px; text-transform:none; white-space:normal; word-spacing:0px; text-decoration:none; font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; background-color:rgb(255,255,255)">
<div class=""><br class="">
type KindPair (a :: ka) (b :: kb) (f :: ka -> kb -> *) = f a b<br class="">
</div>
</div>
</div>
</blockquote>
<div><br class="">
</div>
<div>Did you try using the normal pair constructor?</div>
<div><br class="">
</div>
<div>> type KindPair a b = '(a, b)</div>
<div><br class="">
</div>
<div>That would seem to meet your needs, but perhaps I'm missing something.</div>
<blockquote type="cite" class="">
<div class="">
<div class="" style="font-style:normal; font-variant-caps:normal; font-weight:normal; letter-spacing:normal; text-align:start; text-indent:0px; text-transform:none; white-space:normal; word-spacing:0px; text-decoration:none; font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; background-color:rgb(255,255,255)">
<div class=""><br class="">
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.<br class="">
</div>
</div>
</div>
</blockquote>
<div><br class="">
</div>
<div>Partial application of type synonyms is <i class="">not</i> 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.</div>
<div><br class="">
</div>
<blockquote type="cite" class="">
<div class="">
<div class="" style="font-style:normal; font-variant-caps:normal; font-weight:normal; letter-spacing:normal; text-align:start; text-indent:0px; text-transform:none; white-space:normal; word-spacing:0px; text-decoration:none; font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; background-color:rgb(255,255,255)">
<div class="">
<div class="">type KCurry (tf :: (KindPair ka kb) -> kc) = ka -> kb -> kc</div>
<div class="">type KUncurry (tf :: ka -> kb -> kc) = (KindPair ka kb) -> kc</div>
</div>
</div>
</div>
</blockquote>
<div><br class="">
</div>
<div>My definitions of these look like this:</div>
<div><br class="">
</div>
<div>
<div></div>
<blockquote type="cite" class="">
<div>type Curry :: ((a, b) -> c) -> a -> b -> c</div>
<div>type Curry f x y = f '(x, y)</div>
<div><br class="">
</div>
<div>type Uncurry :: (a -> b -> c) -> (a, b) -> c</div>
<div>type family Uncurry f xy where</div>
<div> Uncurry f '(x, y) = f x y</div>
</blockquote>
<div class=""><br class="">
</div>
<div class="">where I've also used -XStandaloneKindSignatures (in GHC 8.10 and up), but you don't need to.</div>
<div class=""><br class="">
</div>
<div class="">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.</div>
</div>
<br class="">
<blockquote type="cite" class="">
<div class="">
<div class="" style="font-style:normal; font-variant-caps:normal; font-weight:normal; letter-spacing:normal; text-align:start; text-indent:0px; text-transform:none; white-space:normal; word-spacing:0px; text-decoration:none; font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; background-color:rgb(255,255,255)">
<div class=""><br class="">
</div>
<div class="">Is what I am trying to do completely absurd? I do not think it is, but maybe I am being naive?<br class="">
</div>
</div>
</div>
</blockquote>
<div><br class="">
</div>
<div>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.</div>
</div>
<br class="">
</div>
<div class="">I hope this helps!</div>
<div class="">Richard</div>
</div>
</div>
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
</body>
</html>