[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... URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140204/1d7bc626/attachment.html> |
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 <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... URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140204/c1aef559/attachment-0001.html> |
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" <eir at cis.upenn.edu> 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 <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. > > > An HTML attachment was scrubbed... URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140204/05a8b28d/attachment.html> |
Free forum by Nabble | Edit this page |