Great. Thanks. 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. On Feb 4, 2014 1:20 PM, "Richard Eisenberg" wrote:

Say I have

...

data Nat = Zero | Succ Nat data SNat :: Nat -> * where SZero :: SNat Zero SSucc :: SNat n -> SNat (Succ n) data SBool :: Bool -> * where SFalse :: SBool False STrue :: SBool True

Now, I want

...

eq :: SNat a -> SNat b-> SBool (a == b) eq SZero SZero = STrue eq (SSucc _) SZero = SFalse eq SZero (SSucc _) = SFalse eq (SSucc c) (SSucc d) = eq c d

Does that type check?

Suppose we have

...

type family EqPoly (a :: k) (b :: k) :: Bool where EqPoly a a = True EqPoly a b = False type instance a == b = EqPoly a b

(Let's forget that the instance there would overlap with any other instance.)

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.

Now, suppose

...

type family EqNat a b where EqNat Zero Zero = True EqNat (Succ n) (Succ m) = EqNat n m EqNat Zero (Succ n) = False EqNat (Succ n) Zero = False type instance a == b = EqNat a b

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!

Thus, the second version is better.

I hope this helps! Richard

On Feb 4, 2014, at 1:08 PM, Nicolas Frisby wrote:

[CC'ing Richard, as I'm guessing he's the author of the comment.]

I have a question regarding the comment on the type family Data.Type.Equality.(==).

"A poly-kinded instance [of ==] is *not* provided, as a recursive definition for algebraic kinds is generally more useful."

Can someone elaborate on "generally more useful".

Thank you.