<html><head><meta http-equiv="Content-Type" content="text/html charset=iso-8859-1"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><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">nicolas.frisby@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><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></body></html>