Clarify laws of TestEquality

[Ericson2314]

(See https://github.com/obsidiansystems/dependent-sum/issues/31 and https://github.com/GaloisInc/parameterized-utils/issues/63 for some background.)

It is unclear what TestEquality is for. There are 3 possible choices.

Assuming

data Tag a where
    TagInt1 :: Tag Int
    TagInt2 :: Tag Int

Weakest -- type param equality semi-decidable

Just Refl merely means the type params are equal, the values being compared might not be. Nothing means the type params may or may not be not equal.

instance TestEquality Tag where
    testEquality TagInt1 TagInt1 = Nothing -- oopsie is allowed
    testEquality TagInt1 TagInt2 = Just Refl
    testEquality TagInt2 TagInt1 = Just Refl
    testEquality TagInt2 TagInt2 = Just Refl

This option is better demonstrated with a different type:

data Tag' a where
    TagInt1 :: Tag Int
    TagInt2 :: Tag a

instance TestEquality Tag' where
    testEquality TagInt1 TagInt1 = Just Refl
    testEquality TagInt1 TagInt2 = Nothing -- can't be sure
    testEquality TagInt2 TagInt1 = Nothing -- can't be sure
    testEquality TagInt2 TagInt2 = Nothing -- can't be sure

Weaker -- type param equality decidable

Just Refl merely means the type params are equal, the values being compared might not be. Nothing means the type params are not equal.

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

Strong -- Like Eq

Just Refl means the type params are equal, and the values are equal according to Eq.

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

Strongest -- unique value concrete type

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.

-- instance TestEquality -- invalid instance because two variants for `Int`

---

I don't care that much which choice is made, as long as a choice is made!

[Bodigrim]

https://hackage.haskell.org/package/base-4.14.0.0/docs/Data-Type-Equality.html#t:TestEquality says "Conditionally prove the equality of a and b", where a and b are types. It does not say anything about terms and does not require Eq a, so in my eyes it means the weakest type of equality.

An interesting question is whether we allow individual instances to return false negatives (= operate under stricter rules). I think it is fine: maybe types are equal, but testEquality is not clever enough to find a proof.

[Ericson2314]

Yes the first part implies the weakest, and only

Typically, only singleton types should inhabit this class.

hints at the strongest. Nothing hints the middle.

The false negatives question is good too, thanks.

[Jashweii]

The key monad is a good example of something that relies on weakest equality and produces false negatives.

instance TestEquality (Key s)
instance Monad (KeyM s)
newKey :: KeyM s (Key s a)
runKeyM :: (forall s . KeyM s a) -> a

Key is realistically an Int, and KeyM state linear in an Int. (Depending what you want to do with your keys, in my case I wanted them in wrapped IntMaps and IntSets.) TestEquality just checks the two keys are equal, else (possibly false negative) doesn't return an equality.

I can imagine uses for weakest equality like closed operations where you don't mind if the values differ but require the same type. In fact you can recover the utility of strongest equality from weakest anyway:

-- really should be Eq (f a) | Eq (f b) =>
testEqual :: (TestEquality f, Eq (f a)) => f a -> f b -> Maybe (a :~: b)
testEqual a b = mfilter (\Refl -> a == b) (testEquality a b)

I guess you could have usual equivalence relation laws for TestEquality and TestCoercion, where the two arguments are related if they return Just Refl or Just Coercion.

[Bodigrim]

I assume this is a rare case, where we need CLC approval for documentation, because it clarifies semantics unexpressable otherwise. Since no one raised a voice in favor of options other than the weakest notion, could someone please to raise an MR for CLC to vote on?

[Ericson2314]

I am going to try to get some of the people from https://github.com/GaloisInc/parameterized-utils to chime in here, as the "weakest" direction is a bit contrary form their current documented laws, though not in a fundamental way. (They are doing the exact same thing as the classes from https://hackage.haskell.org/package/some)

[Jashweii]

Just wanted to add, if you exclude false negatives for the type parameter, you arrive at decidable equality for the type parameter. This implies returning Either (¬ eq) eq rather than Maybe eq, as in https://hackage.haskell.org/package/singletons-3.0.1/docs/Data-Singletons-Decide.html This would rule out the Key example, and if applied to TestCoercion would rule out potential instances TestCoercion IORef or TestCoercion (STRef s).

[robdockins]

For our use cases in parameterized-utils, it's important that we have the middle Eq-like equality. If TestEquality is going to mean something other than that, we will probably change to use a different class. Whether that is desirable or not, I don't know.

[Ericson2314]

@robdockins OK just wanted to make sure one of you knew, so thank for chiming in. As I wrote in https://github.com/GaloisInc/parameterized-utils/issues/62, I recommend using https://hackage.haskell.org/package/some for GEq for that, and there is more de-duplicating that can be done thereafter.

[robdockins]

Just wanted to add, if you exclude false negatives for the type parameter, you arrive at decidable equality for the type parameter. This implies returning Either (¬ eq) eq rather than Maybe eq, as in https://hackage.haskell.org/package/singletons-3.0.1/docs/Data-Singletons-Decide.html This would rule out the Key example, and if applied to TestCoercion would rule out potential instances TestCoercion IORef or TestCoercion (STRef s).

Indeed, I think if what is desired from testEquality is that it returns Just Refl if and only if the type parameters are equal, than it should return negative information in the alternate case, turning it into a decidable equality test for the type parameters, as suggested by @Jashweii.

[Bodigrim]

For our use cases in parameterized-utils, it's important that we have the middle Eq-like equality. If TestEquality is going to mean something other than that, we will probably change to use a different class. Whether that is desirable or not, I don't know.

In the absense of clarification in TestEquality description we must assume the weakest possible interpretation by default. Your use case is probably better served by GEq and friends.

I'd say that the wording "This class contains types where you can learn the equality of two types from information contained in terms" prohibits returning false negative answers: testEquality returns Just{} iff types are equal. Otherwise the type class becomes lawless and there are multiple possible definitions of testEquality (e. g., testEquality _ _ = Nothing is always valid).

One could raise a CLC proposal asking to change the semantics of TestEquality to a stricter one, which is IMO a viable proposal. Please clarify if there is such intention.

[Ericson2314]

Notion, could someone please to raise an MR for CLC to vote on?

I made https://gitlab.haskell.org/ghc/ghc/-/merge_requests/7333

[Bodigrim]

Dear CLC members, let's have a vote on https://gitlab.haskell.org/ghc/ghc/-/merge_requests/7333 @gwils @cgibbard @emilypi @cigsender @chessai

---

+1 from me.

[treeowl]

I know I'm coming really late, but I think either:

1. The type should be changed to provide a witness to inequality.
2. The weak option should be weakened further, so that Nothing means no type equality information is available.

[Bodigrim]

1. Change of type really deserves a separate proposal, because it is a breaking change for all users of TypeEquality.
2. As discussed above, this would make the class lawless and allowing more than one implementation.

[Ericson2314]

What is a good witness for inequality in Haskell? a :~ b -> Void is full of bottoms and can't be used by the type checker.

I do think "lawless" is too harsh plenty of classes (e.g. Monoid) have more than one possible instance. I still don't have much of a preference either way, but I think it is just more fair to give it another name.

[robdockins]

Just to chime in, I don't think I understand the "lawless" objection either. The class is already lawless in the sense that it doesn't have any stated laws (hence this discussion). I think probably everyone assumes the operation given should define some equivalence relation on the values in the family f, so the question is just: which equivalence relations should be acceptable for this class. Just from the type, it's clear that only equivalence relations where the type indices are equal can be accepted.

So, do we want to require that values be considered equivalent iff their types are equal? This seems unnecessarily strong to me, but is a reasonable stance. I agree with @Ericson2314 that negative type equality information isn't useful; in my mind this is a good reason to reject this requirement. I don't think that additional law enables any interesting programming patterns.

Then, we end up in the case that I think is most useful, which is that testEquality defines some equivalence relation on values, and if values are equivalent, then their types must be equal, but there may be values with equal types that are not equivalent. This makes perfect sense for the (AFAIK) original motivating example for GADTs in the first place; type-indexed abstract syntax and values. There's no particular reason to think that two values with the same type have to be equal.

[Ericson2314]

Hmm I thought original purpose was TypeRep / Typeable, where one does want full decidability. But doing some recursive git blaming through many renames, it seems it dates back to 98d6079706cb0e86aa9b36e7f904207cfe6cef88

---

Honestly, It might just be best to remove this from base. It's unclear what it's for or why it's there. This thing seems too half-baked to deserve to be in base.

some and dependent-{sum,map} already have their own, and parameterized-utils could use some to or define it's own.

Conversely, a class for singletons or Typeable should be at least elsewhere in base, or in the singletons package.

[treeowl]

So like tryTestEquality :: f a -> f b -> Maybe (a :~: b)? Fine. And then we may want things like

data Decision a = No (a -> Void) | Yes a
class DecidableEquality f where
  decideEquality :: f a -> f b -> Decision (a :~: b)

Getting type families to reduce is currently mostly impossible, but special cases could be handled like this:

type family a === b where
  a === a = True
  _ === _ = False

data EqualityRes a b where
  YesEqual :: EqualityRes a a
  NotEqual :: (a === b) ~ 'False => EqualityRes a b

class Blahblahblah f where
  yeppers :: f a -> f b -> EqualityRes a b

[Ericson2314]

Pulling out of base would allow us to experiment which of @treeowl's options are better for the full decidability use-case. I hope with things like https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3868 working with negated coercersions might start to get more ergonomic / useful, too.

[robdockins]

I don't think you need to pull TestEquality out of base to do those experiments. Instead, you could clarify that TestEquality has weaker requirements, and later add a different class with stronger laws if it is warranted/useful.

If the final judgment is that TestEquality is half-baked and should be removed anyway... OK, but I guess that will lead to code churn as alternatives with essentially the same type are chosen/invented.

[Ericson2314]

@robdockins one doesn't need to strictly speaking, yes, but the weakest option just isn't that useful IMO. it's a type class whose only purpose is to be subtypeclassed to better serve the two uses we've identified, one of which wants a generalized Eq, and the other of which wants full decidability.

While I personally want to see more super-fine-grained class hierarchies, Haskell itself isn't currently isn't set up very well for it, nor has base historically embraced it. I therefore think any "centipede mathematics" project of trying to codify the commonality between GEq and DecideTypeParamEquality should happen outside of base.

[cgibbard]

The current Haddocks for TestEquality seem reasonably clear that the intention of the class is to learn equalities of types from information contained in terms, and not to compare terms themselves for equality, though it also specifies that it should usually only have instances which are singletons, which makes that question a moot point.

Based on the documentation I'd support either the weakest interpretation, or discarding the class. We have GEq/GCompare for term equality that also learns about type equality as it goes. I wouldn't be wholly opposed to putting those in base, but I also wouldn't rush to do it, since that just makes working on them harder.

I'm not sure I've ever seen this TestEquality class put to use. If we were to just remove it, how much would break?

[robdockins]

Well, it would break a bunch of stuff at Galois. This class is used throughout our program analysis suite of tools, both for singleton-style type representatives, and for broader uses, as I've argued for above. If TestEquality is changed or removed, I will probably personally end up spending the better part of a week shepherding a complicated, interconnected series of PRs in at least 10 repositories to probably more than 50 packages to make the necessary coordinated changes.

I would implore the core library committee to make API-breaking changes to base only for very clear, compelling reasons. I don't see any here.

[Ericson2314]

I dont know when the policy for removing things from base is, but I would assume it would be deprecated first, then removed, to give people time and advanced notice.

@robdockins I also would volunteer to send PRs to your open source repos like parameterized-utils, because I am interested in seeing more Haskellers standardize around GEq/GCompare. I understand the open source ones are probably not the whole iceberg, but I hope that still helps.

[Bodigrim]

I'm not sure I've ever seen this TestEquality class put to use. If we were to just remove it, how much would break?

47 packages according to https://hackage-search.serokell.io/?q=TestEquality And I use it in private codebases as well.

I do not quite follow the discussion above. Are there specific non-breaking suggestions to incorporate in https://gitlab.haskell.org/ghc/ghc/-/merge_requests/7333 ?

[Ericson2314]

The discussion was an alternative of (deprecating and eventually) removing it altogether.

The search is nice, I suppose we can see what use-case is more common.

[cgibbard]

Yeah, in the case that people are getting use out of it, I'm fine with clarifying its meaning, but not with removal. GEq seems like an almost totally separate concept to me, that just happens to overlap in the case of singletons.

On Fri., Jan. 14, 2022, 19:09 John Ericson, @.***> wrote:

The discussion as an alternative of (deprecating and eventually) removing it altogether.

The search is nice, I suppose we can see what use-case is more common.

— Reply to this email directly, view it on GitHub https://github.com/haskell/core-libraries-committee/issues/21#issuecomment-1013553608, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABVVE3H3MRE3A4Y4IGVFXQ3UWC3MVANCNFSM5JFM5YHQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you were mentioned.Message ID: @.***>

[Ericson2314]

Looks like we just need some more votes on the PR as written, then?

[Bodigrim]

I think so. @cgibbard @gwils @chessai @emilypi @cigsender may I hear your opinion (and vote) please?

[mixphix]

I'm in favour of clarifying the semantics to the weakest definition as described in the MR. +1

[chessai]

+1 to the weakest semantics described in the MR

[Bodigrim]

@cgibbard @emilypi @cgibbard opinions please? We need one more vote to approve.

[Bodigrim]

@cgibbard @emilypi @gwils May I have your attention please?

[cgibbard]

+1 to clarifying the documentation without changing the meaning as it stands.

[Bodigrim]

With 4 votes out of 6 in favor, the proposal https://gitlab.haskell.org/ghc/ghc/-/merge_requests/7333 is approved. Thanks everyone.

[chshersh]

I'm trying to summarise the state of this proposal as part of my volunteering effort to track the progress of all approved CLC proposals.

Field	Value
Author	@Ericson2314
Status	merged
base version	4.17.0.0
Merge Request (MR)	https://gitlab.haskell.org/ghc/ghc/-/merge_requests/7333
Blocked by	nothing
CHANGELOG entry	missing (please, raise an MR to base to update changelog)
Migration guide	not needed

Please, let me know if you find any mistakes 🙂