Leibniz coercion

Recently Ryan Scott wrote an article about Leibniz (and Martin-Löf) equality. Interestingly we can do the same thing for coercions (which are representational equalities). That exercise stumbles on the first-orderness of role system in GHC, making it a good example to be solved. (I’d like to have a solution, but I only have a problem).

{-# LANGUAGE GADTs, RankNTypes, QuantifiedConstraints #-}
{-# LANGUAGE StandaloneKindSignatures, PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables, TypeOperators, TypeApplications #-}
import Data.Coerce (Coercible, coerce)
import Data.Kind (Type)
import Data.Functor.Identity (Identity (..))

The Coercion type defined in Data.Type.Coercion is akin to Martin-Löf equality (:~:):

type Coercion :: k -> k -> Type
data Coercion a b where
  Coercion :: Coercible a b => Coercion a b

compare that to alternative way¹ to write (:~:):

type (:~:) :: k -> k -> Type
data a :~: b where
  Refl :: a ~ b => a :~: b

There is an analog of castWith function, called coerceWith, a type-safe cast using representational equality:

coerceWith' :: Coercion a b -> a -> b
coerceWith' Coercion x = coerce x

Symmetry, transitivity etc combinators are defined similarly by pattern matching on the constructor.

#Leibniz coercion

What would Leibniz variant look like? Recall identity of indiscernibles: two objects are equal if and only if they satisfy the same properties. We encode that in Haskell as:

type (:=) :: k -> k -> Type
newtype a := b = Leibniz { subst' :: forall c. c a -> c b }

where c is all properties, or contexts. For Coercion we need to restrict that to the representational ² contexts. We can encode representational contexts using QuantifiedConstraints extension:

type Koerzion :: k -> k -> Type
newtype Koerzion a b = Koerzion
  { subst :: forall c. (forall x y. Coercible x y => Coercible (c x) (c y))
          => c a -> c b
  }

(Leibniz was German, and this is the first name I thought of. I do not know German, I’m sorry).

Another way to think about this is:

• Everything should respect the nominal equality.

• However, only representational things respect representational equality, i.e. coercions.

Next, lets defined define some basic combinators. Reflexivity is defined similarly as for the (nominal) Leibniz equality:

refl :: Koerzion a a
refl = Koerzion id

We can generalise it to arbitrary Coercible types, that is the point of coercions:

koerzion :: Coercible a b => Koerzion a b
koerzion = Koerzion coerce

The type-safe cast do not pose any problems either:

coerceWith :: Koerzion a b -> a -> b
coerceWith ab a = runIdentity (subst ab (Identity a))

With transitivity we step into a problem:

trans :: forall a b c. Koerzion a b -> Koerzion b c -> Koerzion a c
trans ab bc = subst bc ab

doesn’t work. Let’s ignore a problem for now, and follow David Feuer comment and defined transitivity as:

trans :: forall a b c. Koerzion a b -> Koerzion b c -> Koerzion a c
trans ab bc = Koerzion (subst bc . subst ab)

So far so good. We have defined reflexivity, transitivity, and type-safe cast.

#Symmetry

If we try to define symmetry, following the nominal Leibniz equality example:

type Symm :: k -> k -> Type
newtype Symm a b = Symm { unsymm :: Koerzion b a }

sym :: forall a b. Koerzion a b -> Koerzion b a
sym ab = unsymm (subst ab (Symm refl))

we get an error (which is similar to what we get in the first transitivity attempt):

    • Couldn't match representation of type: c y
                               with that of: c x
        arising from a use of ‘subst’

though I’d expected

    • Couldn't match representation of type: Symm a a
                               with that of: Symm a b
        arising from a use of ‘subst’

However, I believe that it caused by the same underlying reason: Koerzion roles are not representational:

*Main> :i Koerzion 
type role Koerzion nominal nominal nominal
type Koerzion :: forall k. k -> k -> *

In comparison, GADT variant Coercion is:

*Main> :i Coercion
type Coercion :: forall k. k -> k -> *
type role Coercion nominal representational representational

This highlights the first-orderness of the role system. Koerzion is morally representational in a and b, but GHC doesn’t want to infer it. (And there is no way to say trust me). The QuantifiedConstraints "hack" to internalize representational contexts is not integrated into roles system and Coercible constraint solver (AFAIK), so the things do not work out.

#Equivalence of Leibniz and Martin-Löf-like coercions

However, Coercion and Koerzion are equivalent:

toKoerzion :: Coercion a b -> Koerzion a b
toKoerzion Coercion = Koerzion coerce

fromKoerzion :: forall a b. Koerzion a b -> Coercion a b
fromKoerzion ab = subst ab @(Coercion a) (Coercion :: Coercion a a)

And we can define sym via that equivalence:

sym :: forall a b. Koerzion a b -> Koerzion b a
sym = toKoerzion . sym' . fromKoerzion

sym' :: Coercion a b -> Coercion b a
sym' Coercion = Coercion

which justifies my "Koerzion is morally representational" claim, because Coercion is representational, Koerzion should be too.

It would be very nice if GHC had higher-order roles. There are plenty of practical examples which run into the same problem (e.g. the core type in pipes is not representational in any of its type arguments, though it should be). But maybe this Koerzion example will nerd-snip someone to solve this problem :)

• 2024-04-18 – What makes a good compiler warning?
• 2024-04-12 – Core Inspection
• 2024-04-01 – Implicit arguments
• 2024-03-17 – ST with an early exit
• 2024-02-27 – More QualifiedDo examples

twitter github email linkedin stackoverflow