
<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Dec 30, 2019, at 11:16 AM, Alexis King <<a href="mailto:lexi.lambda@gmail.com" class="">lexi.lambda@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><span style="caret-color: rgb(0, 0, 0); font-family: Menlo-Regular; font-size: 11px; 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; float: none; display: inline !important;" class="">I don’t know if there is a way to encode those using the constraint language available in source Haskell today.</span></div></blockquote></div><br class=""><div class="">I gave it a good try, but failed. The trick I was hoping to leverage was *partial improvement*. Here is an example of partial improvement:</div><div class=""><br class=""></div><div class="">> class FD1 a b | a -> b</div><div class="">> class FD2 a b | a -> b</div><div class="">></div><div class="">> instance FD1 a b => FD2 (Maybe a) (Maybe b)</div><div class="">></div><div class="">> f :: FD2 a b => a -> b</div><div class="">> f = undefined</div><div class="">></div><div class="">> x = f (Just True)</div><div class=""><br class=""></div><div class="">This program will require solving [W] FD2 (Maybe Bool) beta, where the [W] indicates that we have a "wanted" constraint (a goal we are trying to satisfy) and beta is a unification variable. GHC can figure out from the fundep on FD2 that the only FD2 instance that can apply is the one we see above. It thus knows that beta must be Maybe beta2 (for some fresh beta2). This is the essence of partial improvement, when we solve one unification variable with an expression involving another (but is more informative somehow).</div><div class=""><br class=""></div><div class="">I thought that, maybe, we could use partial improvement to give you what you want, by replacing the RHSs of the type family with expressions involving classes with fundeps. (Injective type families work very analogously, but it's not worthwhile showing the translation of this idea to that domain here.) I couldn't quite get it to work out, though. Maybe you can, armed with this description... but I doubt it. The problem is that partial improvement must always be a shadow of some "total" improvement process. In the example above, note that I haven't written down an instance of FD1. Clearly, we'll need to satisfy the FD1 constraint in order to satisfy the FD2 constraint. The problem is that, in your example, we really only want partial improvement... and I don't think there's a way to state that. What's tantalizing is that GHC already does all this partial improvement stuff -- it's just that we can't seem to write the instance declarations the way we want to satisfy your use case.</div><div class=""><br class=""></div><div class="">I don't know if this really moves us forward at all, but maybe a description of my failure can lead to someone's success. Or perhaps it will lead to a language improvement that will allow us to express what you want.</div><div class=""><br class=""></div><div class="">Richard</div></body></html>