Re: RFC: Singleton equality witnesses
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#L409The
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
RE: RFC: Singleton equality witnesses
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#L409The 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.edumailto: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
Re: RFC: Singleton equality witnesses
On Sat, Dec 1, 2012 at 10:46 PM, Gábor Lehel illiss...@gmail.com wrote: On Sat, Dec 1, 2012 at 5:31 PM, Richard Eisenberg e...@cis.upenn.edu wrote: 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 Hmm, isn't TypeRep also used to represent types of other kinds, though, not just *? I share this concern; TypeRep represents things of all kinds, so it's a bit surprising that its promotion would be * ... (For the record, I also think that :~: is a better name.) Cheers, Pedro -- Your ship was destroyed in a monadic eruption. ___ 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
Re: RFC: Singleton equality witnesses
On Dec 1, 2012, at 5:46 PM, Gábor Lehel wrote: Hmm, isn't TypeRep also used to represent types of other kinds, though, not just *? Yes, of course. Silly me. Richard ___ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
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#L409The 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
Re: RFC: Singleton equality witnesses
On Sat, Dec 1, 2012 at 5:31 PM, Richard Eisenberg e...@cis.upenn.edu wrote: 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 Hmm, isn't TypeRep also used to represent types of other kinds, though, not just *? -- Your ship was destroyed in a monadic eruption. ___ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
RFC: Singleton equality witnesses
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 Description: Binary data ___ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
Re: RFC: Singleton equality witnesses
Hi Gabor, Only one (minor) comment: `SingEq` is not specific to singletons, is it? To me it looks like a kind-polymorphic type equality predicate, useful to have in several situations. Why not call the datatype (:==:), its constructor Refl, and put it in GHC.Exts? I guess that things like `Proxy` should probably go directly to GHC.Exts as well... Cheers, Pedro On Fri, Nov 30, 2012 at 2:13 PM, Gabor Greif ggr...@gmail.com 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 ___ 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
Re: RFC: Singleton equality witnesses
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
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 e...@cis.upenn.eduwrote: 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
Re: RFC: Singleton equality witnesses
On Fri, Nov 30, 2012 at 7:58 PM, Iavor Diatchki iavor.diatc...@gmail.com wrote: Hello, Here are my thoughts: * I agree that we should use (:==:) for the name, as it is not specific to singletons. Apologies for the bikeshedding, but why not (:~:)? -- Your ship was destroyed in a monadic eruption. ___ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
