| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Noether.Equality
Description
Flexible, extensible notions of equality supporting "custom deriving strategies".
This module is, as of now, completely separate from the rest of the codebase (which was developed later, using ideas first tested here).
There are no incoherent or even overlapping instances anywhere here. The ideas are based off of the "Advanced Overlap" page on the Haskell wiki: https://wiki.haskell.org/GHC/AdvancedOverlap, and were inspired by the observation that the overlapping instances there could be completely replaced with not-necessarily-closed type families.
This last point is crucial for Noether, which aspires to be a library that people can use for their own work. The closed-TF approach of declaring how a couple standard types are compared, putting a catch-all case after those to handle everything else (all in the core library), and then calling it a day isn't really sensible, then, for obvious reasons.
I have some prototype Oleg-style "guided resolution" in development that seems to be promising, and I think this approach, together with the former, can be used to handle (instances of typeclasses representing) algebraic structures on types without the incoherent nonsense in place currently.
- type family Equality a
- type family EquateResult s a
- type EquateResult' a = EquateResult (Equality a) a
- type EquateAs' a = EquateAs (Equality a) a
- class Eq a where
- class EquateAs s a where
- data PreludeEq
- data Numeric
- data Approximate
- data Common a
- data Composite a b
- data Explicit s
- data Modulo n
- data CoerceFrom a s
- type CoerceFrom' a = CoerceFrom a (Equality a)
Documentation
type family Equality a Source #
This represents the unique "equality strategy" to be used for a.
There may be many different notions of equality that can be applied to a
particular type, and instances of the Equality family are used to disambiguate
those by specifying which one to use.
type family EquateResult s a Source #
Different notions of equality can have different "results". For instance, standard Eq-style "tired" equality returns Bool values, whereas a more numerically "wired" implementation for floating-point numbers could instead use tolerances/"epsilons" to compare things.
This is reminiscent of subhask-ish things (in particular, the all-pervasive Logic type family).
Instances
| type EquateResult Approximate a Source # | |
| type EquateResult Numeric a Source # | |
| type EquateResult PreludeEq a Source # | |
| type EquateResult (Explicit * (Modulo n)) Int Source # | |
| type EquateResult (Common * Approximate) (a, a) Source # | |
| type EquateResult (Common * Numeric) (a, a) Source # | |
| type EquateResult (Common * PreludeEq) (a, a) Source # | |
| type EquateResult (CoerceFrom * * a s) b Source # | |
| type EquateResult (Composite * * l r) (a, b) Source # | |
type EquateResult' a = EquateResult (Equality a) a Source #
This is the user-facing Eq replacement class.
The Eq a/EquateAs s a trick is straight off the GHC wiki, as I said, although
we can now use proxies instead of slinging undefineds around :)
Minimal complete definition
Methods
(==) :: a -> a -> EquateResult' a Source #
class EquateAs s a where Source #
An instance of this class defines a way to equate two terms of
a given type according to a given "strategy" s.
Minimal complete definition
Methods
equateAs :: Proxy# s -> a -> a -> EquateResult s a Source #
Instances
| (Num a, Ord a) => EquateAs Approximate a Source # | |
| (Eq a, Num a) => EquateAs Numeric a Source # | |
| Eq a => EquateAs PreludeEq a Source # | |
| KnownNat n => EquateAs (Explicit * (Modulo n)) Int Source # | |
| EquateAs Approximate a => EquateAs (Common * Approximate) (a, a) Source # | |
| (EquateAs Numeric a, EquateAs Numeric a) => EquateAs (Common * Numeric) (a, a) Source # | |
| (EquateAs PreludeEq a, EquateAs PreludeEq a) => EquateAs (Common * PreludeEq) (a, a) Source # | |
| (EquateAs s a, Coercible * b a) => EquateAs (CoerceFrom * * a s) b Source # | |
| (EquateAs l a, EquateAs r b) => EquateAs (Composite * * l r) (a, b) Source # | |
data Approximate Source #
Instances
| (Num a, Ord a) => EquateAs Approximate a Source # | |
| EquateAs Approximate a => EquateAs (Common * Approximate) (a, a) Source # | |
| type EquateResult Approximate a Source # | |
| type EquateResult (Common * Approximate) (a, a) Source # | |
Instances
| EquateAs Approximate a => EquateAs (Common * Approximate) (a, a) Source # | |
| (EquateAs Numeric a, EquateAs Numeric a) => EquateAs (Common * Numeric) (a, a) Source # | |
| (EquateAs PreludeEq a, EquateAs PreludeEq a) => EquateAs (Common * PreludeEq) (a, a) Source # | |
| type EquateResult (Common * Approximate) (a, a) Source # | |
| type EquateResult (Common * Numeric) (a, a) Source # | |
| type EquateResult (Common * PreludeEq) (a, a) Source # | |
The Composite strategy just uses the canonical strategies on each
"slot" of the tuple and returns a tuple of results.
It's ... sort of lazy.
data CoerceFrom a s Source #
Lightweight equality for newtypes using Coercible from Coerce.
This is so, so wonderful. (Well, now that the complaints about differing representations have gone away, anyway.)
Instances
| (EquateAs s a, Coercible * b a) => EquateAs (CoerceFrom * * a s) b Source # | |
| type EquateResult (CoerceFrom * * a s) b Source # | |
type CoerceFrom' a = CoerceFrom a (Equality a) Source #