Better docs to distinguish from TestEquality

[Ericson2314]

See https://github.com/haskell/core-libraries-committee/issues/21. The important thing about GEq is that it is doing term and type equality. Likewise GCompare is doing value ordering.

This will be easier after https://github.com/haskellari/some/pull/21, as the quantified constraints bring the plain H98 classes "in scope", so we can less awkwardly write laws clarifying the situation.

(That PR is in turn blocked on https://github.com/haskell/core-libraries-committee/issues/10, but the current plain H98 class instances for Sum and Product are too pointlessly restrictive for this to work.)

[phadej]

I wouldn't hold my breath on #21 going in. Please, hold your horses.

[Ericson2314]

Oh I know

[bb010g]

If GEq f is doing term and type equality, then shouldn't TestEquality f, which is just type quality, be a superclass?

[langston-barrett]

I'd like to see this clarification, especially now that https://github.com/haskell/core-libraries-committee/issues/21 is resolved. It may help us use this package instead of Data.Parameterized.Some (https://github.com/GaloisInc/parameterized-utils/issues/62).

[phadej]

@bb010g if they would do different thing, I think it might be a good idea to keep them separate. Having types implement the function with a complicated type (suggesting they do the thing) is confusing. In fact, GEq and TestEquality requirements are conflicting for data TagInt a where TagInt1 :: TagInt Int; TagInt2 :: TagInt Int type.

Typically, only singleton types should inhabit this class. In that case type argument equality coincides with term equality:

I'd follow that suggestion and only write TestEquality for singleton types. If GEq had TestEquality as a constraint, that would force to write TestEquality instance for non-singleton types too, something people may not want to do.

TL;DR I'd keep the classes separate. I have to adjust the docs now as the @Ericson2314 change in base is released, so I can refer to it.

[bb010g]

@phadej Right after that suggestion, it says:

Singleton types are not required, however, and so the latter two would-be laws are not in fact valid in general.

haskell/core-libraries-committee#21 explicitly accepted the "Weaker" option of ghc/ghc#7333, which means

instance TestEquality Tag where
    testEquality TagInt1 TagInt1 = Just Refl
    testEquality TagInt1 TagInt2 = Just Refl
    testEquality TagInt2 TagInt1 = Just Refl
    testEquality TagInt2 TagInt2 = Just Refl

is explicitly a legal instance. If people want a typeclass where type argument equality coincides with term equality, then they should use a typeclass where that is explicitly the case (i.e. not TestEquality).

I don't see why GEq should act as if the "Strongest" option for TestEquality was chosen by the committee when that isn't the case.

[phadej]

is explicitly a legal instance.

It's also the only legal TestEquality instance for Tag.

That however is probably not the GEq instance you want. (GEq can act the same way, but then the == and defaultEq should probably agree as well).

[bb010g]

I agree that you don't want that instance for GEq. I'd imagine GEq would still have a geq :: f a -> f b -> Maybe (a :~: b) that doesn't default to geq = testEquality? You would want TestEquality as a superclass constraint, though, as geq x y != None should entail geq x y == testEquality x y, and testEquality x y == None should entail testEquality x y == geq x y. geq differs from testEquality in that for some values x and y where testEquality x y == Just Refl, geq x y == None, whenever x and y are not equal at the term level.

[phadej]

@bb010g your analysis of TestEquality and GEq relationship seems correct, but I still disagree that either class should imply other.

As I said, it's very much the purpose of GEq to have instances for types like GEq, but forcing users to write phishy instance TestEquality Tag is IMO not nice. Yes, the laws of TestEquality allow to write TestEquality Tag, but I argue that it's not good idea. And base docs say Typically, only singleton types should inhabit this class.. I repeat, I don't want to force users of GEq to go against that recommendation.

I also think that if relation could be there, it should be GEq f => TestEquality f.

I won't add the dependency, and close this issue when I get to update the docs. There is no practical motivation to have GEq or TestEquality imply each other.

(3rd option is to add geq method to TestEquality, as I don't think there is a type which can implement only GEq or TestEquality but not the other - I might be wrong though, as I didn't think too hard about that).

[bb010g]

@phadej I think you could implement TestEquality DynamicF where data DynamicF f where { DynamicF :: forall a. TypeRep (f a) -> f a -> DynamicF f; }, but not GEq DynamicF, as you don't have a witness of value equality for f a.

I repeat, I don't want to force users of GEq to go against that recommendation.

I'm curious what @Ericson2314's thoughts are here. This doesn't feel right to me; if this wording is making you feel unsure about what laws the class has, I would like to see it removed and, if necessary, TypeEquality's laws changed again to reflect how the class is going to be used. I personally don't see the point in having a typeclass like this in base that's going to be inconsistently implemented. Maybe there really just needs to be a typeclass in base where

Just Refl means the type params are equal, and the values are equal, and the class assume if the type params are equal the values must also be equal. In other words, the type is a singleton type when the type parameter is a closed term.

alongside a typeclass with weaker laws, so people know their options and can choose what's necessary without assuming TestEquality has stronger laws than it does.

There is no practical motivation to have GEq or TestEquality imply each other.

By that reasoning, is there a practical reason for Ord to imply Eq? Both compare and <= don't rely on ==.

[phadej]

I'm curious what @Ericson2314's thoughts are here.

It's irrelevant. CLC didn't wanted to restrict TestEquality to singletons only (which was an option). Then TestEquality couldn't be a super-class of GEq, and this case would been closed for good.

Ord and Eq

Ord explicitly mentions Eq in laws.

Antisymmetry if x <= y && y <= x = True, then x == y = True

One can argue that GEq should have laws tying it to testEquality, as we discussed. But I disagree. These classes are different enough, so I consider better to make people think which one they need. I cannot think of example where people need both at the same time.

[Ericson2314]

data Foo a where
  MkFoo :: (Nat -> Nat) -> Foo () 

is a simple example of a data type for which TestEquality Foo exists (and is trivial), and GEq Foo does not exist.

TestEquality is indeed logically a super class, but I am in no rush to add the superclass relationship because it would be a big breaking change and I think the "stylistic" argument that the purpose are rather different does hold water. But I could go either way on this.

Regardless:

geqFromTestEquality a b = do
  prf @ Refl <- testEquality
  guard $ a == b
  Just prf

is now a valid function and we should probably add at least that.

[phadej]

geqFromTestEquality a b = do
  prf @ Refl <- testEquality
  guard $ a == b
  Just prf

is "good", but OTOH we don't require that Eq and GEq are compatible. We probably should (re #21), but I want to wait until 9.6 hits the masses and we learn a bit more about QuantifiedConstraints in the wild.

[phadej]

I come up with an example, where one can have GEq but cannot have TestEquality.

Well, rather one can have GCoerce (#46 ) but not TestCoercion:

We can have GCoerce IORef as if IORefs are equal the types should be coercible, but we cannot test whether the types are coercible in TestCoercion sense:

If we have x :: IORef a and y :: IORef b, we cannot satisfy TestCoercion (x :: IORef a) (y :: IORef b) = Just Coercion ⟺ Coercible a b

Similarly if one makes IORef-like nominally represented type, it can have GEq, but no TestEquality.

[phadej]

Though TestCoercion doesn't have docs clarified as TestEquality, i think it's just an oversight to be fixed soon, what you think @Ericson2314?

[phadej]

Another, maybe even less contrived example is the instance for Sum

instance (GEq a, GEq b) => GEq (Sum a b) where
    geq (InL x) (InL y) = geq x y
    geq (InR x) (InR y) = geq x y
    geq _ _ = Nothing

But one cannot have

instance (TestEquality a, TestEquality b) => TestEquality (Sum a b) where

as e.g. testEquality (InL TagInt1) (InR TagInt2) should result in Just Refl, but it seems impossible to do that in general.

[Ericson2314]

Oops didn't reply here. Yeah I think the IORef counterexample is valid. Sum also. Frankly, it sounds like TestEquality might have made a mistake going with "if and only if"!

[phadej]

Frankly, it sounds like TestEquality might have made a mistake going with "if and only if"!

If and only if is fine for singleton types, in fact I makes TestEquality more useful in that case.