[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
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 _)
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 e...@cis.upenn.edu wrote:
Say I have
data
