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^{1} 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.
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).
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.
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.
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 :)
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.↩︎
Another Ryan’s blog post has a section about roles. GHC manual is also a good source of knowledge.↩︎