Re: RFC: Singleton equality witnesses

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
> [email protected]
> http://www.haskell.org/mailman/listinfo/cvs-ghc