Make it clearer that `Geq` is also about value equality

[jeltsch]

Currently (that is, as of version 1.0.6), the documentation of Geq, including the one of its geq method, doesn’t seem to mention what geq is primarily about: checking of value equality. From what I understand, geq is a heterogeneous equality operator (checking equality of values whose type’s type parameters may differ) with the additional feature that it yields a witness of type parameter equality whenever the given values are equal. The present documentation, however, presents Geq and geq as essentially being about type equality (“decide the equality of types”, “produce a witness of type-equality”). It delves quickly into a comparisons with TestEquality, which isn’t very useful for people like me, who haven’t yet heard about this other class. However, only in this comparison I found hints that geq actually checks value equality. In my opinion, this should be mentioned much more prominently, perhaps similar to how I described geq above:

geq is a heterogeneous equality operator (checking equality of values whose type’s type parameters may differ) with the additional feature that it yields a witness of type parameter equality whenever the given values are equal.

That said, it should be noted that a full heterogeneous equality operator would probably allow the types of its arguments to be arbitrary; so maybe a more refined characterization of geq should be found.

[phadej]

The underlying question is, did you look for something like geq but the documentation made it unclear it is what you are looking for; or did you look for something else and mistakenly used geq?

[jeltsch]

I actually wanted to make Some with a particular type parameter an instance of Eq, saw that my instantiation clashed with an existing one, and then started to research what this existing one was about. As a result, I wanted to understand what geq is doing. So I didn’t search for some particular operation, although it turned out later that geq is indeed useful in my situation.

No matter the background, I’d say that it is important for the documentation of Geq and particularly geq to more prominently mention the fact that a comparison of values is conducted, simply because it’s an important part of what geq is doing, beside the establishment of type equality in case of value equality. The current documentation actually caused me to initially dismiss Geq and geq as not being useful in my case, and only when pondering a bit about them later I suddenly realized that I had been wrong.

[phadej]

Eq Some will use EqP in the next major release of some. I probably should make that soon.

When that change is done, I may alter documentation a bit. EqP will become a superclass of GEq, and the law eqp x y = True <=> geq x y == Just Refl will formally say that geq is about value equality.

[jeltsch]

Eq Some will use EqP in the next major release of some. I probably should make that soon.

When that change is done, I may alter documentation a bit. EqP will become a superclass of GEq, and the law eqp x y = True <=> geq x y == Just Refl will formally say that geq is about value equality.

Sounds good. 🙂