<div>On Fri, Feb 12, 2010 at 2:11 PM, Andrew Coppin <span dir="ltr">&lt;<a href="mailto:andrewcoppin@btinternet.com">andrewcoppin@btinternet.com</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0px 0px 0px 0.8ex; BORDER-LEFT: #ccc 1px solid">OK, well in that case, I&#39;m utterly puzzled as to why both forms exist in the first place. If TFs don&#39;t allow you to do anything that can&#39;t be done with ATs, why have them?<br>
<br>My head hurts... </blockquote></div>
<div> </div>
<div>You can say anything you might say with type families using GADTs, but you&#39;ll often be talking about stuff you don&#39;t care about. =)<br> <br>sometimes you don&#39;t care what the Element type of a container is, just that it is a container. Yet using GADTs you must always reference the content type.<br>
 <br>size :: Container&#39; c e =&gt; c -&gt; Int -- using Container&#39; defined with GADTs<br> <br>as opposed to<br> <br>size :: Container c =&gt; c -&gt; Int<br> <br>That doesn&#39;t seem like a huge sacrifice at first, until you start considering things like:<br>
 <br><a href="http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Category-Cartesian-Closed.html">http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Category-Cartesian-Closed.html</a><br>
 <br>Instead of just being able to talk about a CCC based on the type used for its homomorphisms, now I must constantly talk about the type used for its product, and exponentials, and the identity of the product, even when I don&#39;t care about those properties!<br>
 <br>This ability to not talk about those extra types becomes useful when you start defining data types.<br> <br>Say you define a simple imperative growable hash data type, parameterized over the monad type. You could do so with TFs fairly easily:<br>
 <br>newtype Hash m k v = Hash (Ref m (Array Int (Ref m [(k,v)])))<br>empty :: MonadRef m =&gt; m (Hash m k v)<br>insert :: (Hashable k, MonadRef m) =&gt; k -&gt; v -&gt; Hash m k v -&gt; m ()<br> <br>But the GADT version leaks implementation-dependent details out to the data type:<br>
 <br>newtype Hash r k v = Hash (r (Array Int (r [(k,v)])))<br>empty :: MonadRef m r =&gt; m (Hash r k v)<br>insert :: (Hashable k, MonadRef m r) =&gt; k -&gt; v -&gt; Hash r k v -&gt; m ()<br> <br>This gets worse as you need more and more typeclass machinery. <br>
 <br>On the other hand, GADTs are useful when you want to define multidirectional mutual dependencies without repeating yourself. Each is a win in terms of the amount of boilerplate you have to write in different circumstances.<br>
 <br>class Foo a b c | a b -&gt; c, b c -&gt; a, c a -&gt; b where<br>    foo :: a -&gt; b -&gt; c<br> <br>would require 3 different class associate types, one for each fundep.<br> <br>-Edward Kmett</div>