please elaborate on comment for base:Data.Type.Equality.(==)?
eir at cis.upenn.edu
Tue Feb 4 19:20:52 UTC 2014
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.
> 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!
On Feb 4, 2014, at 1:08 PM, Nicolas Frisby <nicolas.frisby at gmail.com> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the ghc-devs