search

obsidiansystems / dependent-sum

Dependent sums and supporting typeclasses for comparing and displaying them
54 stars 39 forks source link

Make GEq = TestEquality (or not?) #31

Closed phadej closed 3 years ago

phadej commented 5 years ago

The classes seem to be exactly the same.

This class contains types where you can learn the equality of two types from information contained in terms. Typically, only singleton types should inhabit this class.

If the point is to differentiate cases like:

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

instance GEq Tag where
    geq TagInt1 TagInt1 = Just Refl
    geq TagInt2 TagInt2 = Just Refl
    geq _ _ = Nothing

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

than it should be pointed out in the documentation of GEq. As dependent-sum is GHC >= 8.0, TestEquality is always available.

ryantrinkle commented 5 years ago

Yeah, GEq would definitely expect those two to be unequal, and it would be good if that were clearer. It's not clear to me what TestEquality is expecting, but your implementation looks reasonable to me here.

We could even specify that GEq is just TestEquality + Eq, but with a more (possibly) efficient implementation.

Ericson2314 commented 5 years ago

@phadej hah! I hadn't seen this issue before, but wish I had. I made https://github.com/GaloisInc/parameterized-utils/issues/62 https://github.com/GaloisInc/parameterized-utils/issues/63 after comparing the libraries, and we ended up rehashing all of the conversation in this thread in person.

@dbornside just now points out that maybe

Typically, only singleton types should inhabit this class.

Means that "typically" one would have:

(testEquality a b = Just Refl) => a == b

i.e. every value would have a different index. That would make TestEquality a stronger, not weaker class.

Ah! base just needs some new docs. I care more that the class is described well than about what it does; downstream can adapt.

Ericson2314 commented 3 years ago

The ambiguity is with base so I am throwing this to the CLC: https://github.com/haskell/core-libraries-committee/issues/21 . Once they have a decision, we can adjust accordingly.