Use Leibniz equality #11
Conversation
- Rename `leibniz` to `typeEqualsProof`. I changed my mind about `proof` because I think it's likely to be used as a variable name in other places already. - Remove `leibnizOp` - Simplify implementations of `to` and `from`
|
cc @kl0tl |
There was a problem hiding this comment.
I would find an implementation of from based on newtype From a b = From (b -> a) a bit simpler:
from :: forall a b. TypeEquals a b => b -> a
from = case typeEqualsProof (From (\a -> a)) of From f -> fespecially if we don’t export symm.
A similar implementation of to based on a redundant newtype To a b = To (a -> b) would then be nice for symmetry.
This looks good to me regardless though!
test/Main.purs
Outdated
| test2 :: forall ty row. TypeEquals row ( message :: String ) => Newtype ty (Record row) => ty -> String | ||
| test2 = unwrap >>> typeEqualsProof >>> _.message |
There was a problem hiding this comment.
message seems like a good name for that function.
src/Type/Equality.purs
Outdated
| class TypeEquals a b | a -> b, b -> a where | ||
| to :: a -> b | ||
| from :: b -> a | ||
| typeEqualsProof :: forall p. p a -> p b |
There was a problem hiding this comment.
I think proof is more likely to be used as a local variable name, which is why I was thinking of giving this a longer name. I guess it depends whether we expect this module to be imported qualified or not?
There was a problem hiding this comment.
I was imagining it'll be qualified - that's also the pattern we've been encouraging in most places - dropping type/class names from functions and members, like all the Ref stuff a while back.
With it already having names like to and from I've only ever imported it qualified as it is.
There was a problem hiding this comment.
Yeah, true. It seems Type.Prelude currently re-exports the entirety of this module unqualified, which I think is perhaps not ideal. Come to think of it I'm not sure if people tend to import Type.Prelude qualified or not. Maybe we could just not re-export the new proof from Type.Prelude?
There was a problem hiding this comment.
Not re-exporting proof sounds fine to me 👍.
I'm not sure I've ever imported Type.Prelude at all, but if I were to do so I'd probably import it qualified, but then I import almost everything qualified these days, unless it's in our app prelude.
There was a problem hiding this comment.
Type.Prelude re-exports only TypeEquals, from and to so nothing to change there then o/
|
If someone wants to carry this over the line I'd be grateful. I think all that's necessary is replacing |
|
I pushed a few commits, this should be good to merge once Travis agrees. |
Following on from #9