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 <e...@cis.upenn.edu>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
> > 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
>
_______________________________________________
Cvs-ghc mailing list
Cvs-ghc@haskell.org
http://www.haskell.org/mailman/listinfo/cvs-ghc
