Last active
March 20, 2022 18:28
-
-
Save yangzhixuan/1b29bbebeb1b8584e2568cc2248a889e to your computer and use it in GitHub Desktop.
A Haskell implementation of adjoint folds and some interface for category theory.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE KindSignatures, GADTs, TypeOperators, TypeFamilies, UndecidableInstances #-} | |
| {-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FlexibleInstances #-} | |
| {-# LANGUAGE ConstraintKinds, DeriveFunctor #-} | |
| import Prelude hiding (Functor) | |
| import qualified Prelude (Functor) | |
| -- This file explores doing category theory in Haskell by implementing | |
| -- Ralf Hinze et al.'s adjoint folds [1]: | |
| -- | |
| -- 1. Type classes for categories, functors, initial algebras and adjunctions | |
| -- are implemented, inspired by Visscher's library [2]. | |
| -- | |
| -- 2. Adjoint folds are implemented, taking adjunctions as arguments. Specifically, | |
| -- mutumorphisms are obtained from the adjunction Diagonal -| (x) : C x C -> C, | |
| -- and histomorphisms are obtained from the adjunction Forgetful -| Cofree : C -> F-Coalg. | |
| -- | |
| -- [1] Ralf Hinze, Nicolas Wu, and Jeremy Gibbons. 2013. Unifying structured | |
| -- recursion schemes. SIGPLAN Not. 48, 9 (September 2013), 209–220. | |
| -- DOI:https://doi.org/10.1145/2544174.2500578 | |
| -- | |
| -- [2] Sjoerd Visscher. 2020. data-category: Category theory. | |
| -- https://hackage.haskell.org/package/data-category-0.10 | |
| -- Part 1. Let's start with some basic definitions of category theory. | |
| --------------------------------------------------------------------- | |
| -- The following Haskell implementation of categories is a simplification of | |
| -- the one in Data.Category by Sjoerd Visscher. | |
| -- Idea: objects of categories are always indexed by types *, | |
| -- and a category is represented by its hom sets |hom :: * -> * -> *|. | |
| -- | |
| -- Moreover, it is not required that every type |t :: *| corresponds to a valid | |
| -- object in the category since |hom| can be constructed using GADTs. | |
| -- Thus an element |hom t t| can be understood as the evidence for |t| being | |
| -- an object in this category. | |
| class Category (hom :: * -> * -> *) where | |
| -- Composition | |
| comp :: hom b c -> hom a b -> hom a c | |
| -- Identity arrows on the source/target of an arrow | |
| src :: hom a b -> hom a a | |
| tgt :: hom a b -> hom b b | |
| -- We usually use an identity arrow in |hom a a| as evidence for |a :: *| being | |
| -- an object in a category. | |
| type Obj hom a = hom a a | |
| -- Some instances of categories | |
| ------------------------------- | |
| -- The category Hask of Haskell types and functions | |
| instance Category (->) where | |
| comp f g = f . g | |
| src _ = id | |
| tgt _ = id | |
| -- The product category of Hask x Hask | |
| data ProdCat :: * -> * -> * where | |
| PArr :: (a -> b) -> (c -> d) -> ProdCat (a, c) (b, d) | |
| instance Category ProdCat where | |
| comp (PArr f g) (PArr f' g') = PArr (f . f') (g . g') | |
| src (PArr _ _) = PArr id id | |
| tgt (PArr _ _) = PArr id id | |
| -- Category of algebras on Hask. | |
| -- Since we cannot index a type by functions, we workaround it by | |
| -- restricting every type has (at most) one algebra. | |
| class Algebra f a where | |
| alg :: f a -> a | |
| data Alg (f :: * -> *) :: * -> * -> * where | |
| AlgHom :: (Algebra f a, Algebra f b) => (a -> b) -> Alg f a b | |
| -- A functor is in principle a type family for the object mapping and an | |
| -- arrow mapping, but in Haskell we cannot make type families instances | |
| -- of type classes. To workaround, every functor will be given a 'tag' of kind '*'. | |
| class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where | |
| -- | The domain, or source category, of the functor. | |
| type Dom ftag :: * -> * -> * | |
| -- | The codomain, or target category, of the functor. | |
| type Cod ftag :: * -> * -> * | |
| -- | @:%@ maps objects. | |
| type ftag :% a :: * | |
| -- | @%@ maps arrows. | |
| (%) :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b) | |
| -- Every Prelude.Functor defines a functor on Hask | |
| data HaskellFunctor (f :: * -> *) = HaskellFunctor | |
| instance Prelude.Functor f => Functor (HaskellFunctor f) where | |
| type Dom (HaskellFunctor f) = (->) | |
| type Cod (HaskellFunctor f) = (->) | |
| type (HaskellFunctor f) :% a = f a | |
| (%) _ g = fmap g | |
| -- The tag of the functor (x) : Hask x Hask -> Hask | |
| data HaskProd = HaskProd | |
| instance Functor HaskProd where | |
| type Dom HaskProd = ProdCat | |
| type Cod HaskProd = (->) | |
| type HaskProd :% (a, b) = (a, b) | |
| (%) _ (PArr f g) = \ (a, b) -> (f a, g b) | |
| -- The diagonal functor Hask -> Hask x Hask | |
| data Diag = Diag | |
| instance Functor Diag where | |
| type Dom Diag = (->) | |
| type Cod Diag = ProdCat | |
| type Diag :% a = (a, a) | |
| (%) _ f = PArr f f | |
| -- Type class for adjunctions | |
| class (Functor ltag, Functor rtag, Dom ltag ~ Cod rtag, Dom rtag ~ Cod ltag) | |
| => Adjunction ltag rtag where | |
| phi :: ltag -> rtag -> Obj (Dom ltag) a -> Obj (Cod ltag) b | |
| -- The two objects arguments are sometimes used for evidencing a and b are indeed objects. | |
| -> Cod ltag (ltag :% a) b -> Dom ltag a (rtag :% b) | |
| phiInv :: ltag -> rtag -> Obj (Dom ltag) a -> Obj (Cod ltag) b | |
| -> Dom ltag a (rtag :% b) -> Cod ltag (ltag :% a) b | |
| instance Adjunction Diag HaskProd where | |
| phi _ _ _ _ (PArr f g) = \a -> (f a, g a) | |
| phiInv _ _ _ (PArr _ _) h = PArr (fst . h) (snd . h) | |
| -- Adjoint folds with the initial algebra fixed to be in the category Hask. | |
| data Mu f = In { inOp :: f (Mu f) } | |
| cata :: Prelude.Functor f => (f a -> a) -> Mu f -> a | |
| cata alg = alg . fmap (cata alg) . inOp | |
| afold :: (Category c, Adjunction l r, | |
| Dom l ~ (->), | |
| Cod l ~ c, | |
| Prelude.Functor f) | |
| => l -> r -> Obj c a -> Obj (->) (Mu f) | |
| -> c (l :% f (r :% a)) a | |
| -> c (l :% Mu f) a | |
| afold l r aObj mufObj alg = phiInv l r mufObj aObj h where | |
| h = cata (phi l r id aObj alg) | |
| -- Mutumorphism from adjoint fold | |
| mutu :: Prelude.Functor f | |
| => (f (a, b) -> a) -> (f (a, b) -> b) | |
| -> (Mu f -> a, Mu f -> b) | |
| mutu alg1 alg2 = (h1, h2) where | |
| (PArr h1 h2) = afold Diag HaskProd (PArr id id) id (PArr alg1 alg2) | |
| -- Part 2 | |
| -- Adjoint folds with both categories being generic and the example of | |
| -- histomorphism. | |
| --------------------------------------------------------------------- | |
| -- But let us first build a generic interface for functors | |
| -- with initial algebras. | |
| class (Functor f, Cod f ~ Dom f) => HasInitAlg f where | |
| type InitAlg f :: * | |
| inAlgId :: f -> Cod f (InitAlg f) (InitAlg f) | |
| inAlg :: f -> Cod f (InitAlg f) (InitAlg f) | |
| -> Cod f (f :% InitAlg f) (InitAlg f) | |
| inAlgOp :: f -> Cod f (InitAlg f) (InitAlg f) | |
| -> Cod f (InitAlg f) (f :% InitAlg f) | |
| cataG :: f -> Cod f (InitAlg f) (InitAlg f) -> Cod f a a | |
| -> Cod f (f :% a) a -> Cod f (InitAlg f) a | |
| type EndoFunctor f c = (Cod f ~ c, Dom f ~ c, Functor f) | |
| -- All endofunctors on Hask has initial algebras. | |
| -- (This is commented out because |HasInitAlg f| overlaps all other instances). | |
| {- | |
| instance (EndoFunctor f (->)) => HasInitAlg f where | |
| newtype instance InitAlg f = HaskInitAlgIn { haskInitAlgInOp :: f :% InitAlg f } | |
| inAlgId _ = id | |
| inAlg _ _ = HaskInitAlgIn | |
| inAlgOp _ _ = haskInitAlgInOp | |
| cataG f _ _ alg = go where | |
| go = alg . (f % go) . haskInitAlgInOp | |
| -} | |
| -- The generic version of adjoint folds on two categories c and d, | |
| -- for an endofunctor on d with initial algebras. | |
| afoldG :: (Category c, Category d, Adjunction l r, | |
| Dom l ~ d, Cod l ~ c, EndoFunctor f d, HasInitAlg f) | |
| => f -> l -> r -> Obj c a -> Obj d (InitAlg f) | |
| -> c (l :% (f :% (r :% a))) a | |
| -> c (l :% InitAlg f) a | |
| afoldG f l r aObj mufObj alg = phiInv l r mufObj aObj h where | |
| -- h :: d (InitAlg f) (r :% a) | |
| h = cataG f mufObj raObj (phi l r (f % raObj) aObj alg) | |
| -- d (r % a) (r % a) | |
| raObj = r % aObj | |
| -- Histomorphisms are adjoint folds arising from the forgetful/cofree adjunction. | |
| -- First we define the category of coalgebras of some endofunctor on Hask. | |
| data CoalgHom (f :: * -> *) :: * -> * -> * where | |
| CoalgArr :: (Coalgebra f a, Coalgebra f b) => (a -> b) -> CoalgHom f a b | |
| class Coalgebra f a where | |
| coalg :: a -> f a | |
| -- Whenever there is a coalgebra a -> f a, there is another f a -> f (f a) | |
| instance (Coalgebra f a, Prelude.Functor f) => Coalgebra f (f a) where | |
| coalg = fmap coalg | |
| instance Category (CoalgHom f) where | |
| comp (CoalgArr h) (CoalgArr g) = CoalgArr (h . g) | |
| src (CoalgArr _) = CoalgArr id | |
| tgt (CoalgArr _) = CoalgArr id | |
| -- An endofunctor f on Hask can be lifted to an endofunctor on f-Coalg | |
| data LiftToCoalg (f :: * -> *) = LiftToCoAlg | |
| instance Prelude.Functor f => Functor (LiftToCoalg f) where | |
| type Dom (LiftToCoalg f) = CoalgHom f | |
| type Cod (LiftToCoalg f) = CoalgHom f | |
| type (LiftToCoalg f) :% a = f a | |
| _ % (CoalgArr h) = CoalgArr (fmap h) | |
| -- And the lifted functor |LiftToCoalg f :: f-Coalg -> f-Coalg| has initial | |
| -- algebras. | |
| instance Prelude.Functor f => HasInitAlg (LiftToCoalg f) where | |
| type InitAlg (LiftToCoalg f) = Mu f | |
| inAlgId _ = CoalgArr id | |
| inAlg _ _ = CoalgArr In | |
| inAlgOp _ _ = CoalgArr inOp | |
| cataG f _ _ (CoalgArr alg) = CoalgArr go where | |
| go = alg . (fmap go) . inOp | |
| instance Coalgebra f (Mu f) where | |
| coalg = inOp | |
| -- We continue to construct the forgetful/cofree adjunction. | |
| -- The forgetful functor f-Coalg -> Hask. | |
| data UCoAlg (f :: * -> *) = UCoAlg | |
| instance Prelude.Functor f => Functor (UCoAlg f) where | |
| type Dom (UCoAlg f) = CoalgHom f | |
| type Cod (UCoAlg f) = (->) | |
| type (:%) (UCoAlg f) a = a | |
| _ % (CoalgArr f) = f | |
| -- The cofree functor Hask -> f-Coalg | |
| data CofreeF (f :: * -> *) = CofreeF | |
| -- The carrier of the cofree coalgebra | |
| data Cofree f x = Cofree { label :: x, branch :: f (Cofree f x) } | |
| instance Coalgebra f (Cofree f x) where | |
| coalg = branch | |
| instance Prelude.Functor f => Functor (CofreeF f) where | |
| type Dom (CofreeF f) = (->) | |
| type Cod (CofreeF f) = CoalgHom f | |
| type (:%) (CofreeF f) a = Cofree f a | |
| _ % h = CoalgArr go where | |
| go (Cofree label branch) = Cofree (h label) (fmap go branch) | |
| -- The forgetful functor is left adjoint to the cofree coalgebra functor | |
| instance (Prelude.Functor f) => Adjunction (UCoAlg f) (CofreeF f) where | |
| phi _ _ (CoalgArr _) _ f = CoalgArr go where | |
| go a = Cofree (f a) (fmap go (coalg a)) | |
| phiInv _ _ (CoalgArr _) _ (CoalgArr g) = label . g | |
| -- Histomorphism is an adjoint fold from the above adjunction | |
| hist :: Prelude.Functor f => (f (Cofree f a) -> a) -> (Mu f -> a) | |
| hist alg = afoldG LiftToCoAlg UCoAlg CofreeF id (CoalgArr id) alg | |
| -- Let's check if I got all the code right. | |
| data NatF x = Z | Suc x deriving Prelude.Functor | |
| fib :: Mu NatF -> Integer | |
| fib = hist alg where | |
| alg Z = 0 | |
| alg (Suc (Cofree _ Z)) = 1 | |
| alg (Suc (Cofree n (Suc (Cofree m _)))) = n + m | |
| fibTest :: Integer -> Integer | |
| fibTest k | |
| | k >= 0 = fib (toNat k) where | |
| toNat 0 = In Z | |
| toNat n = In (Suc (toNat (n - 1))) | |
| -- I did! Amazing! | |
| -- map fibTest [0 .. 10] = [0,1,1,2,3,5,8,13,21,34,55] |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment