Re: RFC: Singleton equality witnesses

Hello,
Here are my thoughts:
  * I agree that we should use (:==:) for the name, as it is not specific
to singletons.
  * I don't think that we need the Coq style `Not` as in Haskell we already
have this function anyway, so the `Right` case would not be giving any new
information and just making things more complex.
  * I tend to agree that perhaps this should be a separate class.
  * I think that, perhaps, the new class should have `SingE` as a super
class.  Not sure about that though, what do you guys think?

A tangentially related idea.  I was wondering if, perhaps, we should make *
be part of the singleton framework, it seems to fit rather naturally, with
TypeReps as evidence,
and it serves a similar purpose to `Proxy`.  Here's the implementation:

newtype instance Sing (x :: *) = SingT TypeRep

instance Typeable a => SingI (a :: *) where
  sing = mk undefined -- or just use scoped type variables
    where mk :: Typeable a => a -> Sing a
          mk = SingT . typeOf

instance SingE (KindParam :: OfKind *) where
  type DemoteRep (KindParam :: OfKind *) = TypeRep
  fromSing (SingT t) = t

Pedro, would that fit the new version of typeable that you've been working
on?

-Iavor





On Fri, Nov 30, 2012 at 7:56 AM, Richard Eisenberg <[email protected]>wrote:

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

_______________________________________________
Cvs-ghc mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/cvs-ghc