<br><br><div class="gmail_quote">On Thu, Jul 1, 2010 at 7:54 PM, 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="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br><div class="im">
|  Also, what is the difference between fundeps and type families<br>
|  wrt local type constraints? I had always assumed them to be<br>
|  equivalent, if fully implemented. Similar to logic vs functional<br>
|  programming, where Haskellers tend to find the latter more<br>
|  convenient. Functional logic programming shows that there<br>
|  are some tricks missing if one just drops the logic part.<br>
<br>
</div>Until now, no one has know how to combine fundeps and local constraints.  For example<br>
<div class="im"><br>
  class C a b | a-&gt;b where<br>
    op :: a -&gt; b<br>
<br>
</div><div class="im">  instance C Int Bool where<br>
</div>    op n = n&gt;0<br>
<br>
  data T a where<br>
    T1 :: T a<br>
    T2 :: T Int<br>
<br>
  -- Does this typecheck?<br>
  f :: C a b =&gt; T a -&gt; Bool<br>
  f T1 = True<br>
  f T2 = op 3<br>
<br>
The function f &quot;should&quot; typecheck because inside the T2 branch we know that (a~Int), and hence by the fundep (b~Bool).  But we have no formal type system for fundeps that describes this, and GHC&#39;s implementation certainly rejects it. </blockquote>
</div><br>Martin Sulzmann,
<a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wazny:Jeremy.html">Jeremy Wazny</a>,
<a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/s/Stuckey:Peter_J=.html">Peter J. Stuckey</a>:
A Framework for Extended Algebraic Data Types.
<a href="http://www.informatik.uni-trier.de/%7Eley/db/conf/flops/flops2006.html#SulzmannWS06">FLOPS 2006</a>: 47-64<br><br>describes such a system, fully implemented in Chameleon, but this<br>system is no longer maintained.<br>
<br>Type families and Fundeps are equivalent in expressive power and it&#39;s<br>not too hard to show how to encode one in terms of the other.<br>Local constraints are an orthogonal extension. In terms of type inference,<br>
type families + local constraints and fundeps + local constraints pose the same<br>challenges.<br><br>Probably, Simon is refrerring to the &#39;unresolved&#39; issue of providing a System F style translation for fundeps + local constraints. Well, the point is that System FC<br>
is geared toward type families. The two possible solutions are (a) either<br>consider fundeps as syntactic sugar for type families (doesn&#39;t quite work once<br>you throw in overlapping instances), (b) design a variant System FC_fundep<br>
which has built-in support for fundeps.<br><br>-Martin<br>