New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Define Eq
and Ord
instances for SSymbol
, SChar
, and SNat
#148
Comments
Another reason is to support derived instances. data Foo n = Foo !(SNat n) String
deriving (Eq, Ord) I'm in favor. |
This seems quite uncontroversial to me. @RyanGlScott could you please raise an MR which we can vote on? |
This implements [CLC proposal #148](haskell/core-libraries-committee#148).
+1 |
Dear CLC members, let's vote on the proposal to add @tomjaguarpaw @chshersh @hasufell @angerman @parsonsmatt +1 from me. |
+1 |
+1 If only every proposal was as easy to vote for as this one 🥺 |
+1 |
1 similar comment
+1 |
Thanks all, 6 votes out of 7 possible are enough for approval. |
I'm trying to summarise the state of this proposal as part of my volunteering effort to track the progress of all
Please, let me know if you find any mistakes 🙂 |
This implements [CLC proposal ghc#148](haskell/core-libraries-committee#148).
There are four singleton types currently defined in
base
:TypeRep
, defined inType.Reflection
SSymbol
, defined inGHC.TypeLits
SChar
, defined inGHC.TypeLits
SNat
, defined inGHC.TypeNats
SSymbol
,SChar
, andSNat
were introduced as part of proposal #85, and their APIs were designed to mimic that ofTypeRep
. Unfortunately, #85 forgot to carry over one aspect of theTypeRep
API: theEq
andOrd
instances:I propose that we define similar
Eq
andOrd
instances forSSymbol
,SChar
, andSNat
.How?
How can we know that the
Eq
andOrd
instances forTypeRep
always returnTrue
/EQ
? This is becauseTypeRep
is a singleton type. That is, given a fixed typea
, there is only ever a single unique value¹ that can inhabit typeTypeRep a
. Therefore, the equality checks that(==)
andcompare
perform will always succeed by virtue of the typing discipline involved.The same reasoning applies to all other singleton types, including
SSymbol
,SChar
, andSNat
.Why?
Why bother defining these instances in the first place? On their own, they aren't terribly useful, as
(==)
/compare
will always compute the same answer. They are more useful for the purpose of satisfying superclasses of other instances. For instance, theEqP
class in thesome
library requires a quantifiedEq
superclass, so it would not be possible to define anEqP
instance forTypeRep
(or any other singleton type) without first giving it anEq
instance.Prior art
TypeRep
is the most notable singleton type to defineEq
/Ord
instances in this fashion. BesidesTypeRep
, I have also found other occurrences of these sort ofEq
/Ord
instances in the wild:SNat
, defined insingleton-nats
SBool
, defined insingleton-bool
BoolRepr
,NatRepr
, andSymbolRepr
, defined inparameterized-utils
¹ Besides
⊥
, but it is fine to reason modulo⊥
.The text was updated successfully, but these errors were encountered: