please elaborate on comment for base:Data.Type.Equality.(==)?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

please elaborate on comment for base:Data.Type.Equality.(==)?

Nicolas Frisby
[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>

Reply | Threaded
Open this post in threaded view
|

please elaborate on comment for base:Data.Type.Equality.(==)?

Richard Eisenberg-2
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>

Reply | Threaded
Open this post in threaded view
|

please elaborate on comment for base:Data.Type.Equality.(==)?

Nicolas Frisby
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.
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140204/05a8b28d/attachment.html>