<div dir="ltr">Hello,<div class="gmail_extra"><br><br><div class="gmail_quote">On Sat, Oct 12, 2013 at 5:23 AM, Joachim Breitner <span dir="ltr"><<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im"><br>
> Moreover, I'm very keen to give a simple, precise answer to the question<br>
> if s is coercible to t<br>
> when is (T s) coercible to (T t)<br>
> I propose that the answer is given by precisely T's roles. At the<br>
> moment I don't see why we would want to do anything more complicated.<br>
<br>
</div>I’m not sure if „... if the roles allow it“ is any simpler than „if<br>
there is a Coercible instance for it“, and Haskell programmers might be<br>
happier if they can think in terms of type class instances without<br>
learning a new concept.<br></blockquote><div><br></div><div>I like the `deriving Coercible` idea, it seems to fit quite naturally with the rest of the language and does not require programmers to have to know about roles.</div>
<div>We'd have to be careful that we use the instances consistently though, in particular, I don't think we can just fall back to using roles behind the scenes,</div><div>because the class mechanism is more general (unles we restrict it somehow). Here are some examples:</div>
<div><br></div><div><font face="courier new, monospace">data T a = T</font></div><div><font face="courier new, monospace">deriving instance Coercible (T Int) (T Char)</font></div><div><font face="courier new, monospace">deriving instance Coercible (T Int) (T Bool)</font></div>
<div><br></div><div>This allows very precise control, but I don't think that we can express it with roles. Now consider another declaration like this:</div><div><font face="courier new, monospace"><br></font></div><div>
<font face="courier new, monospace">data S a = S (T a)deriving Coercible</font></div><div><br></div><div>Here we'd need some cleverness to determine what instances to derive. </div><div><br></div><div>Another question is: are the instances going to be automatically symmetric, or would one have to write two versions of each rule?</div>
<div>Using the previous example, would I have to also add:</div><div><br></div><div><font face="courier new, monospace">deriving instance Coercible (T Char) (T Int)</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="arial, helvetica, sans-serif">This seems a bit tedious and not in the spirit of `Coercible`. OTOH, if we were to make `Coercable` automatically symmetric,</font></div><div><font face="arial, helvetica, sans-serif">we'd have to make sure that the derived user instances are invertible. Consider for example:</font></div>
<div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="courier new, monospace">deriving instance Eq a => Coercible (T a) (T b)</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div>
<div><font face="arial, helvetica, sans-serif">This allows coercing `T Int` to `T (Int -> Int)` but not the other way.</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">All in all, I like the `deriving Coercible` notation, but I think that we should restrict it to something that essentially matches the `role` mechanism under the hood (and get an error saying that we can't derive the instance otherwise).</font></div>
<div><font face="arial, helvetica, sans-serif">Here is a stab at the rules:<br> * The head of the instance must be of the form: Coercible (T a1 a2 ...) (T b1 b2 ...), where `T` is a concrete type, and the `as` and `bs` are variables.</font></div>
<div><font face="arial, helvetica, sans-serif"> * The only constraints in the context may be of the form `Coercible a1 b1`, or `Coercible a2 b2`, etc...</font></div><div><font face="arial, helvetica, sans-serif"> * There can be only one instance derived per type `T`</font></div>
<div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">With these restrictions we essentially have another way to specify the roles. The role of the Nts parameter of `T` can be determined like this:</font></div>
<div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="courier new, monospace">role aN bN</font></div><div><font face="courier new, monospace"> | aN == bN = Nominal</font></div><div><font face="courier new, monospace"> | otherwise = if context has Coercible aN bN then Representational else Phantom</font></div>
<div><br></div><div>Hope this helps,</div><div>-Iavor</div><div><br></div><div><br></div><div><br></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif"><br></font></div>
<div><font face="courier new, monospace"><br></font></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div> </div><div><br></div><div><br></div>
<div> </div></div></div></div>