A few points of response: - The 'Not' that I am proposing is distinct from the Boolean 'Not' that is easy to write. I was inspired by this discussion to write a blog post about the issue; see http://typesandkinds.wordpress.com/2012/12/01/decidable-propositional-equality-in-haskell/ The end of the (overly long) post is the interesting bit about Not.
I admit that the propositional Not isn't as useful in GHC as it currently stands, but with bigfixes for #3927 and #2431, it would gain a new lease on life. - +1 to (:~:); this reserves (:==:) for type-level Boolean equality, which matches (==) better. - I'm mildly in favor of making SingE (and SingI?) a superclass of the equality class, but I don't have strong feelings. - I agree that * can be part of the singletons framework. The singletons library has similar definitions to the ones Iavor proposes. See https://github.com/goldfirere/singletons/blob/master/devel/Data/Singletons/TypeRepStar.hs The one problem with this approach is that TypeRep does not get promoted to *. So, if you have a datatype that uses TypeRep and you want to use that datatype with singletons, you're out of luck. An example might help: data Foo = Bar Bool TypeRep does not get promoted, because TypeRep is not promotable. What I would like is to get the following: data kind Foo = Bar Bool * The workaround (due to Pedro's recent WGP paper): data Foo a = Bar Bool a type FooTypeRep = Foo TypeRep -- I wish: kind FooStar = Foo *, but we don't have kind synonyms This works reasonably well, and I think you could hand-code most of the singletons definitions around this. However, because of this restriction around promoting TypeRep, I wrote a different singleton associated with * in https://github.com/goldfirere/singletons/blob/master/devel/Data/Singletons/CustomStar.hs Unfortunately, that's much harder to make sense of, so see here: https://github.com/goldfirere/singletons/blob/master/devel/README#L409 The idea is that the programmer chooses some subset of * as their universe. The implementation creates a datatype 'Rep' as a type representation. While Rep is not automatically promoted to *, functions over Rep do get promoted to type families over *. Bottom line: I would hesitate committing to a single choice for the singleton associated with * until TypeRep automatically gets promoted to *. Which leads me to ask: Why can't we special-case TypeRep to be promoted to *, allowing the construction I wrote above? It seems both kludgy and elegant at the same time, somehow. I would love to hear others' thoughts on this. Thanks, Richard On Nov 30, 2012, at 1:58 PM, Iavor Diatchki wrote: > 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
