<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 12 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Verdana;
panose-1:2 11 6 4 3 5 4 4 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri","sans-serif";}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
p.MsoPlainText, li.MsoPlainText, div.MsoPlainText
{mso-style-priority:99;
mso-style-link:"Plain Text Char";
margin:0cm;
margin-bottom:.0001pt;
font-size:10.0pt;
font-family:"Verdana","sans-serif";}
span.PlainTextChar
{mso-style-name:"Plain Text Char";
mso-style-priority:99;
mso-style-link:"Plain Text";
font-family:"Verdana","sans-serif";}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 90.0pt 72.0pt 89.95pt;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:984889404;
mso-list-type:hybrid;
mso-list-template-ids:212640852 134807553 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
ol
{margin-bottom:0cm;}
ul
{margin-bottom:0cm;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-GB" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoPlainText">Joachim<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">Discussing with Richard Eisenberg, we wondered the following.<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText" style="margin-left:36.0pt;text-indent:-18.0pt;mso-list:l0 level1 lfo1">
<![if !supportLists]><span style="font-family:Symbol"><span style="mso-list:Ignore">·<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]>note that the “seq” nonsense is because we allow user-defined NT-values<o:p></o:p></p>
<p class="MsoPlainText" style="margin-left:36.0pt;text-indent:-18.0pt;mso-list:l0 level1 lfo1">
<![if !supportLists]><span style="font-family:Symbol"><span style="mso-list:Ignore">·<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]>also note that to determine which NT values we can derive from in-scope NT values, we have to do something very similar to type-class solving. Eg. need NT [T] [S], have available ntList :: forall ab. NT a b -> NT [a] [b], so
use ntList to simplify NT [T] [S] to NT T S.<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">Hence the following suggestion: revert from NT as a data value to NT as a class. Thus<o:p></o:p></p>
<p class="MsoPlainText"> class NT a b where<o:p></o:p></p>
<p class="MsoPlainText"> castNT :: a -> b<o:p></o:p></p>
<p class="MsoPlainText"> uncastNT :: b -> a<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">Now when you have a data type you can say “deriving( NT )”, or things like<o:p></o:p></p>
<p class="MsoPlainText"> deriving NT a b => NT [a] [b]<o:p></o:p></p>
<p class="MsoPlainText">and expect the usual type-class deriving mechanism to do the job.<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">As usual, you can only do this if you can see the data constructor of the relevant type.<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">Now, you can say things like<o:p></o:p></p>
<p class="MsoPlainText"> newtype Age = MkAge Int<o:p></o:p></p>
<p class="MsoPlainText"> f :: [Age] -> Int<o:p></o:p></p>
<p class="MsoPlainText"> f xs = sum (uncastNT xs)<o:p></o:p></p>
<p class="MsoPlainText">and it’ll work fine. If you omitted the type annotation on f you’d get something like<o:p></o:p></p>
<p class="MsoPlainText"> f :: (Num a, NT [a] b) => b -> a<o:p></o:p></p>
<p class="MsoPlainText">which is probably OK.<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">You might worry that instances are not scopeable. Quite right. If you make an NT instance, *<b>everyone</b>* can see it. So don’t make a type an instance of NT unless that’s want. This is not terrible; it just means that you can’t
make *<b>local</b>* NT instances, just as you can’t make local Eq instances.<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">This seems to involve a lot less special pleading than before, while still allowing the control you need. For example, for Map you might say<o:p></o:p></p>
<p class="MsoPlainText"> deriving instance NT a b => NT (Map k a) (Map k b)<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">The *<b>derived</b>* NT instances would be implemented, just as now, with lifted coercions.<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">You cannot write your own NT instance, just as you can’t write your own Typable instance. That means we don’t need to worry about those bogus instances.<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">Does that make sense?<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">Simon<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">| <span lang="EN-US">-----Original Message-----</span></p>
<p class="MsoPlainText">| <span lang="EN-US">From: ghc-devs-bounces@haskell.org [mailto:ghc-devs-bounces@haskell.org] On</span></p>
<p class="MsoPlainText">| <span lang="EN-US">Behalf Of Joachim Breitner</span></p>
<p class="MsoPlainText">| <span lang="EN-US">Sent: 11 July 2013 09:41</span></p>
<p class="MsoPlainText">| <span lang="EN-US">To: ghc-devs@haskell.org</span></p>
<p class="MsoPlainText">| <span lang="EN-US">Subject: Re: Exposing newtype coercions to Haskell</span></p>
<p class="MsoPlainText">| </p>
<p class="MsoPlainText">| Hi,</p>
<p class="MsoPlainText">| </p>
<p class="MsoPlainText">| Am Montag, den 08.07.2013, 09:39 +0000 schrieb Simon Peyton-Jones:</p>
<p class="MsoPlainText">| > | > If you CAN do that, then it's ok (internally) to use ordinary</p>
<p class="MsoPlainText">| > | > coercion lifting, roughly</p>
<p class="MsoPlainText">| > | > ntT g = T g refl</p>
<p class="MsoPlainText">| > | > The above per-constructor-arg testing is just to make sure that</p>
<p class="MsoPlainText">| > | > all the relevant witnesses are in scope, to preserve abstraction.</p>
<p class="MsoPlainText">| > | > It's not for soundness.</p>
<p class="MsoPlainText">| > |</p>
<p class="MsoPlainText">| > | I understand the approach, but I think it is insufficient. Assume</p>
<p class="MsoPlainText">| > | that the user wants to cheat for some reason and has this definition</p>
<p class="MsoPlainText">| > | for ntS, clearly writable without having access to S’s internals:</p>
<p class="MsoPlainText">| > |</p>
<p class="MsoPlainText">| > | ntS :: NT p p' -> NT q q' -> NT (S p q) (S p' q') ntS _ _ = error</p>
<p class="MsoPlainText">| > | "nah nah"</p>
<p class="MsoPlainText">| ></p>
<p class="MsoPlainText">| > Quite right! My mistake was to say "if you CAN do that..." and then</p>
<p class="MsoPlainText">| > discard the evidence that you can do it. What I should have said is</p>
<p class="MsoPlainText">| ></p>
<p class="MsoPlainText">| > * prove a large bunch of NT constraints (one per constructor</p>
<p class="MsoPlainText">| > field)</p>
<p class="MsoPlainText">| > * then `seq` them</p>
<p class="MsoPlainText">| > * before returning the "ordinary coercion lifting" result.</p>
<p class="MsoPlainText">| ></p>
<p class="MsoPlainText">| > The thing is, that the "ordinary coercion lifting" is sound (roles</p>
<p class="MsoPlainText">| > permitting -- should check that right off the bat). But we are making</p>
<p class="MsoPlainText">| > a stronger check here, namely that the programmer has exported enough</p>
<p class="MsoPlainText">| > evidence, to expose abstractions.</p>
<p class="MsoPlainText">| </p>
<p class="MsoPlainText">| </p>
<p class="MsoPlainText">| Although it feels a bit weird to force one set of coercion witnesses (based on</p>
<p class="MsoPlainText">| datacon field types) and then use another (based on typecon parameters), it could</p>
<p class="MsoPlainText">| have worked, so I did more work in that direction, but I have hit another obstacle:</p>
<p class="MsoPlainText">| </p>
<p class="MsoPlainText">| Just to clarify that we talk about the same things, an easy case:</p>
<p class="MsoPlainText">| data Family a = Family a a (List a)</p>
<p class="MsoPlainText">| deriving familyNT :: NT a b -> NT (Family a) (Family b) with "listNT :: NT a</p>
<p class="MsoPlainText">| b -> NT (List a) (List b)" in scope would get this</p>
<p class="MsoPlainText">| implementation:</p>
<p class="MsoPlainText">| familyNT nt = nt `seq` nt `seq` listNT nt `seq`</p>
<p class="MsoPlainText">| case nt of (NT co -> NT (Family co)) This does ensure that, without</p>
<p class="MsoPlainText">| breaking abstractions, the user is allowed to convert the arguments of the datacon</p>
<p class="MsoPlainText">| and produces a sound coercion in in the F_C sense.</p>
<p class="MsoPlainText">| </p>
<p class="MsoPlainText">| But what about a simple tree type?</p>
<p class="MsoPlainText">| data Tree a = Tree a (List (Tree a))</p>
<p class="MsoPlainText">| deriving treeNT :: NT a b -> NT (Tree a) (Tree b) I need to force witnesses</p>
<p class="MsoPlainText">| for</p>
<p class="MsoPlainText">| * (NT a b) (easy, that is the first argument) and for</p>
<p class="MsoPlainText">| * (NT (List (Tree a)) (NT (List (Tree b)).</p>
<p class="MsoPlainText">| The only way to obtain such a witness is to use listNT, which</p>
<p class="MsoPlainText">| would strictly(!) expect a value of type NT (Tree a) (Tree b),</p>
<p class="MsoPlainText">| which is what I am trying to produce at the moment, so I cannot</p>
<p class="MsoPlainText">| simply call treeNT.</p>
<p class="MsoPlainText">| </p>
<p class="MsoPlainText">| In this case I can work around it by first creating the final NT value and then use it</p>
<p class="MsoPlainText">| to create and seq the witnesses required, before returning the result:</p>
<p class="MsoPlainText">| treeNT nt = let resNT = case nt of (NT co -> NT (Tree co))</p>
<p class="MsoPlainText">| in nt `seq` listNT resNT `seq` resNT but this is becoming more and</p>
<p class="MsoPlainText">| more hacky and inelegant. For example, with mutually recursive data types, I’d</p>
<p class="MsoPlainText">| have to detect that they are mutually recursive and create similar witnesses in</p>
<p class="MsoPlainText">| advance for all involved types; for nested recursion I’d have to create multiple</p>
<p class="MsoPlainText">| witnesses, and who knows what else can happen.</p>
<p class="MsoPlainText">| </p>
<p class="MsoPlainText">| </p>
<p class="MsoPlainText">| From a logical point of view, I’d expect the coercion lifting for a recursive data type</p>
<p class="MsoPlainText">| to have a type like</p>
<p class="MsoPlainText">| a ~/C b -> (forall ta tb. (ta ~/C tb -> List ta ~/C List tb)) -> Tree a ~/C</p>
<p class="MsoPlainText">| Tree b (justified by writing the data type as a fixed point and thinking about fixed-</p>
<p class="MsoPlainText">| point induction), but its soundness breaks down immediately as the function type</p>
<p class="MsoPlainText">| -> in the second argument is not total.</p>
<p class="MsoPlainText">| </p>
<p class="MsoPlainText">| </p>
<p class="MsoPlainText">| </p>
<p class="MsoPlainText">| That’s it for now,</p>
<p class="MsoPlainText">| Joachim</p>
<p class="MsoPlainText">| </p>
<p class="MsoPlainText">| --</p>
<p class="MsoPlainText">| Joachim “nomeata” Breitner</p>
<p class="MsoPlainText">| mail@joachim-breitner.de • http://www.joachim-breitner.de/</p>
<p class="MsoPlainText">| Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C</p>
<p class="MsoPlainText">| Debian Developer: nomeata@debian.org</p>
</div>
</body>
</html>