<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">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="Apple-interchange-newline"><div class=""><div style="caret-color: rgb(0, 0, 0); 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; -webkit-text-stroke-width: 0px; text-decoration: none; font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; background-color: rgb(255, 255, 255);" class=""><span style="font-size: 12pt;" class="">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 style="caret-color: rgb(0, 0, 0); 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; -webkit-text-stroke-width: 0px; text-decoration: none; font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; background-color: rgb(255, 255, 255);" class=""><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 style="caret-color: rgb(0, 0, 0); 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; -webkit-text-stroke-width: 0px; text-decoration: none; font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; background-color: rgb(255, 255, 255);" class=""><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 style="caret-color: rgb(0, 0, 0); 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; -webkit-text-stroke-width: 0px; text-decoration: none; font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; background-color: rgb(255, 255, 255);" class=""><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 style="caret-color: rgb(0, 0, 0); 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; -webkit-text-stroke-width: 0px; text-decoration: none; font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; background-color: rgb(255, 255, 255);" class=""><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></body></html>