Use leibniz equality #9
Conversation
There was a problem hiding this comment.
Would it be possible to depend on https://github.com/paf31/purescript-leibniz instead of redefining leibniz equality here?
| to a = case leibniz (To a) of | ||
| To b -> b |
There was a problem hiding this comment.
The To newtype is perhaps better for readability but we could define to as leibniz \a -> a.
There was a problem hiding this comment.
Good point, I missed that that was possible.
| from b = case leibnizOp (To b) of | ||
| To a -> a |
There was a problem hiding this comment.
Is leibnizOp really necessary? Given Data.Op.Op we could define from as case leibniz (Op \b -> b) of Op f -> f.
If we don’t want any dependency newtype Op a b = Op (b -> a) is also perhaps a bit simpler than newtype Op a b = Op (forall p. p b -> p a) and could rename it to Symm or something more semantic for this use case (the reversal of a leibniz equality).
There was a problem hiding this comment.
I think having the symmetric/opposite form of Leibniz in this place is good, because sometimes you’ll need both directions (just for easier access) and you don’t want to have to add another constraint. It’s just one newtype that only needs to be used internally.
There was a problem hiding this comment.
I think I would prefer not to export leibnizOp at first; if people want to flip it around they can use the leibniz library, right? If we’re saying this is only the basic stuff and people should use the leibniz library for more involved usage, then to me that seems consistent with not exporting leibnizOp.
| class TypeEquals a b | a -> b, b -> a where | ||
| to :: a -> b | ||
| from :: b -> a | ||
| leibniz :: forall p. p a -> p b |
There was a problem hiding this comment.
I like proof for this, yeah
|
We can’t depend on Phil’s library because it’s not in the core packages. Also, I prefer not to, simply because it’s unnecessary: we don’t even need to export a Leibniz type, we can just use the encoding. If users want more operations for manipulating the equalities they can easily use it with a Leibniz library or write it themselves. (Even if the Leibniz constructor was not exposed, you can still convert between the representations by using |
|
This was merged with #11. Thank you for proposing that in the first place @MonoidMusician! |
Using Leibniz equality lets us have polykinds and also have more evidence for stronger coercions down the line (not just to/from, which need to be manually threaded through functor-y things).
This should be backwards-compatible, since we have the same public API.