Use a different representation of categories, add a couple data types.
parent
2e06699c97
commit
3e3a9ccbd3
GPG Key ID:
4B7F3DA9351E577C
|
|
@ -4,7 +4,7 @@ cabal-version: 2.2
|
|||
--
|
||||
-- see: https://github.com/sol/hpack
|
||||
--
|
||||
-- hash: dbc9287122d243040cde8135abd883bf209073c191d5ece40c561f33abfbd4c8
|
||||
-- hash: d2b69687ecaa1f177ecb0533b202092619c3c90b1107255e2fdaef7e70b84af5
|
||||
|
||||
name: monoids-in-the-categoy-of-endofunctors
|
||||
version: 0.1.0.0
|
||||
|
|
@ -29,19 +29,17 @@ library
|
|||
Category
|
||||
Category.Base
|
||||
Category.Constraint
|
||||
Category.Functor.Base
|
||||
Category.Natural
|
||||
Category.Star
|
||||
Category.Functor
|
||||
Category.Functor.Foldable
|
||||
Data.Dict
|
||||
Data.Recursive
|
||||
Data.Fin
|
||||
Data.Nat
|
||||
other-modules:
|
||||
Paths_monoids_in_the_categoy_of_endofunctors
|
||||
hs-source-dirs:
|
||||
src
|
||||
default-extensions: BlockArguments ConstraintKinds DataKinds FlexibleContexts FlexibleInstances FunctionalDependencies GADTs ImportQualifiedPost InstanceSigs LambdaCase MultiParamTypeClasses NoImplicitPrelude PolyKinds RankNTypes ScopedTypeVariables TypeApplications TypeFamilies TypeOperators
|
||||
default-extensions: BlockArguments ConstraintKinds DataKinds DefaultSignatures FlexibleContexts FlexibleInstances FunctionalDependencies GADTs ImportQualifiedPost InstanceSigs LambdaCase MultiParamTypeClasses NoImplicitPrelude PolyKinds QuantifiedConstraints RankNTypes ScopedTypeVariables TypeApplications TypeFamilies TypeOperators
|
||||
ghc-options: -Weverything -Wno-missing-export-lists -Wno-missing-import-lists -Wno-safe -Wno-missing-safe-haskell-mode
|
||||
build-depends:
|
||||
base >=4.13 && <5
|
||||
, invariant >=0.5 && <0.6
|
||||
, profunctors >=5.5 && <6
|
||||
default-language: Haskell2010
|
||||
|
|
|
|||
|
|
@ -15,6 +15,7 @@ default-extensions:
|
|||
- BlockArguments
|
||||
- ConstraintKinds
|
||||
- DataKinds
|
||||
- DefaultSignatures
|
||||
- FlexibleContexts
|
||||
- FlexibleInstances
|
||||
- FunctionalDependencies
|
||||
|
|
@ -25,6 +26,7 @@ default-extensions:
|
|||
- MultiParamTypeClasses
|
||||
- NoImplicitPrelude
|
||||
- PolyKinds
|
||||
- QuantifiedConstraints
|
||||
- RankNTypes
|
||||
- ScopedTypeVariables
|
||||
- TypeApplications
|
||||
|
|
@ -41,8 +43,6 @@ ghc-options:
|
|||
|
||||
dependencies:
|
||||
- base >= 4.13 && < 5
|
||||
- invariant >= 0.5 && < 0.6
|
||||
- profunctors >= 5.5 && < 6
|
||||
|
||||
library:
|
||||
source-dirs: src
|
||||
|
|
|
|||
109
src/Category.hs
109
src/Category.hs
|
|
@ -1,112 +1,9 @@
|
|||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Category
|
||||
( module Category.Base
|
||||
, module Category.Functor.Base
|
||||
, module Category.Natural
|
||||
, Monoidal, Unit, Product, monBi, monIdLI, monIdRI, monIdLE, monIdRE, monAssocL, monAssocR
|
||||
, BiEndo, biendomap
|
||||
, ProEndo, diendomap
|
||||
, Bi, bimap
|
||||
, Pro, dimap
|
||||
, Semigroup, append
|
||||
, Monoid, empty
|
||||
, Applicative, pure, ap
|
||||
, Monad, join
|
||||
, module Category.Constraint
|
||||
, module Category.Functor
|
||||
) where
|
||||
|
||||
import Category.Base
|
||||
import Category.Constraint
|
||||
import Category.Functor.Base
|
||||
import Category.Natural
|
||||
import Category.Star qualified as Star
|
||||
import Data.Kind (Type)
|
||||
|
||||
-- | A bi-endofunctor in an unenriched category covariant in both arguments.
|
||||
class Category cat => BiEndo cat f where
|
||||
biendomap :: cat a c -> cat b d -> cat (f a b) (f c d)
|
||||
|
||||
instance {-# OVERLAPPABLE #-} Star.Bifunctor f => BiEndo (->) f where
|
||||
biendomap = Star.bimap
|
||||
|
||||
-- | A pro-endofunctor in an unenriched category (contravariant in the left argument, covariant in the right).
|
||||
class Category cat => ProEndo cat f where
|
||||
diendomap :: cat c a -> cat b d -> cat (f a b) (f c d)
|
||||
|
||||
instance {-# OVERLAPPABLE #-} Star.Profunctor f => ProEndo (->) f where
|
||||
diendomap = Star.dimap
|
||||
|
||||
-- | A bifunctor in an unenriched category covariant in both arguments.
|
||||
class (Category dom, Category cod) => Bi dom cod f where
|
||||
bimap :: dom a c -> dom b d -> cod (f a b) (f c d)
|
||||
|
||||
instance {-# OVERLAPPABLE #-} BiEndo cat f => Bi cat cat f where
|
||||
bimap = biendomap
|
||||
|
||||
-- | A profunctor in an unenriched category (contravariant in the left argument, covariant in the right).
|
||||
class (Category dom, Category cod) => Pro dom cod f where
|
||||
dimap :: dom c a -> dom b d -> cod (f a b) (f c d)
|
||||
|
||||
instance {-# OVERLAPPABLE #-} ProEndo cat f => Pro cat cat f where
|
||||
dimap = diendomap
|
||||
|
||||
instance Pro (:-) (->) (:-) where
|
||||
dimap f g h = g . h . f
|
||||
|
||||
class Category cat => Monoidal (cat :: i -> i -> Type) where
|
||||
type Unit cat :: i
|
||||
type Product cat :: i -> i -> i
|
||||
monBi :: proxy cat -> Dict (BiEndo cat (Product cat))
|
||||
monIdLI :: a `cat` Product cat a (Unit cat)
|
||||
monIdRI :: a `cat` Product cat (Unit cat) a
|
||||
monIdLE :: Product cat a (Unit cat) `cat` a
|
||||
monIdRE :: Product cat (Unit cat) a `cat` a
|
||||
monAssocL :: Product cat (Product cat a b) c `cat` Product cat a (Product cat b c)
|
||||
monAssocR :: Product cat a (Product cat b c) `cat` Product cat (Product cat a b) c
|
||||
|
||||
instance Monoidal (->) where
|
||||
type Unit (->) = ()
|
||||
type Product (->) = (,)
|
||||
monBi _ = Dict
|
||||
monIdLI x = (x, ())
|
||||
monIdRI x = ((), x)
|
||||
monIdLE (x, ()) = x
|
||||
monIdRE ((), x) = x
|
||||
monAssocL ((x, y), z) = (x, (y, z))
|
||||
monAssocR (x, (y, z)) = ((x, y), z)
|
||||
|
||||
-- | A semigroup object in a monoidal unenriched category.
|
||||
class Monoidal cat => Semigroup cat s where
|
||||
append :: Product cat s s `cat` s
|
||||
|
||||
instance {-# OVERLAPPABLE #-} Star.Semigroup s => Semigroup (->) s where
|
||||
append (x, y) = (Star.<>) x y
|
||||
|
||||
-- | A monoid object in a monoidal unenriched category.
|
||||
class Semigroup cat s => Monoid cat s where
|
||||
empty :: Unit cat `cat` s
|
||||
|
||||
instance {-# OVERLAPPABLE #-} Star.Monoid s => Monoid (->) s where
|
||||
empty () = Star.mempty
|
||||
|
||||
-- | An applicative functor.
|
||||
class (Monoidal cat, Endofunctor cat f) => Applicative cat f where
|
||||
pure :: a `cat` f a
|
||||
ap :: Product cat (f (a `cat` b)) (f a) `cat` f b
|
||||
|
||||
instance {-# OVERLAPPABLE #-} Star.Applicative f => Applicative (->) f where
|
||||
pure = Star.pure
|
||||
ap (f, x) = (Star.<*>) f x
|
||||
|
||||
-- | A monoid object in the category of endofunctors in a monoidal unenriched category.
|
||||
class Applicative cat m => Monad cat m where
|
||||
join :: m (m a) `cat` m a
|
||||
|
||||
instance {-# OVERLAPPABLE #-} Star.Monad m => Monad (->) m where
|
||||
join = Star.join
|
||||
|
||||
class AnyC a
|
||||
instance AnyC a
|
||||
|
||||
class AnyC2 a b
|
||||
instance AnyC2 a b
|
||||
import Category.Functor
|
||||
|
|
|
|||
|
|
@ -1,15 +1,63 @@
|
|||
{-# LANGUAGE ExplicitNamespaces #-}
|
||||
module Category.Base
|
||||
( module Control.Category
|
||||
, type (~>)
|
||||
, Post
|
||||
) where
|
||||
module Category.Base where
|
||||
|
||||
import Control.Category (Category, id, (.))
|
||||
import Data.Kind (Type)
|
||||
|
||||
-- | An unenriched hom.
|
||||
type family (~>) :: i -> i -> Type
|
||||
type instance (~>) = (->)
|
||||
type Obj q a = a `q` a
|
||||
|
||||
class Semigroupoid (q :: i -> i -> Type) where
|
||||
(.) :: b `q` c -> a `q` b -> a `q` c
|
||||
|
||||
instance Semigroupoid (->) where
|
||||
(.) f g x = f (g x)
|
||||
|
||||
class Semigroupoid q => Category q where
|
||||
src :: a `q` b -> Obj q a
|
||||
tgt :: a `q` b -> Obj q b
|
||||
|
||||
instance Category (->) where
|
||||
src _ x = x
|
||||
tgt _ x = x
|
||||
|
||||
class Category q => Groupoid q where
|
||||
inv :: a `q` b -> b `q` a
|
||||
|
||||
newtype Yoneda (q :: i -> i -> Type) (a :: i) (b :: i) = Op { getOp :: b `q` a }
|
||||
|
||||
instance Semigroupoid q => Semigroupoid (Yoneda q) where
|
||||
Op f . Op g = Op (g . f)
|
||||
|
||||
instance Category q => Category (Yoneda q) where
|
||||
src (Op f) = Op (tgt f)
|
||||
tgt (Op f) = Op (src f)
|
||||
|
||||
type family Op (q :: i -> i -> Type) :: i -> i -> Type where
|
||||
Op (Yoneda q) = q
|
||||
Op q = Yoneda q
|
||||
|
||||
type Post f = forall a. f a
|
||||
type Endo f a = f a a
|
||||
|
||||
data (:~:) :: i -> i -> Type where
|
||||
Refl :: a :~: a
|
||||
|
||||
instance Semigroupoid (:~:) where
|
||||
Refl . Refl = Refl
|
||||
|
||||
instance Category (:~:) where
|
||||
src _ = Refl
|
||||
tgt _ = Refl
|
||||
|
||||
instance Groupoid (:~:) where
|
||||
inv Refl = Refl
|
||||
|
||||
data Unit a b = Unit
|
||||
|
||||
instance Semigroupoid Unit where
|
||||
Unit . Unit = Unit
|
||||
|
||||
instance Category Unit where
|
||||
src _ = Unit
|
||||
tgt _ = Unit
|
||||
|
||||
instance Groupoid Unit where
|
||||
inv _ = Unit
|
||||
|
|
|
|||
|
|
@ -1,4 +1,3 @@
|
|||
{-# LANGUAGE RankNTypes #-}
|
||||
module Category.Constraint
|
||||
( module Data.Dict
|
||||
, (:-) (Sub)
|
||||
|
|
@ -10,11 +9,12 @@ import Data.Dict
|
|||
|
||||
newtype a :- b = Sub (a => Dict b)
|
||||
|
||||
type instance (~>) = (:-)
|
||||
|
||||
(\\) :: a => (b => c) -> (a :- b) -> c
|
||||
r \\ Sub Dict = r
|
||||
|
||||
instance Category (:-) where
|
||||
id = Sub Dict
|
||||
instance Semigroupoid (:-) where
|
||||
f . g = Sub (Dict \\ f \\ g)
|
||||
|
||||
instance Category (:-) where
|
||||
src _ = Sub Dict
|
||||
tgt _ = Sub Dict
|
||||
|
|
|
|||
|
|
@ -0,0 +1,72 @@
|
|||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Category.Functor where
|
||||
|
||||
import Category.Base
|
||||
import Data.Kind (Type)
|
||||
|
||||
class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
|
||||
type Dom f :: i -> i -> Type
|
||||
type Cod f :: j -> j -> Type
|
||||
map :: Dom f a b -> Cod f (f a) (f b)
|
||||
|
||||
class (Functor f, Dom f ~ q, Cod f ~ r) => FunctorOf q r f
|
||||
instance (Functor f, Dom f ~ q, Cod f ~ r) => FunctorOf q r f
|
||||
|
||||
class (Functor f, Dom f ~ Cod f) => Endofunctor f
|
||||
instance (Functor f, Dom f ~ Cod f) => Endofunctor f
|
||||
|
||||
data Nat (q :: i -> i -> Type) (r :: j -> j -> Type) (f :: i -> j) (g :: i -> j) :: Type where
|
||||
Nat :: (FunctorOf q r f, FunctorOf q r g) => (forall a. Obj q a -> r (f a) (g a)) -> Nat q r f g
|
||||
|
||||
instance Semigroupoid r => Semigroupoid (Nat q r) where
|
||||
(.) (Nat f) (Nat g) = Nat \p -> (f p . g p)
|
||||
|
||||
instance Category r => Category (Nat q r) where
|
||||
src (Nat f) = Nat (src . f)
|
||||
tgt (Nat f) = Nat (tgt . f)
|
||||
|
||||
instance Functor (->) where
|
||||
type Dom (->) = Op (->)
|
||||
type Cod (->) = Nat (->) (->)
|
||||
map (Op f) = Nat \_ -> (. f)
|
||||
|
||||
instance Functor ((->) a) where
|
||||
type Dom ((->) a) = (->)
|
||||
type Cod ((->) a) = (->)
|
||||
map f g = f . g
|
||||
|
||||
instance Functor (,) where
|
||||
type Dom (,) = (->)
|
||||
type Cod (,) = Nat (->) (->)
|
||||
map f = Nat \_ (x, y) -> (f x, y)
|
||||
|
||||
instance Functor ((,) a) where
|
||||
type Dom ((,) a) = (->)
|
||||
type Cod ((,) a) = (->)
|
||||
map f (x, y) = (x, f y)
|
||||
|
||||
--
|
||||
type family NatDom (f :: (i -> j) -> (i -> j) -> Type) :: (i -> i -> Type) where
|
||||
NatDom (Nat p _) = p
|
||||
|
||||
type family NatCod (f :: (i -> j) -> (i -> j) -> Type) :: (j -> j -> Type) where
|
||||
NatCod (Nat _ q) = q
|
||||
|
||||
type Dom2 p = NatDom (Cod p)
|
||||
type Cod2 p = NatCod (Cod p)
|
||||
|
||||
class (Functor p, Cod p ~ Nat (Dom2 p) (Cod2 p), Category (Dom2 p), Category (Cod2 p)) => Bifunctor (p :: i -> j -> k)
|
||||
instance (Functor p, Cod p ~ Nat (Dom2 p) (Cod2 p), Category (Dom2 p), Category (Cod2 p)) => Bifunctor (p :: i -> j -> k)
|
||||
|
||||
newtype Const a b = Const { getConst :: a }
|
||||
|
||||
instance Functor (Const a) where
|
||||
-- FIXME
|
||||
type Dom (Const a) = (:~:)
|
||||
type Cod (Const a) = (->)
|
||||
map _ (Const x) = Const x
|
||||
|
||||
instance Functor Const where
|
||||
type Dom Const = (->)
|
||||
type Cod Const = Nat (:~:) (->)
|
||||
map f = Nat \_ -> \case (Const x) -> Const (f x)
|
||||
|
|
@ -1,67 +0,0 @@
|
|||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Category.Functor.Base
|
||||
( Phantom, phmap
|
||||
, Endofunctor, emap, Functor, map
|
||||
, ContraEndofunctor, contraemap, ContraFunctor, contramap
|
||||
, InvariantEndofunctor, invemap, InvariantFunctor, invmap
|
||||
) where
|
||||
|
||||
import Category.Base
|
||||
import Category.Star qualified as Star
|
||||
import Data.Kind (Type)
|
||||
|
||||
-- | A type constructor ending in Type which varies freely in its argument.
|
||||
--
|
||||
-- All Phantom types should also implement Endofunctor and ContraEndofunctor.
|
||||
class Category cat => Phantom cat f where
|
||||
phmap :: f a `cat` f b
|
||||
|
||||
-- | An endofunctor in an unenriched category which is covariant in its argument.
|
||||
--
|
||||
-- All Endofunctors should also implement InvariantEndofunctor.
|
||||
class Category cat => Endofunctor cat f where
|
||||
emap :: a `cat` b -> f a `cat` f b
|
||||
|
||||
instance {-# OVERLAPPABLE #-} Star.Functor f => Endofunctor (->) f where
|
||||
emap = Star.fmap
|
||||
|
||||
-- | A functor between unenriched categories which is covariant in its argument.
|
||||
--
|
||||
-- All Functors should also implement InvariantFunctor.
|
||||
class (Category dom, Category cod) => Functor dom cod f where
|
||||
map :: a `dom` b -> f a `cod` f b
|
||||
|
||||
instance {-# OVERLAPPABLE #-} Endofunctor cat f => Functor cat cat f where
|
||||
map = emap
|
||||
|
||||
-- \ An endofunctor in an unenriched category which is contravariant in its argument.
|
||||
--
|
||||
-- All ContraEndofunctors should also implement InvariantEndofunctor.
|
||||
class Category cat => ContraEndofunctor cat f where
|
||||
contraemap :: b `cat` a -> f a `cat` f b
|
||||
|
||||
instance {-# OVERLAPPABLE #-} Star.Contravariant f => ContraEndofunctor (->) f where
|
||||
contraemap = Star.contramap
|
||||
|
||||
-- | A functor between unenriched categories which is contravariant in its argument.
|
||||
--
|
||||
-- All ContraFunctors should also implement InvariantFunctor.
|
||||
class (Category dom, Category cod) => ContraFunctor dom cod f where
|
||||
contramap :: b `dom` a -> f a `cod` f b
|
||||
|
||||
instance {-# OVERLAPPABLE #-} ContraEndofunctor cat f => ContraFunctor cat cat f where
|
||||
contramap = contraemap
|
||||
|
||||
-- | An endofunctor-like type in an unenriched category which is parametric in its argument.
|
||||
class Category cat => InvariantEndofunctor cat f where
|
||||
invemap :: a `cat` b -> b `cat` a -> f a `cat` f b
|
||||
|
||||
instance {-# OVERLAPPABLE #-} Star.Invariant f => InvariantEndofunctor (->) f where
|
||||
invemap = Star.invmap
|
||||
|
||||
-- | An endofunctor-like type between unenriched categories which is parametric in its argument.
|
||||
class (Category dom, Category cod) => InvariantFunctor dom cod f where
|
||||
invmap :: a `dom` b -> b `dom` a -> f a `cod` f b
|
||||
|
||||
instance {-# OVERLAPPABLE #-} InvariantEndofunctor cat f => InvariantFunctor cat cat f where
|
||||
invmap = invemap
|
||||
|
|
@ -0,0 +1,22 @@
|
|||
module Category.Functor.Foldable where
|
||||
|
||||
import Category.Base
|
||||
import Category.Functor
|
||||
|
||||
type family Base (t :: i) :: i -> i
|
||||
|
||||
class Endofunctor (Base t) => Recursive t where
|
||||
project :: Dom (Base t) t (Base t t)
|
||||
|
||||
class Endofunctor (Base t) => Corecursive t where
|
||||
embed :: Dom (Base t) (Base t t) t
|
||||
|
||||
type Algebra f a = Dom f (f a) a
|
||||
|
||||
cata :: Recursive t => Algebra (Base t) a -> Dom (Base t) t a
|
||||
cata alg = alg . map (cata alg) . project
|
||||
|
||||
type Coalgebra f a = Dom f a (f a)
|
||||
|
||||
ana :: Corecursive t => Coalgebra (Base t) a -> Dom (Base t) a t
|
||||
ana coalg = embed . map (ana coalg) . coalg
|
||||
|
|
@ -1,17 +0,0 @@
|
|||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
-- | The category of natural transformations.
|
||||
module Category.Natural where
|
||||
|
||||
import Category.Base
|
||||
import Data.Kind (Type)
|
||||
|
||||
newtype Nat f g = Nat { runNat :: forall a. f a ~> g a }
|
||||
|
||||
type instance (~>) = Nat
|
||||
|
||||
type ChildHom (nat :: (i -> j) -> (i -> j) -> Type) = (~>) :: j -> j -> Type
|
||||
|
||||
instance (nat ~ Nat, Category (ChildHom nat)) => Category (nat :: (i -> j) -> (i -> j) -> Type) where
|
||||
id = Nat id
|
||||
Nat f . Nat g = Nat (f . g)
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
-- | Re-export category typeclasses which are specialized to the category of types.
|
||||
module Category.Star
|
||||
( module Control.Applicative
|
||||
, module Control.Monad
|
||||
, module Data.Bifunctor
|
||||
, module Data.Functor
|
||||
, module Data.Functor.Contravariant
|
||||
, module Data.Functor.Invariant
|
||||
, module Data.Monoid
|
||||
, module Data.Profunctor
|
||||
, module Data.Semigroup
|
||||
) where
|
||||
|
||||
import Control.Applicative (Applicative, pure, (<*>))
|
||||
import Control.Monad (Monad, join)
|
||||
import Data.Bifunctor (Bifunctor, bimap)
|
||||
import Data.Functor (Functor, fmap)
|
||||
import Data.Functor.Contravariant (Contravariant, contramap)
|
||||
import Data.Functor.Invariant (Invariant, invmap)
|
||||
import Data.Monoid (Monoid, mempty)
|
||||
import Data.Profunctor (Profunctor, dimap)
|
||||
import Data.Semigroup (Semigroup, (<>))
|
||||
|
|
@ -1,4 +1,3 @@
|
|||
{-# LANGUAGE RankNTypes #-}
|
||||
module Data.Dict where
|
||||
|
||||
data Dict c where
|
||||
|
|
|
|||
|
|
@ -0,0 +1,47 @@
|
|||
module Data.Fin where
|
||||
|
||||
import Category
|
||||
import Category.Functor.Foldable
|
||||
import Data.Nat
|
||||
|
||||
data Fin n where
|
||||
FZ :: Fin ('S n)
|
||||
FS :: Fin n -> Fin ('S n)
|
||||
data FinF r n where
|
||||
FZF :: FinF r ('S n)
|
||||
FSF :: r n -> FinF r ('S n)
|
||||
type instance Base Fin = FinF
|
||||
|
||||
instance Functor Fin where
|
||||
type Dom Fin = (:~:)
|
||||
type Cod Fin = (->)
|
||||
map Refl x = x
|
||||
|
||||
instance Functor (FinF r) where
|
||||
type Dom (FinF r) = (:~:)
|
||||
type Cod (FinF r) = (->)
|
||||
map Refl x = x
|
||||
|
||||
instance Functor FinF where
|
||||
type Dom FinF = Nat (:~:) (->)
|
||||
type Cod FinF = Nat (:~:) (->)
|
||||
map :: forall f g. Nat (:~:) (->) f g -> Nat (:~:) (->) (FinF f) (FinF g)
|
||||
map (Nat f) = Nat \_ -> \case
|
||||
FZF -> FZF
|
||||
(FSF r) -> FSF (f Refl r)
|
||||
|
||||
instance Recursive Fin where
|
||||
project = Nat \_ -> \case
|
||||
FZ -> FZF
|
||||
(FS r) -> FSF r
|
||||
|
||||
instance Corecursive Fin where
|
||||
embed = Nat \_ -> \case
|
||||
FZF -> FZ
|
||||
(FSF r) -> FS r
|
||||
|
||||
fin2nat :: Nat (:~:) (->) Fin (Const N)
|
||||
fin2nat = cata (Nat \_ -> alg)
|
||||
where alg :: FinF (Const N) n -> Const N n
|
||||
alg FZF = Const Z
|
||||
alg (FSF (Const n)) = Const (S n)
|
||||
|
|
@ -0,0 +1,58 @@
|
|||
module Data.Nat where
|
||||
|
||||
import Category
|
||||
import Category.Functor.Foldable
|
||||
|
||||
data N = Z | S N
|
||||
data NF r = ZF | SF r
|
||||
type instance Base N = NF
|
||||
|
||||
instance Functor NF where
|
||||
type Dom NF = (->)
|
||||
type Cod NF = (->)
|
||||
map _ ZF = ZF
|
||||
map f (SF r) = SF (f r)
|
||||
|
||||
instance Recursive N where
|
||||
project Z = ZF
|
||||
project (S n) = SF n
|
||||
|
||||
instance Corecursive N where
|
||||
embed ZF = Z
|
||||
embed (SF n) = S n
|
||||
|
||||
data NTy n where
|
||||
ZTy :: NTy 'Z
|
||||
STy :: NTy n -> NTy ('S n)
|
||||
data NFTy r n where
|
||||
ZFTy :: NFTy r 'Z
|
||||
SFTy :: r n -> NFTy r ('S n)
|
||||
type instance Base NTy = NFTy
|
||||
|
||||
instance Functor NTy where
|
||||
type Dom NTy = (:~:)
|
||||
type Cod NTy = (->)
|
||||
map Refl x = x
|
||||
|
||||
instance Functor (NFTy r) where
|
||||
type Dom (NFTy r) = (:~:)
|
||||
type Cod (NFTy r) = (->)
|
||||
map Refl x = x
|
||||
|
||||
instance Functor NFTy where
|
||||
type Dom NFTy = Nat (:~:) (->)
|
||||
type Cod NFTy = Nat (:~:) (->)
|
||||
|
||||
map (Nat f) = Nat \_ -> \case
|
||||
ZFTy -> ZFTy
|
||||
(SFTy r) -> SFTy (f Refl r)
|
||||
|
||||
instance Recursive NTy where
|
||||
project = Nat \_ -> \case
|
||||
ZTy -> ZFTy
|
||||
(STy r) -> SFTy r
|
||||
|
||||
instance Corecursive NTy where
|
||||
embed = Nat \_ -> \case
|
||||
ZFTy -> ZTy
|
||||
(SFTy r) -> STy r
|
||||
|
|
@ -1,78 +0,0 @@
|
|||
module Data.Recursive where
|
||||
|
||||
import Category
|
||||
import Data.Kind (Type)
|
||||
import Data.Maybe (Maybe (Nothing, Just))
|
||||
|
||||
type family Base (t :: i) :: i -> i
|
||||
|
||||
class (Category cat, Endofunctor cat (Base t)) => Recursive cat (t :: i) where
|
||||
project :: cat t (Base t t)
|
||||
|
||||
class (Category cat, Endofunctor cat (Base t)) => Corecursive cat (t :: i) where
|
||||
embed :: cat (Base t t) t
|
||||
|
||||
data N = Z | S N
|
||||
|
||||
type instance Base N = Maybe
|
||||
|
||||
instance Recursive (->) N where
|
||||
project Z = Nothing
|
||||
project (S n) = Just n
|
||||
|
||||
data Fin (n :: N) where
|
||||
FZ :: Fin ('S n)
|
||||
FS :: Fin n -> Fin ('S n)
|
||||
|
||||
data FinF (r :: N -> Type) (n :: N) :: Type where
|
||||
FZF :: FinF r ('S n)
|
||||
FSF :: r n -> FinF r ('S n)
|
||||
|
||||
type instance Base Fin = FinF
|
||||
|
||||
instance Endofunctor Nat FinF where
|
||||
emap (Nat f) = Nat \case
|
||||
FZF -> FZF
|
||||
(FSF r) -> FSF (f r)
|
||||
|
||||
instance Recursive Nat Fin where
|
||||
project = Nat \case
|
||||
FZ -> FZF
|
||||
(FS n) -> FSF n
|
||||
|
||||
data Vec (a :: Type) (n :: N) :: Type where
|
||||
VZ :: Vec a 'Z
|
||||
VS :: a -> Vec a n -> Vec a ('S n)
|
||||
|
||||
data VecF (a :: Type) (r :: N -> Type) (n :: N) :: Type where
|
||||
VZF :: VecF a r 'Z
|
||||
VSF :: a -> r n -> VecF a r ('S n)
|
||||
|
||||
type instance Base (Vec a) = VecF a
|
||||
|
||||
instance Endofunctor Nat (VecF a) where
|
||||
emap (Nat f) = Nat \case
|
||||
VZF -> VZF
|
||||
(VSF x r) -> VSF x (f r)
|
||||
|
||||
instance Recursive Nat (Vec a) where
|
||||
project = Nat \case
|
||||
VZ -> VZF
|
||||
(VS x r) -> VSF x r
|
||||
|
||||
type Algebra cat t a = t a `cat` a
|
||||
|
||||
cata :: Recursive cat t => Algebra cat (Base t) a -> t `cat` a
|
||||
cata alg = alg . emap (cata alg) . project
|
||||
|
||||
newtype Ixr a n = Ixr { getIxr :: Vec a n -> a }
|
||||
|
||||
indexer :: Fin ~> Ixr a
|
||||
indexer = cata (Nat alg)
|
||||
where alg :: FinF (Ixr a) n -> Ixr a n
|
||||
alg = \case
|
||||
FZF -> Ixr (\case (VS x _) -> x)
|
||||
(FSF (Ixr r)) -> Ixr (\case (VS _ xs) -> r xs)
|
||||
|
||||
index :: Vec a n -> Fin n -> a
|
||||
index xs i = getIxr (runNat indexer i) xs
|
||||
Loading…
Reference in New Issue