-
Notifications
You must be signed in to change notification settings - Fork 21
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
Add Mirror and Snoc type classes to Symbol #51
base: master
Are you sure you want to change the base?
Conversation
Could you rebase this on top of current |
I’m actually undecided on whether this ought to be in typelevel-prelude. It’s at a very high up place in the hierarchy so we should be quite choosy about what we put in it. |
Two questions. First, does the class and its instances look good, so that we should accept it (wherever it is we do put it). Second, where should it go? Now that PolyKinds are supported, there are many other compile-time programming we can do. While the below question doesn't need to be answered before v0.14.0 comes out, it's been on my mind. |
I don’t do enough type level programming to feel confident reviewing this, although I think Reverse might be a better name than Mirror. Also, even if it does look good, that doesn’t necessarily mean it needs to live in core; it could live in some other library outside of core, or even in the project where it’s needed. I think there should be evidence of demand for something across multiple people and projects before we merge it in here, ideally. Typelevel-prelude should be considered at the bottom of the hierarchy for type-level programming libraries because it only depends on prelude and type-equality (which is tiny), and because most other type-level libraries are likely to depend on it. |
src/Type/Data/Symbol.purs
Outdated
|
||
-- Mirror | ||
|
||
class MirrorP (a :: Symbol) (mirror :: Symbol) | a -> mirror, mirror -> a |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The mirror -> a
functional dependency here doesn't seem to be respected by the mirrorCons
instance. Possibly makes sense to keep MirrorP
unidirectional anyway, if Mirror
runs it in both directions.
Going one step further: another option is to only have the one class, and keep it unidirectional.
Because Mirror
is its own inverse, users can swap the args if they need it to run it the other direction. If a user wants both directions, they can use two constraints like you did in mirrorMirrorP
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is has been some time since I wrote this code, so I need to retrace my steps here.
If I remember correctly the advantage of having Mirror be bidirectional is, that type inference works a lot better.
At the very least, this should include tests to verify it works as expected. I am curious how this would play with |
That's funny ^^ I had already written tests for this 2 years ago, but forgot to stage them in git. They are now pushed. |
Can you add these two tests? -- or something like this that verifies this is true
testReverseTwice :: forall a b. IsSymbol a => IsSymbol b => Reverse a b => Proxy a -> Boolean
testReverseTwice p = reflectSymbol p == reflectSymbol sameThing
where
sameThing = reverse (reverse p)
-- just confirming that more complex unicode works
testUnicode :: Proxy _
testUnicode = reverse (Proxy :: Proxy "pine🍎") |
It would be nice to run this in quickcheck, but I cannot find a good way to use reifySymbol :: forall proxy r. String -> (forall sym. IsSymbol sym => proxy sym -> r) -> r does not allow add additional constraints to the In general adding additional constraints would not be sound. But because I.e. for |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM.
(I don't have any real opinion about whether this should be added, but...) As i touched on above, i still think it'd make more sense to either:
The current implementation seems to have a bit too much going on regarding instance constraints. I'm imagining something like: class Reverse (i :: Symbol) (o :: Symbol) | i -> o
instance Reverse "" ""
else
instance ( Symbol.Cons h t l, Reverse t s, Symbol.Append s h r ) => Reverse l r
reverse :: forall i o proxy . Reverse i o => proxy i -> Proxy o
reverse _ = Proxy
--
example :: Proxy _ -- "fedcba"
example = reverse (Proxy :: _ "abcdef")
check :: Proxy _ -- True
check =
Symbol.equals
(reverse (reverse example))
example
checkReflected :: Boolean
checkReflected =
Symbol.reflectSymbol (reverse (reverse example))
==
Symbol.reflectSymbol example |
As for |
This PR adds Type-Classes for Mirroring Symbols ("Test" ~> "tseT") and Snoc ("Tes" "t" ~> "Test").
These Type-Classes can be useful when parsing Symbols to Numbers.
If this is to esoteric for the typelevel-prelude, feel free to reject the PR.