I don't think anything here is *high priority*, just musings on how best to
move forward.
About empty case, consider this:
> data a :~: b where
> Refl :: a :~: a
>
> absurd :: True :~: False -> a
Now, I want to write a term binding for absurd. GHC can figure out that (True
:~: False) is an empty type. So, if we have (absurd x = case x of …), there are
no valid patterns, other than _, that could be used. Instead of writing (absurd
_ = undefined), I would much prefer to write (absurd x = case x of {}). Why? If
I compile with -fwarn-incomplete-patterns and -Werror, then the latter has no
possible source of partiality and yet compiles. The former looks dangerous, and
GHC doesn't check to make sure that, in fact, the function can never get called.
The bottom line, for me at least, is that I want to avoid the partial
constructs (incomplete patterns, undefined, etc) in Haskell as much as
possible, especially when I'm leveraging the type system to a high degree. The
lack of empty case statements forces me to use undefined where it isn't really
necessary.
I'll leave it to others to comment on TypeRep, as I'm a little hazy there
myself.
Richard
On Dec 5, 2012, at 5:05 AM, Simon Peyton-Jones wrote:
> 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> 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
