Add Mirror and Snoc type classes to Symbol

[csicar]

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.

[JordanMartinez]

Could you rebase this on top of current master?

[hdgarrood]

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.

[JordanMartinez]

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.
We can now have a type-level Maybe, Either, and List, etc. as well as type-level functions for these types. Where should such data types and functions go in the ecosystem? Should typelevel-prelude be considered at the "bottom" of this type-level library ecosystem as prelude does for value-level libraries? Or does typelevel-prelude combine multiple libraries together?

[hdgarrood]

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.

[LiamGoodacre]

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.

[csicar]

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.

[JordanMartinez]

At the very least, this should include tests to verify it works as expected. I am curious how this would play with reifySymbol though, as I still don't get how one uses that function productively.

[csicar]

That's funny ^^ I had already written tests for this 2 years ago, but forgot to stage them in git. They are now pushed.

[JordanMartinez]

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🍎")

[csicar]

It would be nice to run this in quickcheck, but I cannot find a good way to use reifySymbol with typeclass-computations:
reifySymbol qcSymbol testReverseTwice, but the type of

reifySymbol :: forall proxy r. String -> (forall sym. IsSymbol sym => proxy sym -> r) -> r

does not allow add additional constraints to the (forall sym. IsSymbol sym => proxy sym -> r argument, which would be necessary for Reverse.

In general adding additional constraints would not be sound. But because Reverse is implemented forall Symbols, it would be sound in the case of Reverse.

I.e. for Reverse such a function would be valid:
canReverseAnySymbol :: ∀ a r. IsSymbol a => (∀ b. IsSymbol b => Reverse a b => r) -> r

[JordanMartinez]

LGTM.

[LiamGoodacre]

(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:

• make Reverse have a unidirectional fundep and remove ReverseP
• make ReverseP have a unidirectional fundep & simplify its constraints

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

[LiamGoodacre]

As for Snoc, i feel that might be better as a Prim built-in like Cons is.