There are two tasks:
subst obey the equations
specified by
.
In particular, the version you wrote for one type is the same as the
version wrote for the other type with coercions inserted. Or maybe itʼs
the other way, the one you wrote with explicit coercions could have all
just been identities in some parallel universe.List,
Tsil,
Array
Weʼre not going to go in depth here (thatʼs what the rest of this article is for!), but we need to set some ground rules. We start with two Haskell definitions of type-equality:
newtype Leibniz a b = EquiConvertable (forall f. f a -> f b)
data x :~: y where
Refl :: z :~: zUnfortunately, we really need dependent types to explain HoTT, so we
canʼt just stick with Haskell and I will invoke Agda as necessary.
Mostly for syntactic convenience, since it is very helpful to
have a coherent syntax to talk about the concepts and types we are
discussing! Note that the main difference is the roles of : and :: are flipped in
Haskell vs Agda, as type annotation versus list constructor.I personally like the Agda convention better, but of
course I say that as a type theorist 😉. The
substantial programs will still be in Haskell.
Here are two equivalent definitions in Agda:
data _≡_ (x : Type) : Type -> Type where
refl : x ≡ x
data _≡_ : Type -> Type -> Type where
refl : (x : Type) -> x ≡ xNote that coercions in the sense of Haskellʼs Coercible are
a fascinating topic, but largely orthogonal to what we are talking about
here! We are going to ignore them for the rest of this article.
One could think of coercions as paths that compile down to the identity, but that requires referencing some underlying (runtime) model which we donʼt talk about in HoTT.
Instead we will talk about coercing along a path. This means
that given some path (p :: x :~: y)
we can write (coe p :: x -> y)
for the coercion along the path p.
Our goal is to explain path induction for types, which is also
referred to as Axiom
for historical reasons. Hereʼs the type of Axiom
(specialized to Type):
J :
(x : Type) ->
(P : (y : Type) -> x ≡ y -> Type) ->
P x refl ->
(y : Type) ->
(p : x ≡ y) ->
P y pThis says:
(x : Type),(P : (y : Type) -> x ≡ y -> Type)
ranging over possible second types (y : Type)
and equality proofs x ≡ y,P x refl
holds,(y : Type)(p : x ≡ y),p too: P y p. This is just from the fact that it
held at refl, which is what
everyone finds surprising!Letʼs pick this apart a bit more and put it into a programming context.
P is going to be like a schema for
programs varying along an abstract interface. For example, we could take
P yx is the one that our programs expect
to use, while y will be the type they are
given.x ≡ y.Original monomorphic program. Type family that specifies what we want to target.
There are a few related meanings of functors that we need to disentangle before we go further.
The simplest meaning: anything of kind Type -> Type.
More broadly: any type-level function.
The next simplest is our beloved Functor
typeclass:
class Functor f where
fmap :: forall a b. (a -> b) -> f a -> f b
There are also related classes: Contravariant,
Invariant,
Phantom.
Thereʼs a fifth I want to include for completeness: EquiFunctor,
which I will explain later. Itʼs a folklore result that any standard
functor (in the first sense) will satisfy one of these classes.
class Contravariant f where
contramap :: forall a b. (a -> b) -> f b -> f a
class Invariant f where
invmap :: forall a b. (a -> b) -> (b -> a) -> f a -> f b
class Phantom (f :: Type -> Type) where
coerce :: forall a b. f a -> f b
class EquiFunctor (f :: Type -> Type) where
equimap :: forall a b. Leibniz a b -> f a -> f b
Finally we have the category-theoretic notion of Functor, which goes much much further. We will not try to model the full scope of this in Haskell, but it is good to know that there is an underlying concept that unifies all of the above.
Letʼs explore.