# Leibniz coercion

Posted on 2021-09-09 by Oleg Grenrus

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 way1 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 2 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).

• 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 :)

1. I’m not sure that the representation of this and original variant is exactly the same, i.e. whether the equality constraint is unboxed in both variants. That details is not important for us now.↩︎

2. Another Ryan’s blog post has a section about roles. GHC manual is also a good source of knowledge.↩︎

Site proudly generated by Hakyll