Clarify laws of TestEquality #21

Ericson2314 · 2021-12-01T20:27:19Z

(See obsidiansystems/dependent-sum#31 and GaloisInc/parameterized-utils#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!

The text was updated successfully, but these errors were encountered:

Bodigrim · 2021-12-01T21:41:44Z

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 · 2021-12-02T00:48:43Z

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 · 2021-12-17T12:04:23Z

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 · 2021-12-17T23:41:03Z

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 · 2021-12-18T18:37:34Z

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 · 2021-12-19T19:35:48Z

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 · 2021-12-20T20:05:24Z

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 · 2021-12-21T20:19:33Z

@robdockins OK just wanted to make sure one of you knew, so thank for chiming in. As I wrote in GaloisInc/parameterized-utils#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 · 2021-12-21T20:28:17Z

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 · 2022-01-12T00:35:18Z

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.

It is unclear what `TestEquality` is for. There are 3 possible choices. Assuming ```haskell data Tag a where TagInt1 :: Tag Int TagInt2 :: Tag Int ``` `Just Refl` merely means the type params are equal, the values being compared might not be ```haskell instance TestEquality where testEquality TagInt1 TagInt1 = Just Refl testEquality TagInt1 TagInt2 = Just Refl testEquality TagInt2 TagInt1 = Just Refl testEquality TagInt2 TagInt2 = Just Refl ``` `Just Refl` means the type params are equal, and the values are equal according to `Eq`. ```haskell instance TestEquality where testEquality TagInt1 TagInt1 = Just Refl testEquality TagInt2 TagInt2 = Just Refl testEquality _ _ = Nothing ``` - `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. ```haskell -- instance TestEquality -- invalid instance because two variants for `Int` ``` ------ The discussion in haskell/core-libraries-committee#21 on this topic is veering towards the weakest option so that is what is implementing here, so that is what I am implementing. The committee will vote on this change.

It is unclear what `TestEquality` is for. There are 3 possible choices. Assuming ```haskell data Tag a where TagInt1 :: Tag Int TagInt2 :: Tag Int ``` ## Weakest -- type param equality only `Just Refl` merely means the type params are equal, the values being compared might not be ```haskell instance TestEquality where testEquality TagInt1 TagInt1 = Just Refl testEquality TagInt1 TagInt2 = Just Refl testEquality TagInt2 TagInt1 = Just Refl testEquality TagInt2 TagInt2 = Just Refl ``` ## Middle -- Like `Eq` `Just Refl` means the type params are equal, and the values are equal according to `Eq`. ```haskell instance TestEquality 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. ```haskell -- instance TestEquality -- invalid instance because two variants for `Int` ``` ------ The discussion in haskell/core-libraries-committee#21 on this topic is veering towards the weakest option so that is what is implementing here, so that is what I am implementing. The committee will vote on this change.

Ericson2314 · 2022-01-12T01:04:49Z

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 · 2022-01-13T21:00:37Z

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 · 2022-01-13T21:05:21Z

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

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

Bodigrim · 2022-01-13T21:16:02Z

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

Ericson2314 · 2022-01-13T22:46:16Z

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 · 2022-01-13T23:02:42Z

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 · 2022-01-13T23:14:03Z

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 · 2022-01-13T23:15:11Z

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 · 2022-01-13T23:22:57Z

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 · 2022-01-13T23:38:30Z

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 · 2022-01-14T00:14:02Z

@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 · 2022-01-14T16:35:34Z

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 · 2022-01-14T17:27:31Z

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 · 2022-01-14T18:07:42Z

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 · 2022-01-15T00:01:26Z

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 · 2022-01-15T00:09:35Z

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 · 2022-01-15T04:00:15Z

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 <#21 (comment)>, 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 · 2022-01-19T00:09:37Z

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

Bodigrim · 2022-01-19T01:34:21Z

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

mixphix · 2022-01-19T17:26:38Z

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

chessai · 2022-01-22T02:45:57Z

+1 to the weakest semantics described in the MR

Bodigrim · 2022-01-22T18:33:24Z

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

Bodigrim · 2022-01-29T11:55:21Z

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

cgibbard · 2022-01-29T18:00:35Z

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

Bodigrim · 2022-02-01T00:12:26Z

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

It is unclear what `TestEquality` is for. There are 3 possible choices. Assuming ```haskell 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. ```haskell 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: ```haskell data Tag' a where TagInt1 :: Tag Int TagInt2 :: Tag a ``` ```haskell 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. ```haskell 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`. ```haskell 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. ```haskell -- instance TestEquality -- invalid instance because two variants for `Int` ``` ------ The discussion in haskell/core-libraries-committee#21 on this topic is veering towards the weakest option so that is what is implementing here, so that is what I am implementing. The committee will vote on this change.

It is unclear what `TestEquality` is for. There are 3 possible choices. Assuming ```haskell 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. ```haskell 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: ```haskell data Tag' a where TagInt1 :: Tag Int TagInt2 :: Tag a ``` ```haskell 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. ```haskell 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`. ```haskell 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. ```haskell -- instance TestEquality -- invalid instance because two variants for `Int` ``` ------ The discussion in haskell/core-libraries-committee#21 has decided on the "Weaker" option (confusingly formerly called the "Weakest" option). So that is what is implemented.

chshersh · 2023-03-16T12:32:56Z

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 🙂

Ericson2314 mentioned this issue Dec 1, 2021

Make GEq = TestEquality (or not?) obsidiansystems/dependent-sum#31

Closed

Ericson2314 mentioned this issue Dec 2, 2021

TestEquality haskellari/some#16

Closed

Ericson2314 mentioned this issue Dec 18, 2021

TestEquality dangerous for value equality (e.g. MapF) GaloisInc/parameterized-utils#63

Closed

RyanGlScott mentioned this issue Jan 5, 2022

Build failure with hashable-1.4.0.0 GaloisInc/parameterized-utils#126

Closed

Bodigrim closed this as completed Feb 1, 2022

Bodigrim added the approved Approved by CLC vote label Feb 1, 2022

This was referenced Apr 9, 2022

Clarify laws of TestCoercion #53

Closed

Better docs to distinguish from TestEquality haskellari/some#47

Closed

chshersh added the base-4.17 Implemented in base-4.17 (GHC 9.4) label Mar 16, 2023

Clarify laws of TestEquality #21

Clarify laws of TestEquality #21

Comments

Ericson2314 commented Dec 1, 2021 • edited Loading

Weakest -- type param equality semi-decidable

Weaker -- type param equality decidable

Strong -- Like Eq

Strongest -- unique value concrete type

Bodigrim commented Dec 1, 2021

Ericson2314 commented Dec 2, 2021

Jashweii commented Dec 17, 2021 • edited Loading

Bodigrim commented Dec 17, 2021

Ericson2314 commented Dec 18, 2021 • edited Loading

Jashweii commented Dec 19, 2021

robdockins commented Dec 20, 2021

Ericson2314 commented Dec 21, 2021 • edited Loading

robdockins commented Dec 21, 2021

Bodigrim commented Jan 12, 2022

Ericson2314 commented Jan 12, 2022

Bodigrim commented Jan 13, 2022

treeowl commented Jan 13, 2022

Bodigrim commented Jan 13, 2022

Ericson2314 commented Jan 13, 2022

robdockins commented Jan 13, 2022

Ericson2314 commented Jan 13, 2022 • edited Loading

treeowl commented Jan 13, 2022

Ericson2314 commented Jan 13, 2022 • edited Loading

robdockins commented Jan 13, 2022

Ericson2314 commented Jan 14, 2022

cgibbard commented Jan 14, 2022

robdockins commented Jan 14, 2022

Ericson2314 commented Jan 14, 2022

Bodigrim commented Jan 15, 2022

Ericson2314 commented Jan 15, 2022 • edited Loading

cgibbard commented Jan 15, 2022 via email

Ericson2314 commented Jan 19, 2022

Bodigrim commented Jan 19, 2022

mixphix commented Jan 19, 2022

chessai commented Jan 22, 2022

Bodigrim commented Jan 22, 2022

Bodigrim commented Jan 29, 2022

cgibbard commented Jan 29, 2022

Bodigrim commented Feb 1, 2022

chshersh commented Mar 16, 2023

Ericson2314 commented Dec 1, 2021 •

edited

Loading

Strong -- Like `Eq`

Jashweii commented Dec 17, 2021 •

edited

Loading

Ericson2314 commented Dec 18, 2021 •

edited

Loading

Ericson2314 commented Dec 21, 2021 •

edited

Loading

Ericson2314 commented Jan 13, 2022 •

edited

Loading

Ericson2314 commented Jan 13, 2022 •

edited

Loading

Ericson2314 commented Jan 15, 2022 •

edited

Loading