Heterogeneous-comparison - Comparison of distinctly typed values with evidence capture

Announcements
1

heterogeneous-comparison

There are times when values need to be tested for equality or compared for ordering, even if they aren’t statically known to be of equivalent types.
Such a test, if successful, may allow that knowledge to be recovered.

Prior Art

base (on singletons):

  • TestCoercion f \approx (HetEq f, Strength f ~ Representational)
  • TestEquality f \approx (HetEq f, Strength f ~ Nominal)

some (universally):

  • GEq f \cong (HetEq f, Strength f ~ Nominal)
  • GCompare f \cong (HetOrd f, Strength f ~ Nominal)

Improvements

HetEq and HetOrd are generalised over the strength of evidence captured.
This allows them to admit and combine a much broader range of instances, e.g.

instance Eq a => HetEq (Const a) where
  type Strength (Const a) = Phantom
  ...
instance HetEq IORef where
  type Strength IORef = Representational
  ...
instance HetEq TypeRep where
  type Strength TypeRep = Nominal
  ...

type HetEq' f = (KnownRole (Strength f), HetEq f)

instance (HetEq' f, HetEq' g) => HetEq (Product f g) where
  type Strength (Product f g) = Max (Strength f) (Strength g)
  ...
instance (HetEq' f, HetEq' g) => HetEq (Sum     f g) where
  type Strength (Sum     f g) = Min (Strength f) (Strength g)
  ...

Consequently, Data.Hetero.Some has much broader Eq and Ord instances than Data.Some:

instance HetEq  f => Eq  (Some f)
instance HetOrd f => Ord (Some f)

dependent-map could similarly broaden the range of key types by replacing GCompare k with (HetOrd k, Strength k > Phantom), though the rare operations requiring Has' _ k f constraints might not come out on top.

4 Likes
2

Are there times like that? If a program is comparing two values, that’s strong evidence to me that the programmer (at least) believes they’re the same type. If there’s some fancy potentially-disparate type trickery going on, I’d expect (the equivalent of) a type equality test with instance despatch.

Talk of “strength” suggests wiggle room between:

  • Equal, therefore same type;
  • NotEqual although same type;
  • Equality is meaningless/inappropriate, because distinct types.
3

Yes. Such times come when type information is discarded. As the readme should suggest, Some f and DMap k f both present use-cases for discarding and recovering type information. Another case that springs to mind is in the exception handling mechanism of bluefin (which effectful should also use).

The programmer has reason to believe two values may be the same, and it may then follow that their types are related, but they don’t know until they compare them. When they do, if the answer is yes, they’d like the type checker to recognise that relation.

There are three equivalence relations on types that are of relevance here: nominal, representational, and trivial/universal/“phantom”. They’re in strict hierarchy, with each implying the next. I only use “strength” to refer to positions in this hierarchy.

type Strength f :: RoleKind

Does not correspond precisely to the role signature of f according to GHC, but rather a lower bound on the Strength of the evidence gleaned from a positive equality test.

  • Comparing a Const a x and a Const a y, you can tell if they’re equivalent by comparing the as, but you can’t say anything meaningful about x and y, only that they’re related in the most trivial way.
  • Comparing an IORef a and an IORef b, you can tell if they’re equivalent by comparing the underlying pointers. Since IORefs are subject to safe coercions you can’t say a ~ b, but you know they’re representationally equivalent.
  • Comparing a TypeRep a and a TypeRep b, you can tell if they’re equivalent by comparing their internal structure. Since that structure reflects a and b precisely, you can then learn that a ~ b.
4 Likes