description of category laws in Idris

Cat.lidr

# Category Theory proofs in Idris

Idris is a language with dependent types, and is similar to Agda.
What distinguishes Idris is that it is intended to be a general-purpose language first,
and a theorem prover second.
To that end it supports optional totality checking
and features to support writing DSLs:
type classes,
do notation,
monad comprehensions (i.e., a more general form of list comprehension),
and idiom brackets.
It also supports multiple compilation targets,
including C and Javascript.

> module Cat

> import Control.Isomorphism
> import Decidable.Order
> import Data.Morphisms

Partial functions are allowed by default.
A totality requirement can be specified per-function.
This line enforces totality checking by default for functions in this module.

> %default total

According to the Curry-Howard correspondence,
mathematical propositions can be represented in a program as types.
An implementation of a type serves as a proof of the corresponding proposition.
In other words, inhabited types represent true propositions.

For example, consider the definition of the natural number type
in the Idris standard library:

~~~~ {.sourceCode .literate .haskell}
%elim data Nat = Z | S Nat
~~~~

There are two constructors given: a number may be zero (`Z`),
or it may be one greater than another number (`S Nat`).

A type that expresses that one natural number is
greater-than-or-equal-to another can be defined like this:

> data GTE'  : (n, m : Nat) -> Type where
>   gteZero : GTE' left Z
>   lteSucc : GTE' left right -> GTE' (S left) (S right)

The syntax is similar to the syntax provided by the GADTs extension in Haskell.
This declares that `GTE'` is a constructor that takes two `Nat` values as parameters,
and produces a `Type`.
It should be read,
"the natural number n is greater than or equal to the natural number m".

There are also two value constructors given.
They are written so that a value can be written that satisfies a given `GTE'` type
if and only if the `n` in that type is less than or equal to the `m`.
In this way, a value that satisfies a type of the form `GTE' n m`
is a proof that `n` is really less than or equal to `m`.

`gteZero` is a singleton value - it is a constructor that takes no arguments.
But its type contains a variable; so it is polymorphic.
It can satisfy any type of the form, `GTE' n Z`.
`gteZero` is effectively an axiom, stating a fundamental property of natural numbers.

Given the definition of `GTE'` it is possible to write a proposition,
such as, "every natural number is greater than or equal to zero".

> nonNegative : (n : Nat) -> GTE' n Z

The proposition is written as a function that takes a number as input.
To write an implementation for `nonNegative`,
it is necessary to produce a value of the appropriate `GTE'` type
without any information about what input might be given,
other than the fact that it will be a natural number.
Totality checking is enabled,
so any implementation must be applicable to every possible input.
Thus a type of the form,
`(x : A) -> P x` describes universal quantification over the type `A`.

`nonNegative` happens to be a restatement of the axiom, `gteZero`.
So an implementation / proof is trivial:

> nonNegative n = gteZero

On the other hand, `lteSucc` maps a given proof to a proof of a related proposition.
It is used in proofs-by-induction.


## Definition of Category

The type system in Idris is sufficiently expressive that most
—if not all—mathematical propositions can be represented.
Diving right in, let's write a definition of a category.
A category requires objects and arrows;
so we have a type class that starts with those.

> class Category obj (arr : obj -> obj -> Type) where

In this definition arrows are *indexed* by objects.
That is, the type of an arrow carries its domain and its codomain.
Note that `obj` is given as an unqualified variable.
In some categories objects will be types—as in the Set category.
In others they will be plain values.
In those categories the type of an arrow *depends* on values.

Arrows must be composable (if they have compatible domain and codomain).
And every object must have a corresponding id arrow.

>   cId   : (a : obj) -> arr a a
>   cComp : {a, b, c : obj} -> arr b c -> arr a b -> arr a c

As was shown above,
a function type serves as a proposition with universal quantification.
So the type of `cId` states that every object must be both the domain
and codomain of at least one arrow.
The implementation will also provide a means to identify that arrow.

Arguments in curly braces are implicit parameters.
In most cases the compiler will infer those values.
So they are generally not given as explicit arguments when invoking the function.
However, it is possible to provide implicit parameters explicitly when needed.

The use of colons in the above types might be unfamiliar.
They label argument positions so that the argument _value_ can be
referenced later in the type.
Wherever you see `(a : A)` it can be read as:
"some value of type `A` will be given here,
and that value will be assigned to the variable `a`".

`cId` and `cComp` are the only required operations.
But it is necessary to provide more specific rules about how they behave.

~~~~ {.sourceCode .literate .haskell}
  cIdLeft  : {a, b : obj} -> (f : arr a b) -> cId b `cComp` f     = f
  cIdRight : {a, b : obj} -> (f : arr a b) ->     f `cComp` cId a = f
~~~~

These propositions state that id arrows must not only have the same
object as domain and codomain,
they must also be identities under composition.
Implementations of `cIdLeft` and `cIdRight` will never be used at runtime.
They are just proofs that `cId` and `cComp` obey the category laws.

Here `(=)` is a type constructor, very much like `GTE'`.
Its definition looks like this:

~~~~ {.sourceCode .literate .haskell}
data (=) : a -> b -> Type where
  refl : x = x
~~~~

The parameters to `(=)` can be an expressions—including plain values or types.
`refl` is another axiom stating that equality is reflexive.
Basically, to prove that two expressions are equivalent
it is necessary to demonstrate to the type checker that
they have the same normal form.

One more proof is required to complete the `Category` type class.
Arrow composition must be associative.

~~~~ {.sourceCode .literate .haskell}
  cCompAssociative : (f : arr a b) -> (g : arr b c) -> (h : arr c d) ->
                     h `cComp` (g `cComp` f) = (h `cComp` g) `cComp` f
~~~~

I have cheated slightly.
In the types for `cIdLeft`, `cIdRight`, and `cCompAssociative`
I left the implicit arguments to `cComp` implicit.
But I was not able to get those definitions to type-check.
I actually had to give the implicit parameters explicitly
when applying `cComp` in a type expression.
I think that the definitions that actually work are more difficult to read:

>   cIdLeft  : {a, b : obj} -> (f : arr a b) -> cComp {a=a} {b=b} {c=b} (cId b) f = f
>   cIdRight : {a, b : obj} -> (f : arr a b) -> cComp {a=a} {b=a} {c=b} f (cId a) = f
>
>   cCompAssociative : (f : arr a b) -> (g : arr b c) -> (h : arr c d) ->
>                      cComp {a=a} {b=c} {c=d} h (cComp {a=a} {b=b} {c=c} g f) =
>                        cComp {a=a} {b=b} {c=d} (cComp {a=b} {b=c} {c=d} h g) f


## A partial ordering category

With the definition of a category in place,
it is possible to describe specific categories—
and to prove that they obey the category laws.

The Idris standard library includes an `LTE` type
that is very similar to the `GTE'` type described earlier.

~~~~ {.sourceCode .literate .haskell}
data LTE  : (n, m : Nat) -> Type where
  lteZero : LTE Z    right
  lteSucc : LTE left right -> LTE (S left) (S right)
~~~~

This can be used to describe a category where arrows are `LTE` relations,
and objects are natural numbers.

> instance Category Nat LTE where
>   cId Z     = lteZero
>   cId (S k) = lteSucc (cId k)

An id arrow in this category is a proof that a number is less than or equal to itself.
The proof that zero is equal to zero is given by the `lteZero` axiom.
Id arrows for other numbers are computed in an inductive step.

Arrow composition is a proof that the less-than-or-equal-to relation is transitive.
For reference, here is the type for `cComp` specialized for `LTE`:

~~~~ {.sourceCode .literate .haskell}
  cComp : {a, b, c : Nat} -> LTE b c -> LTE a b -> LTE a c
~~~~

And the proof construction:

>   cComp _ lteZero = lteZero
>   cComp (lteSucc f) (lteSucc g) = lteSucc (cComp f g)

In the first equation, the second input is `lteZero`;
which implies that `a` is zero.
`a` is also the domain in the `LTE` result that we want to prove;
so the proof is trivial.
The second equation takes advantage of the fact that the `lteSucc`
constructors of input arrows can be recursively unwrapped,
until reaching the base case, where the second input is `lteZero`.

There is no pattern for a case where the first input is `lteZero`
where the second is not.
It is not required, because that case is not allowed by the type of `cComp`,
and the type checker is able to confirm that.
If it were necessary to make explicit that this case is not possible,
that could be stated with a third equation:

~~~~ {.sourceCode .literate .haskell}
  cComp lteZero (lteSucc g) impossible
~~~~

The keyword `impossible` is one tool available for proofs of falsehood.

Now to prove the remaining category laws.

>   cIdLeft lteZero     = refl
>   cIdLeft (lteSucc f) = cong $ cIdLeft f
>
>   cIdRight lteZero     = refl
>   cIdRight (lteSucc f) = cong $ cIdRight f

Demonstrating identity under composition of proofs is a little strange.
What we need to show is that composing an identity arrow with any other arrow
does not introduce new information.

In the base case if `cIdLeft`, if the given arrow, `f`, is `lteZero`
then its domain must be zero.
Therefore the identity arrow it is composed with must also be `lteZero`.
Those are the same normal form,
so the proof invokes `refl`—the axiom of reflexivity of equality.

The inductive step applies `cong`,
which is a proof of congruence of equal expressions.
It is defined in the standard library:

~~~~ {.sourceCode .literate .haskell}
cong : {f : t -> u} -> (a = b) -> f a = f b
cong refl = refl
~~~~

In this case the `f` that `cong` infers as its implicit parameter is `lteSucc`.

`cong` is an example of a proof constructor:
it takes a proof as input and returns a proof of a related proposition.
Functions like `cong` are the building blocks of multi-step proofs.
This is also an example of the principle that types of the form,
`P x -> Q x`
can be read as logical implication.

You may notice that `cong` takes `refl` as an argument and returns it.
`cong` has equality proofs as its input and output.
By definition, the only possible value of an equality type is `refl`.

The base case of `cIdRight` is not as trivial as the base case of `cIdLeft`.
the codomain of `lteZero` is not necessarily zero;
so the identity arrow involved could be some `lteSucc` value.
However the compiler is able to do some normalization automatically.
That means that it is not necessary to spell out every step.

>   cCompAssociative lteZero _ _ = refl
>   cCompAssociative (lteSucc f') (lteSucc g') (lteSucc h') =
>     cong $ cCompAssociative f' g' h'

The proof of associativity follows a similar pattern.


## Iavor's simple category

Iavor demonstrated a category with just one object,
which he arbitrarily represented with `()`,
where the arrows are integers.

Here is my translation.
I have used natural numbers instead of integers
because the Idris standard library has a lot of ready-made proofs for naturals.
It has a recursive definition for integers that could be used instead—
that would just be more work.

This category is made a bit complicated by the choice of requiring that
arrows be indexed by domain and codomain.
Those indexes will not be meaningful in a category with just one object.
For the sake of generality,
a trivial higher-kinded wrapper around `Nat` is needed.

> data NatArrow : () -> () -> Type where
>   getNat : Nat -> NatArrow () ()

To make it clear that a `NatArrow` is really just a `Nat`,
we can prove that the two types are isomorphic.

> isoNatNatArrow : Iso Nat (NatArrow () ())
> isoNatNatArrow = MkIso to from toFrom fromTo where
>   to : Nat -> NatArrow () ()
>   to = getNat
>
>   from : NatArrow () () -> Nat
>   from (getNat n) = n
>
>   toFrom : (y : NatArrow () ()) -> to (from y) = y
>   toFrom (getNat y) = refl
>
>   fromTo : (x : Nat) -> from (to x) = x
>   fromTo x = refl

An isomorphism is a bidirectional mapping that preserves information in both directions.
`to` and `from` specify the mapping;
`toFrom` and `fromTo` prove that information is preserved.

It would be great if type class instances could be automatically derived
from isomorphism proofs.
There might be a feature along those lines that I am not aware of.

> instance Num (NatArrow () ()) where
>   (getNat x) + (getNat y) = getNat (x + y)
>   (getNat x) - (getNat y) = getNat (x - y)
>   (getNat x) * (getNat y) = getNat (x * y)
>   abs = id
>   fromInteger = getNat . fromInteger

Idris includes a number of type classes that are familiar to Haskell programmers,
including `Num` and `Integral`.

Now the definition of the Nat category:

> instance Category () NatArrow where
>   cId () = 0
>   cComp (getNat f) (getNat g) = getNat (f + g)
>
>   cIdLeft  (getNat f) = cong (plusZeroLeftNeutral  f)
>   cIdRight (getNat f) = cong (plusZeroRightNeutral f)
>   cCompAssociative (getNat f) (getNat g) (getNat h) =
>     cong (plusAssociative h g f)

This implementation uses `(+)` for arrow composition.
It reuses proofs of identity and associativity for `(+)`.
It is only necessary to apply `cong` to the predefined proofs
to show that applying the `getNat` constructor to both sides of an equality
does not change anything.


## Category of sets

In the Set category, objects are sets and arrows are functions.
The implementation here will use `Type` as the type of objects.
In Idris, the type of every small type is `Type`.

The definition of `Category` requires proofs of equivalence for arrows.
But there is no predefined comparison function for functions in Idris.
All that you can really do with a function is to give it some inputs,
and check what its outputs are.

To produce a viable category, it is necessary to introduce
the axiom of *function extensionality*:

> funext : (f, g : a -> b) -> ((x : a) -> f x = g x) -> f = g

If two functions produce the same output for all possible inputs,
then they are equivalent.

`funext` takes as input two functions
and a proof that those functions produce the same output for all inputs.
Note the parentheses in that type:
As function types serve as universal quantifiers,
higher-order functions provide a means to nest quantification
inside of larger propositions.

I am told that it is not possible to prove this proposition in Idris—
and that that limitation is not unique to Idris.
That is function extensionality must be given as an axiom:

> funext f g = believe_me

This is a "proof" to use sparingly.

Implementations for an identity function and for composition of functions
are provided in the standard library.
In fact, Idris includes a `Control.Category` module
with a predefined `Category` type class.
But that definition does not include all of the category laws.
Anyway, all that is left are proofs of identity and associativity.

> leftIdPoint : (f : a -> b) -> (x : a) -> id (f x) = f x
> leftIdPoint f x = refl
>
> rightIdPoint : (f : a -> b) -> (x : a) -> f (id x) = f x
> rightIdPoint f x = refl

Proving that `id (f x)` and `f (id x)` reduce to `f x`
is sufficiently easy that the compiler can do most of the work on its own.
To make the next step to `f x = f x -> f = f`
is just a matter of applying `funext`.

> leftId : (f : a -> b) -> id . f = f
> leftId f = funext (id . f) f $ leftIdPoint f
>
> rightId : (f : a -> b) -> f . id = f
> rightId f = funext (f . id) f $ rightIdPoint f

In order to prove associativity, it is helpful to have a helper proof
that could be described as, "pointful composition".

> compPoint : (f : b -> c) -> (g : a -> b) -> (x : a) -> f (g x) = (f . g) x
> compPoint f g x = refl

The proof of associativity is more complicated.
So it is broken in to steps here,
with proven intermediate propositions given for each step.

> compAssociative : (f : a -> b) -> (g : b -> c) -> (h : c -> d) ->
>                   h . (g . f) = (h . g) . f
> compAssociative f g h = qed where
>   step_1   : (x : _) -> h ((g . f) x) = (h . (g . f)) x
>   step_1   = compPoint h (g . f)
>
>   step_2   : (x : _) -> (h . (g . f)) x = h ((g . f) x)
>   step_2 x = sym (step_1 x)
>
>   step_3   : (x : _) -> (h . g) (f x) = ((h . g) . f) x
>   step_3   = compPoint (h . g) f
>
>   step_4   : (x : _) -> (h . (g . f)) x = ((h . g) . f) x
>   step_4 x = trans (step_2 x) (step_3 x)
>
>   qed      : h . (g . f) = (h . g) . f
>   qed      = funext (h . (g . f)) ((h . g) . f) step_4

There are two standard library functions used here that have not been introduced yet.
They are:

~~~~ {.sourceCode .literate .haskell}
sym : {l:a} -> {r:a} -> l = r -> r = l
sym refl = refl

trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
trans refl refl = refl
~~~~

When a free, lowercase variable appears in a type expression,
Idris assumes that the variable is a `Type`,
and inserts an additional implicit parameter at the beginning of the expression.
After carrying out that expansion, the type of `trans` looks like this:

~~~~ {.sourceCode .literate .haskell}
trans : {x, y, z : Type} -> {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
~~~~

There may be more steps listed in `compAssociative` than are really required.
Hopefully including them helps to clarify the proof.

In Haskell, `(->)` is an ordinary type constructor that could be used
as the arrow type in type class like `Category`.
It seems that is not the case in Idris.
To work around that, the standard library includes a type, `Morphism`,
that is isomorphic to the function type.

~~~~ {.sourceCode .literate .haskell}
data Morphism : Type -> Type -> Type where
  Mor : (a -> b) -> Morphism a b
~~~~

The proofs above provide everything that is required to prove the validity of
a category of Types and functions.
But the definition here uses Morphism for arrows;
so a little extra translating is necessary.

> mComp : (b ~> c) -> (a ~> b) -> (a ~> c)
> mComp (Mor f) (Mor g) = Mor (f . g)

The operator `(~>)` is an infix alias for `Morphism`.

> instance Category Type Morphism where
>   cId = Mor id
>   cComp = mComp
>
>   cIdLeft (Mor f) = qed where
>     step_1 : id . f = f
>     step_1 = leftId f
>
>     qed : Mor (id . f) = Mor f
>     qed = cong step_1
>
>   cIdRight (Mor f) = cong (rightId f)
>   cCompAssociative (Mor f) (Mor g) (Mor h) = cong $ compAssociative f g h

As with `Nat` and `NatArrow`,
the correspondence between `(->)` and `Morphism` is made official
with a proof of isomorphism.

> isoMorphismFunction : Iso (Morphism a b) (a -> b)
> isoMorphismFunction = MkIso to from toFrom fromTo where
>   to : (a ~> b) -> (a -> b)
>   to (Mor f) = f
>
>   from : (a -> b) -> (a ~> b)
>   from = Mor
>
>   toFrom : (y : a -> b) -> to (from y) = y
>   toFrom y = refl
>
>   fromTo : (x : a ~> b) -> from (to x) = x
>   fromTo (Mor x) = refl

It is my hope that I can use these definitions to work out exercises
as we continue to explore Category theory.


## Existential quantification

The Archimedean property of natural numbers:
for every natural number, there is a natural number that is larger.

> archimedean : (n : Nat) -> (m : Nat ** NatLTE n m)
> archimedean n = (1 + n ** nLTESm nEqn)