I like the idea of being able to produce a witness of equality like this. I see that unsafeCoerce is necessary to write instances for Nat and Symbol, but it wouldn't be necessary for inductively defined singletons.
I don't think that sameSing should be in the SingE class, because not all singletons may want to support a notion of equality like this. SingE is designed to be applicable to all singletons refined from standard datatypes. I also agree with Pedro that your SingEq class is more widely applicable than just for singletons and should have a more general name. Though it serves a different purpose, you may also want to check out the SEq class in the singletons package, viewable here: https://github.com/goldfirere/singletons/blob/master/devel/Data/Singletons.hs#L108 SEq only works with boolean equality, not propositional equality, so it surely solves a different problem. One further thought: instead of just returning Nothing on disequality, what about using something like this (borrowing from Coq): data a :==: b where Refl :: a :==: a data EmptySet type Not a = a -> EmptySet type DecidableEquality (a :: k) (b :: k) = Either (a :==: b) (Not (a :==: b)) class kparam ~ KindParam => DecEq (kparam :: OfKind k) where decEq :: forall (a :: k) (b :: k). Sing a -> Sing b -> DecidableEquality a b instance DecEq (KindParam :: OfKind Nat) where decEq a b = if fromSing a == fromSing b then Left (unsafeCoerce Refl) else Right (\_ -> undefined) This may be overkill, but I would guess that something like the above is in the future for this approach… Richard On Nov 30, 2012, at 9:13 AM, Gabor Greif wrote: > Hi all! > > After encouragement from Iavor on G+, here is a patch that implements > a class method for singleton type equality witnesses in a generic way. > > Please comment on two things: > - is this a good approach? > - how can we avoid abuse of SingEq (as it is type polymorphic, can this > harm?) > - (possibly) bikeshedding on names. > > Cheers and thanks, > > Gabor > <TypeLits.hs.patch>_______________________________________________ > Cvs-ghc mailing list > Cvs-ghc@haskell.org > http://www.haskell.org/mailman/listinfo/cvs-ghc _______________________________________________ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
