I'm afraid I have not followed this thread in detail; I'm entirely happy to let you decide what the TypeLits library should look like.
But do pls highlight to me any changes to GHC that you think are high priority. I'm very hazy about why this empty-case thing is a big deal. And we also have an open thread about what TypeRep should look like, and whether we should have a typed version of that. It looks as if the two discussions overlap somehow but I'm not sure exactly how. Sorry - I'm just getting a bit lost among all these trees! Simon From: cvs-ghc-boun...@haskell.org [mailto:cvs-ghc-boun...@haskell.org] On Behalf Of Richard Eisenberg Sent: 01 December 2012 16:31 To: Iavor Diatchki Cc: Iavor Diatchki; cvs-ghc Subject: Re: RFC: Singleton equality witnesses 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<mailto: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<mailto:Cvs-ghc@haskell.org> > http://www.haskell.org/mailman/listinfo/cvs-ghc _______________________________________________ Cvs-ghc mailing list Cvs-ghc@haskell.org<mailto: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
