<br><br><div class="gmail_quote">On Sat, Jan 14, 2012 at 12:52 AM, Simon Peyton-Jones <span dir="ltr">&lt;<a href="mailto:simonpj@microsoft.com">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">

<br>
Complexities of (Plan B)<br>
~~~~~~~~~~~~~~~~~~~~~~~~<br>
Proposal (Plan B) sounds innocent enough.  But I promise you, it isn&#39;t.<br>
There has ben some mention of the &quot;left-to-right&quot; bias of Frege type<br>
inference engine; indeed the wohle explanation of which programs are<br>
accepted and which are rejected, inherently involves an understanding<br>
of the type inference algorithm.  This is a Very Bad Thing when the<br>
type inference algorithm gets complicated, and GHC&#39;s is certainly<br>
complicated.<br>
<br>
Here&#39;s an example:<br>
<br>
   type family F a b<br>
   data instance F Int [a] = Mk { f :: Int }<br>
<br>
   g :: F Int b  -&gt; ()<br>
   h :: F a [Bool] -&gt; ()<br>
<br>
   k x = (g x, x.f, h x)<br>
<br>
Consider type inference on k.  Initially we know nothing about the<br>
type of x.<br>
 * From the application (g x) we learn that x&#39;s type has<br>
   shape (F Int &lt;something&gt;).<br>
 * From the application (h x) we learn that x&#39;s type has<br>
   shape (F &lt;something else&gt; [Bool])<br>
 * Hence x&#39;s type must be (F Int [Bool])<br>
 * And hence, using the data family we can see which field<br>
   f is intended.<br>
<br>
Notice that<br>
 a) Neither left to right nor right to left would suffice<br>
 b) There is significant interaction with type/data families<br>
    (and I can give you more examples with classes and GADTs)<br>
 c) In passing we note that it is totally unclear how (Plan A)<br>
    would deal with data families<br>
<br>
This looks like a swamp.  In a simple Hindley-Milner typed language<br>
you might get away with some informal heuristics, but Haskell is far<br>
too complicated.<br></blockquote><div><br>I rarely use Haskell&#39;s complex type machinery (and must admit to very little understanding of it). So before dismissing this as difficult to resolve in the face of a complex type system, For the complex type system I would like to figure out.<br>

* I am assuming that it is always possible to add a type annotation. Is there extra complexity to the annotation, or can we just annotate the record or top-level function?<br>* which parts of Haskell&#39;s complex type sytem will require type annotations for Frege-style records.<br>

* does using a library that uses complex machinery under the hood but tries to limit the complexity of types exposed to the user end up infecting the user&#39;s code with respect to difficulty in resolving records.<br><br>

What makes the Haskell&#39;s type system great is first and foremost typeclasses. And this is as complex as the vast majority of code gets. It doesn&#39;t sound that bad to have an implementation that works very well for the vast majority of code but requires using type annotations or normal verbose name-spacing for those few parts that are already using verbose name spacing.<br>

</div><div> </div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
 - When you have SORF, you don&#39;t really need anything else<br>
<br>
The blocking issues are described on<br>
  <a href="http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields" target="_blank">http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields</a><br>
<br>
  a) &quot;Representation hiding&quot; (look for that heading)<br>
<br>
  b) &quot;Record update&quot; (ditto), most especially for records whose<br>
     fields have polymorphic types<br>
<br>
If we fix these we can move forward.<br>
<br>
<br></blockquote><div><br>So essentially records are stalled again :(<br>I will keep trying to see if I can figure something out.<br></div></div>