Kind-indexed abstract type representation

Learn
1

I find myself in want of something like this:

-- | An abstract, kind-indexed representation of a type, with
-- type constructors taken from `f`.
data ARep f k where
  ARLift ∷ f k → ARep f k
  (:$) ∷ ARep f (k₁ → k₂) → ARep f k₁ → ARep f k₂
deriving stock instance (∀ k'. Show (f k')) ⇒ Show (Rep f k)

instance TestEquality f ⇒ TestEquality (ARep f) where
  testEquality = \cases
    (ARLift a) (ARLift b) → a `testEquality` b

    (f :$ a) (g :$ b)
      | Just Refl ← f `testEquality` g
      , Just Refl ← a `testEquality` b
        → Just Refl

    _ _ → Nothing

There’s no issue with this code from my POV but it seems unlikely that I’d be the first person to write it. Has anyone seen this in a library somewhere?

(Edit: I managed to no longer use that awkward constructor constraint, in case that shakes anything loose.)

1 Like
2

Is this a sort of generalized applicative?

3

Perhaps, but from that perspective it is generalized beyond the expectation of associativity, as A (B C) and A B C are different types. Is a ‘unital magmoidal functor’ a thing?

1 Like