<p dir="ltr">Great. Thanks.</p>
<p dir="ltr">This reminds me of one emphasis of McBride's lectures and keynotes regarding Agda: it's generally a Good Thing for the shape of your type level recursion to match your value level recursion.</p>
<div class="gmail_quote">On Feb 4, 2014 1:20 PM, "Richard Eisenberg" <<a href="mailto:eir@cis.upenn.edu">eir@cis.upenn.edu</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div style="word-wrap:break-word"><div>Say I have</div><div><br></div><div>> data Nat = Zero | Succ Nat</div><div>> data SNat :: Nat -> * where</div><div>>   SZero :: SNat Zero</div><div>>   SSucc :: SNat n -> SNat (Succ n)</div>
<div>> data SBool :: Bool -> * where</div><div>>   SFalse :: SBool False</div><div>>   STrue :: SBool True</div><div><br></div><div>Now, I want</div><div><br></div><div>> eq :: SNat a -> SNat b-> SBool (a == b)</div>
<div>> eq SZero SZero = STrue</div><div>> eq (SSucc _) SZero = SFalse</div><div>> eq SZero (SSucc _) = SFalse</div><div>> eq (SSucc c) (SSucc d) = eq c d</div><div><br></div><div>Does that type check?</div><div>
<br></div><div>Suppose we have</div><div><br></div><div>> type family EqPoly (a :: k) (b :: k) :: Bool where</div><div>>   EqPoly a a = True</div><div>>   EqPoly a b = False</div><div>> type instance a == b = EqPoly a b</div>
<div><br></div><div>(Let's forget that the instance there would overlap with any other instance.)</div><div><br></div><div>Now, in the last line of `eq`, we have that the type of `eq c d` is `SBool (e == f)` where (c :: SNat e), (d :: SNat f), (a ~ Succ e), and (b ~ Succ f). But, does ((e == f) ~ (a == b))? It would need to for the last line of `eq` to type-check. Alas, there is no way to proof ((e == f) ~ (a == b)), so we're hosed.</div>
<div><br></div><div>Now, suppose</div><div><br></div><div>> type family EqNat a b where</div><div>>   EqNat Zero Zero = True</div><div>>   EqNat (Succ n) (Succ m) = EqNat n m</div><div>>   EqNat Zero (Succ n) = False</div>
<div>>   EqNat (Succ n) Zero = False</div><div>> type instance a == b = EqNat a b</div><div><br></div><div>Here, we know that (a ~ Succ e) and (b ~ Succ f), so we compute that (a == b) ~ (EqNat (Succ e) (Succ f)) ~ (EqNat e f) ~ (e == f). Huzzah!</div>
<div><br></div><div>Thus, the second version is better.</div><div><br></div><div>I hope this helps!</div><div>Richard</div><br><div><div>On Feb 4, 2014, at 1:08 PM, Nicolas Frisby <<a href="mailto:nicolas.frisby@gmail.com" target="_blank">nicolas.frisby@gmail.com</a>> wrote:</div>
<br><blockquote type="cite"><div dir="ltr">[CC'ing Richard, as I'm guessing he's the author of the comment.]<div><br></div><div>I have a question regarding the comment on the type family Data.Type.Equality.(==).<div>
<br></div><div>  "<span style="font-family:sans-serif;font-size:13px;line-height:18.200000762939453px">A poly-kinded instance [of ==] is </span><em style="margin:0px;padding:0px;font-family:sans-serif;font-size:13px;line-height:18.200000762939453px">not</em><span style="font-family:sans-serif;font-size:13px;line-height:18.200000762939453px"> provided, as a recursive definition for algebraic kinds is generally more useful."</span></div>


<div><span style="font-family:sans-serif;font-size:13px;line-height:18.200000762939453px"><br></span></div><div>Can someone elaborate on "generally more useful".</div><div><br></div><div>Thank you.</div>

</div></div>
</blockquote></div><br></div></blockquote></div>