%% LyX 1.4.1 created this file. For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[english]{article}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\IfFileExists{url.sty}{\usepackage{url}}
{\newcommand{\url}{\texttt}}
\makeatletter
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LyX specific LaTeX commands.
%% Bold symbol macro for standard LaTeX users
\providecommand{\boldsymbol}[1]{\mbox{\boldmath $#1$}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
%include lhs2TeX.fmt
\usepackage{babel}
\makeatother
\begin{document}
\title{Category Theory in DTH}
\author{Robin Green \url{mailto:greenrd@@greenrd.org}}
\maketitle
\begin{code}
#include "Macros.h"
\end{code}
\section{Equality}
We need to define two equality relation metatypes: one for object
equality, and one for individual equality, since objects and individuals
have different kinds. Also, for convenience, we further define a universal
equality for objects and a universal equality for individuals, in
which the equality scopes over all appropriate values. The universal
equalities imply the ordinary equalities.
NOTE: Ordinary object equality has not been defined yet because I
don't need it yet.
\subsection{Object equality}
\begin{code}
data UnivObjectEquality (eqR :: K_CLASS(K_OBJECT -> K_OBJECT))
= UnivObjectEquality
{ univObEqReflexive :: UnivObReflexive eqR
, univObEqSymmetric :: UnivObSymmetric eqR
, univObEqTransitive :: UnivObTransitive eqR
}
type UnivObReflexive (eqR :: K_CLASS(K_OBJECT -> K_OBJECT))
= forall (a :: K_OBJECT). eqR a a
type UnivObSymmetric (eqR :: K_CLASS(K_OBJECT -> K_OBJECT))
= forall (a :: K_OBJECT) (b :: K_OBJECT). eqR a b -> eqR b a
type UnivObTransitive (eqR :: K_CLASS(K_OBJECT -> K_OBJECT))
= forall (a :: K_OBJECT) (b :: K_OBJECT) (c :: K_OBJECT). eqR a b -> eqR b c -> eqR a c
\end{code}
\subsection{Individual equality}
\begin{code}
data Equality (eqR :: K_RELATION) (a :: K_OBJECT) = Equality
{ eqReflexive :: Reflexive eqR a
, eqSymmetric :: Symmetric eqR a
, eqTransitive :: Transitive eqR a
}
type Reflexive (eqR :: K_RELATION) (a :: K_OBJECT)
= forall a1. a a1 -> eqR a1 a1
type Symmetric (eqR :: K_RELATION) (a :: K_OBJECT)
= forall a1 a2. a a1 -> a a2 -> eqR a1 a2 -> eqR a2 a1
type Transitive (eqR :: K_RELATION) (a :: K_OBJECT)
= forall a1 a2 a3. a a1 -> a a2 -> a a3 -> eqR a1 a2 -> eqR a2 a3 -> eqR a1 a3
type UnivReflexive (eqR :: K_RELATION)
= forall a1. eqR a1 a1
type UnivSymmetric (eqR :: K_RELATION)
= forall a1 a2. eqR a1 a2 -> eqR a2 a1
type UnivTransitive (eqR :: K_RELATION)
= forall a1 a2 a3. eqR a1 a2 -> eqR a2 a3 -> eqR a1 a3
newtype Identity a = Identity {runIdentity :: a}
\end{code}
\section{Types as Theorems}
{}``The type \texttt{x} is inhabited'' represents {}``\texttt{x}
is true''. (All Haskell types are technically inhabited by the special
value $\bot$, which kills the program if it tries to pattern-match
it to anything, but in DTH we don't consider $\bot$ to be a well-defined
inhabitant of any type.)
Consequently, if there is a well-defined function (in the mathematical
sense, i.e. a non-partial function) from x to y, then x implies y.
(Proof: If x is inhabited, then there exists an \texttt{x1 :: x},
so there exists a value of \texttt{y} which the function takes \texttt{x1}
to, so \texttt{y} is inhabited.) In DTH, we don't allow partial functions,
but this is not checked at compile-time and therefore it is up to
the programmer to abide by it.
\texttt{x} and \texttt{y} are logically-equivalent iff \texttt{x}
implies \texttt{y} and \texttt{y} implies \texttt{x}:
\begin{code}
data LogEq (x :: *) (y :: *) = LogEq (x -> y) (y -> x)
id :: UnivReflexive (->)
id x = x
comp :: UnivTransitive (->)
comp g f x = f (g x)
(.) = (flip comp) :: (b -> c) -> (a -> b) -> a -> c
flip f x y = f y x
logEqUnivReflexive :: UnivReflexive LogEq
logEqUnivReflexive = LogEq id id
logEqUnivSymmetric :: UnivSymmetric LogEq
logEqUnivSymmetric (LogEq xy yx) = LogEq yx xy
logEqUnivTransitive :: UnivTransitive LogEq
logEqUnivTransitive (LogEq xy yx) (LogEq yz zy) = LogEq (yz . xy) (yx . zy)
\end{code}
\section{Category Theory}
\texttt{Category} is not a class, because we don't always want to
refer to all the type parameters - which type constraints would require
us to do.
\begin{code}
data Category (ob :: K_CLASS(K_OBJECT))
(objectEquality :: K_CLASS(K_OBJECT -> K_OBJECT))
(hom :: K_MORPHISM_CLASS)
(morphismEquality :: K_RELATION)
(morphismComposition :: K_RELATION -> K_RELATION -> K_RELATION)
(identityRelation :: K_RELATION)
= Category
{ mtCategoryObjectEquality :: UnivObjectEquality objectEquality
, mtCategoryMorphismEquality :: Equality morphismEquality (IsAnyRelInstance hom)
, objectEqualityType :: forall a b. objectEquality a b -> Pair (ob a) (ob b)
, morphismType :: forall a b pcf. hom a b pcf -> Pair (ob a) (ob b)
, morphismEqualityType :: forall f g. morphismEquality f g -> MorphismEqualityRes hom f g
, composeOp :: forall a b c pcf pcg. hom b c pcf -> hom a b pcg -> hom a c (morphismComposition pcf pcg)
, identityMorphism :: forall a. ob a -> hom a a identityRelation
, leftIdentityLaw :: forall a b pcf. ob a -> ob b -> morphismEquality
(hom a b (morphismComposition identityRelation pcf))
(hom a b pcf)
, rightIdentityLaw :: forall a b pcf. ob a -> ob b -> morphismEquality
(hom a b (morphismComposition pcf identityRelation))
(hom a b pcf)
}
data IsAnyRelInstance (fn :: K_MORPHISM_CLASS) (r :: *)
= forall a b. IsAnyRelInstance (IsRelInstance (fn a b) r)
data Pair a b = Pair { fst_ :: a, snd_ :: b }
data IsRelInstance (rc :: K_CLASS(K_RELATION)) (r :: *) = forall pcf. IsRelInstance (IdR (rc pcf) r)
data MorphismEqualityRes hom f g = forall a b. MorphismEqualityRes (IsRelInstance (hom a b) f) (IsRelInstance (hom a b) g)
\end{code}
In this context, a category \textsf{C} - which, for the moment, we
will take to be the universal DTH category:
\begin{code}
type DthUniverse = Category StdObjects StdUnivObjectEquality Fn FnEq ComposeR IdR
dthUniverse :: DthUniverse
dthUniverse = Category
{ mtCategoryObjectEquality = stdUnivObjectEquality
, mtCategoryMorphismEquality = fnEq
, objectEqualityType = \_ -> Pair StdObjects StdObjects
, morphismType = \_ -> Pair StdObjects StdObjects
, morphismEqualityType = \(FnEq _) -> MorphismEqualityRes (IsRelInstance IdR) (IsRelInstance IdR)
, composeOp = compose
, identityMorphism = \_ -> idFn
, leftIdentityLaw = \_ _ -> FnEq (\_ _ -> LogEq (\(ComposeR IdR pcf) -> pcf) (ComposeR IdR))
, rightIdentityLaw = \_ _ -> FnEq (\_ _ -> LogEq (\(ComposeR pcf IdR) -> pcf) (\pcf -> ComposeR pcf IdR))
}
\end{code}
- consists of:
\begin{itemize}
\item a class \textsf{ob(C)} of objects, which are metatypes (i.e. Haskell
types of kind \texttt{{*} -> {*}}), which metaclassify metaterms
\begin{itemize}
\item metaterms, in turn, type terms
\item Recall (see section \ref{sec:Types-as-Theorems}) that metaterms represent
logical variables, while metatypes represent logical predicates
\end{itemize}
\end{itemize}
\begin{code}
data StdObjects (o :: K_OBJECT) = StdObjects
\end{code}
\begin{itemize}
\item An equality \textsf{=} on objects. \texttt{a}\textsf{=}\texttt{b}
iff \texttt{a} and \texttt{b} are the same Haskell type (modulo type
synonym substitution)
\end{itemize}
\begin{code}
data StdUnivObjectEquality (a :: K_OBJECT) (b :: K_OBJECT) where
StdUnivObjectEquality :: StdUnivObjectEquality a a
stdUnivObjectEquality :: UnivObjectEquality StdUnivObjectEquality
stdUnivObjectEquality = UnivObjectEquality
{ univObEqReflexive = StdUnivObjectEquality
, univObEqSymmetric = \StdUnivObjectEquality -> StdUnivObjectEquality
, univObEqTransitive = \StdUnivObjectEquality StdUnivObjectEquality -> StdUnivObjectEquality
}
\end{code}
\begin{itemize}
\item a class \textsf{hom(C)} of morphisms, which are metarelations from
metaterms to metaterms
\begin{itemize}
\item \texttt{Fn a b} metaclassifies metarelations from \texttt{a} to \texttt{b}
\item metarelations, in turn, dependently type functions
\item Below, \texttt{pc} is the postcondition of the function, expressed
as a relation between the input and the output. It does not matter
whether or not the relation \texttt{pc} relates individuals that are
not in the domain of the function to anything. This is because it
would not make sense in general to make \texttt{pc} impose the precondition,
because that is the job of \texttt{Fn}.
\end{itemize}
\end{itemize}
\begin{code}
type FnImpl (a :: K_OBJECT) (b :: K_OBJECT) (pc :: K_RELATION) = PrImp a (FnRes b pc)
newtype Fn (a :: K_OBJECT) (b :: K_OBJECT) (pc :: K_RELATION) = Fn (FnImpl a b pc)
-- FnRes is short for function result
-- FnRes b pc a1 = exists b1. pc a1 b1 && b b1
data FnRes (b :: K_OBJECT) (pc :: K_RELATION) (a1 :: *) = forall (b1 :: *). FnRes (pc a1 b1) (b b1)
-- Predicate implication
type PrImp p q = forall (b1 :: *). p b1 -> q b1
\end{code}
\begin{itemize}
\item An equality \textsf{=} on morphisms. \texttt{Fn a b r} = \texttt{Fn
c d s} iff \texttt{a}=\texttt{c}, \texttt{b}=\texttt{d} and \texttt{forall
a1 b1. a a1 -> b b1 -> (r a1 b1 <-> s a1 b1)}. Note that this does
\textit{not} compare the implementations, but the postconditions -
so two functions where one function has a postcondition that is more
specific than the other's postcondition, but where they both have
an identical implementation, would be treated as unequal by \texttt{FnEq}.
\end{itemize}
\begin{code}
data FnEq (f :: *) (g :: *) where
FnEq :: (forall a1 b1. a a1 -> b b1 -> LogEq (pc1 a1 b1) (pc2 a1 b1))
-> FnEq (Fn a b pc1) (Fn a b pc2)
fnEq :: Equality FnEq (IsAnyRelInstance Fn)
fnEq = Equality
{ eqReflexive = \(IsAnyRelInstance (IsRelInstance IdR)) -> FnEq (\_ _ -> logEqUnivReflexive)
, eqSymmetric = \(IsAnyRelInstance (IsRelInstance IdR)) (IsAnyRelInstance (IsRelInstance IdR)) (FnEq eqAt)
-> FnEq (logEqUnivSymmetric |<<| eqAt)
, eqTransitive = \(IsAnyRelInstance (IsRelInstance IdR)) (IsAnyRelInstance (IsRelInstance IdR))
(IsAnyRelInstance (IsRelInstance IdR)) (FnEq eq1At) (FnEq eq2At)
-> FnEq (\a1 b1 -> logEqUnivTransitive (eq1At a1 b1) (eq2At a1 b1))
}
(|<<|) = (.) . (.)
\end{code}
\begin{itemize}
\item a morphism composition operator, \texttt{Compose}R, which metacomposes
metarelations
\begin{itemize}
\item A metatype implication for \texttt{ComposeR} is given by the signature:
\begin{itemize}
\item \texttt{compose :: Fn b c pcf -> Fn a b pcg -> Fn a c (ComposeR pcf
pcg)}
\item which translates to \texttt{compose :: (pcf :: Fn b c) -> (pcg :: Fn
a b) -> (ComposeR pcf pcg :: Fn a c)}
\end{itemize}
\item \texttt{ComposeR pcf pcg} relates \texttt{a1} to \texttt{c1} iff there
exists \texttt{b1} such that \texttt{pcg a1 b1} and \texttt{pcf b1
c1}
\item \texttt{ComposeR} is associative
\end{itemize}
\end{itemize}
\begin{code}
data ComposeR (pcf :: * -> * -> *) (pcg :: * -> * -> *) (a1 :: *) (c1 :: *) where
ComposeR :: pcf b1 c1 -> pcg a1 b1 -> ComposeR pcf pcg a1 c1
compose :: Fn b c pcf -> Fn a b pcg -> Fn a c (ComposeR pcf pcg)
compose (Fn f) (Fn g) = Fn (\a -> case g a of (FnRes gab b) -> case f b of (FnRes fbc c) -> FnRes (ComposeR fbc gab) c)
\end{code}
\begin{itemize}
\item and an identity morphism, \texttt{IdR}
\begin{itemize}
\item A metatype implication for IdR is given by:
\begin{itemize}
\item \texttt{idFn :: Fn a a IdR}
\item which translates to \texttt{IdR :: Fn a a}
\end{itemize}
\item This satisfies the \texttt{leftIdentityRule} and \texttt{rightIdentityRule},
as proven above.
\end{itemize}
\end{itemize}
\begin{code}
data IdR (a :: *) (b :: *) where
IdR :: IdR a a
idFn :: Fn a a IdR
idFn = Fn (FnRes IdR)
\end{code}
\section{Functors}
\begin{code}
type Functor c d cHom dHom pcSub ret
= forall a b. Fn (Hom cHom a b)
(Hom dHom (ret a) (ret b))
(FunctorPC c d cHom dHom a b pcSub ret)
data Hom hom a b h where
Hom :: hom a b pc -> Hom hom a b (hom a b pc)
data FunctorPC c d cHom dHom a b pcSub ret g r where
\end{code}
\texttt{ret} must take each object in \texttt{c} to an object in \texttt{d}
- but this is implied by the inhabitance of \texttt{Hom dHom (ret
a) (ret b)}, so we don't need to restate it.
\texttt{c} is a category:
\begin{code}
FunctorPC ::
Category cOb cObEq cHom cHomEq cHomComp cId
\end{code}
d is a category:
\begin{code}
-> Category dOb dObEq dHom dHomEq dHomComp dId
\end{code}
fmap maps the identity to the identity:
\begin{code}
-> dHomEq (dHom (ret a) (ret a) dId) (dHom (ret a) (ret a) (pcSub a a cId))
\end{code}
The law \texttt{fmap g . fmap h = fmap g . h}
\begin{code}
-> (cOb e
-> dHomEq (dHom (ret a) (ret e) (dHomComp (pcSub a b pcg) (pcSub b e pch)))
(dHom (ret a) (ret e) (pcSub a e (cHomComp pcg pch))))
-> FunctorPC (Category cOb cObEq cHom cHomEq cHomComp cId) (Category dOb dObEq dHom dHomEq dHomComp dId) cHom dHom a b pcSub ret (cHom a b pcg) (dHom (ret a) (ret b) (pcSub a b pcg))
\end{code}
\subsection{Universal functors}
A universal functor is an endofunctor over \texttt{dthUniverse}.
\begin{code}
type UnivFunctor pcSub ret
= forall a b. Fn (Hom Fn a b)
(Hom Fn (ret a) (ret b))
(UnivFunctorPC a b pcSub ret)
data UnivFunctorPC a b pcSub ret g r where
UnivFunctorPC ::
\end{code}
fmap maps the identity to the identity:
\begin{code}
FnEq (Fn (ret a) (ret a) IdR) (Fn (ret a) (ret a) (pcSub a a IdR))
\end{code}
The law \texttt{fmap g . fmap h = fmap g . h}
\begin{code}
-> FnEq (Fn (ret a) (ret e) (ComposeR (pcSub a b pcg) (pcSub b e pch)))
(dHom (ret a) (ret e) (pcSub a e (ComposeR pcg pch)))
-> UnivFunctorPC a b pcSub ret (Fn a b pcg) (Fn (ret a) (ret b) (pcSub a b pcg))
\end{code}
Universal functors are functors:
\begin{code}
univFunctorToFunctor :: UnivFunctor pcSub ret -> Functor DthUniverse DthUniverse Fn Fn pcSub ret
univFunctorToFunctor uf = Fn (foo uf)
foo :: UnivFunctor pcSub ret
-> FnImpl (Hom Fn a b)
(Hom Fn (ret a) (ret b))
(FunctorPC DthUniverse DthUniverse Fn Fn a b pcSub ret)
foo (Fn uf) gab = case uf gab of
FnRes (UnivFunctorPC idLaw compLaw) r
-> FnRes (FunctorPC dthUniverse dthUniverse idLaw compLaw) r
\end{code}
\end{document}