<div dir="ltr">Hello,<div><br></div><div style>The general functionality for this seems useful, but we should be careful exactly what types we allow in the &#39;newtype wrap/unwrap&#39; declarations.  For example, would we allow something like this:</div>
<div style><br></div><div style>newtype wrap cvt :: f a -&gt; f (Dual a)</div><div style><br></div><div style>If we just worry about what&#39;s in scope, then it should be accepted, however this function could still be used to break the invariant on `Set` because it is polymorphic.</div>
<div style><br></div><div style><br></div><div style>In general, I was never comfortable with GHC&#39;s choice to add an axiom equating a newtype and its representation type, because it looks unsound to me (without any type-functions or newtype deriving).</div>
<div style>For example, consider:</div><div style><br></div><div style>newtype T a = MkT Int</div><div style><br></div><div style>Now, if this generates an axiom asserting that `froall a. T a ~ Int`, then we can derive a contradiction:</div>
<div style><br></div><div style>T Int ~ Int ~ T Char, and hence `Int ~ Char`.</div><div style><br></div><div style>It looks like what we need is a different concept: one that talks about the equality of the representations of types, rather then equality of the types themselves.</div>
<div style><br></div><div style>-Iavor</div><div style><br></div><div style><br></div><div style><br></div><div style><br></div><div style><br></div><div style><br></div><div style><br></div><div style><br></div><div style>
<br></div><div style><br></div><div style><br></div><div style><br></div><div style><br></div><div style><br></div><div style><br></div><div style><br></div><div style><br></div><div style><br></div></div><div class="gmail_extra">
<br><br><div class="gmail_quote">On Mon, Jan 14, 2013 at 10:09 AM, Simon Peyton-Jones <span dir="ltr">&lt;<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">






<div lang="EN-GB" link="blue" vlink="purple">
<div>
<p class="MsoNormal"><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;">Friends<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;">I’d like to propose a way to “promote” newtypes over their enclosing type.  Here’s the writeup<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;">          <a href="http://hackage.haskell.org/trac/ghc/wiki/NewtypeWrappers" target="_blank">
http://hackage.haskell.org/trac/ghc/wiki/NewtypeWrappers</a><u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;">Any comments?  Below is the problem statement, taken from the above page.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;">I’d appreciate<u></u><u></u></span></p>
<p><u></u><span style="font-family:Symbol"><span>·<span style="font:7.0pt &quot;Times New Roman&quot;">        
</span></span></span><u></u><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;">A sense of whether you care. Does this matter?<u></u><u></u></span></p>
<p><u></u><span style="font-family:Symbol"><span>·<span style="font:7.0pt &quot;Times New Roman&quot;">        
</span></span></span><u></u><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;">Improvements to the design I propose<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;">Simon<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;"><u></u> <u></u></span></p>
<p class="MsoNormal"><b><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;">The problem<u></u><u></u></span></b></p>
<p>Suppose we have <u></u><u></u></p>
<pre>newtype Age = MkAge Int<u></u><u></u></pre>
<p>Then if <tt><span style="font-size:10.0pt">n :: Int</span></tt>, we can convert
<tt><span style="font-size:10.0pt">n</span></tt> to an <tt><span style="font-size:10.0pt">Age</span></tt> thus:
<tt><span style="font-size:10.0pt">MkAge n :: Age</span></tt>. Moreover, this conversion is a type conversion only, and involves no runtime instructions whatsoever. This cost model -- that newtypes are free -- is important to Haskell programmers, and encourages
 them to use newtypes freely to express type distinctions without introducing runtime overhead.
<u></u><u></u></p>
<p>Alas, the newtype cost model breaks down when we involve other data structures. Suppose we have these declarations
<u></u><u></u></p>
<pre>data T a   = TLeaf a     | TNode (Tree a) (Tree a)<u></u><u></u></pre>
<pre>data S m a = SLeaf (m a) | SNode (S m a) (S m a)<u></u><u></u></pre>
<p>and we have these variables in scope <u></u><u></u></p>
<pre>x1 :: [Int]<u></u><u></u></pre>
<pre>x2 :: Char -&gt; Int<u></u><u></u></pre>
<pre>x3 :: T Int<u></u><u></u></pre>
<pre>x4 :: S IO Int<u></u><u></u></pre>
<p>Can we convert these into the corresponding forms where the <tt><span style="font-size:10.0pt">Int</span></tt> is replaced by
<tt><span style="font-size:10.0pt">Age</span></tt>? Alas, not easily, and certainly not without overhead.
<u></u><u></u></p>
<ul type="disc">
<li class="MsoNormal">
For <tt><span style="font-size:10.0pt">x1</span></tt> we can write <tt><span style="font-size:10.0pt">map MkAge x1 :: [Age]</span></tt>. But this does not follow the newtype cost model: there will be runtime overhead from executing the
<tt><span style="font-size:10.0pt">map</span></tt> at runtime, and sharing will be lost too. Could GHC optimise the
<tt><span style="font-size:10.0pt">map</span></tt> somehow? This is hard; apart from anything else, how would GHC know that
<tt><span style="font-size:10.0pt">map</span></tt> was special? And it it gets worse.
<u></u><u></u></li></ul>
<ul type="disc">
<li class="MsoNormal">
For <tt><span style="font-size:10.0pt">x2</span></tt> we&#39;d have to eta-expand: <tt>
<span style="font-size:10.0pt">(\y -&gt; MkAge (x2 y)) :: Char -&gt; Age</span></tt>. But this isn&#39;t good either, because eta exapansion isn&#39;t semantically valid (if
<tt><span style="font-size:10.0pt">x2</span></tt> was bottom, <tt><span style="font-size:10.0pt">seq</span></tt> could distinguish the two). See
<a href="http://hackage.haskell.org/trac/ghc/ticket/7542" title="bug: GHC doesn&#39;t optimize (strict) composition with id (new)" target="_blank">
#7542</a> for a real life example. <u></u><u></u></li></ul>
<ul type="disc">
<li class="MsoNormal">
For <tt><span style="font-size:10.0pt">x3</span></tt>, we&#39;d have to map over <tt>
<span style="font-size:10.0pt">T</span></tt>, thus <tt><span style="font-size:10.0pt">mapT MkAge x3</span></tt>. But what if
<tt><span style="font-size:10.0pt">mapT</span></tt> didn&#39;t exist? We&#39;d have to make it. And not all data types have maps.
<tt><span style="font-size:10.0pt">S</span></tt> is a harder one: you could only map over S-values if
<tt><span style="font-size:10.0pt">m</span></tt> was a functor. There&#39;s a lot of discussion abou this on
<a href="http://hackage.haskell.org/trac/ghc/ticket/2110" title="feature request: Rules to eliminate casted id&#39;s (new)" target="_blank">
#2110</a>. <u></u><u></u></li></ul>
<p class="MsoNormal"><span style="font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;"><u></u> <u></u></span></p>
</div>
</div>

<br>_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><br>
<br></blockquote></div><br></div>