Haskell is a bad programming language which requires too much boilerplate.

* Added Vec, indexer for Vec
* Added Pi quantifiers

monoids-in-the-categoy-of-endofunctors.cabal

@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: d2b69687ecaa1f177ecb0533b202092619c3c90b1107255e2fdaef7e70b84af5
+-- hash: ccbe65df6ff8c44717a5cad0ce46e39a026a6e35f58b942545be94a2080cc645
 
 name:           monoids-in-the-categoy-of-endofunctors
 version:        0.1.0.0
@@ -34,6 +34,8 @@ library
       Data.Dict
       Data.Fin
       Data.Nat
+      Data.Vec
+      Quantifier
   other-modules:
       Paths_monoids_in_the_categoy_of_endofunctors
   hs-source-dirs:

src/Category/Functor.hs

@@ -3,6 +3,8 @@ module Category.Functor where
 
 import Category.Base
 import Data.Kind (Type)
+import Data.Maybe (Maybe (Nothing, Just))
+import Quantifier
 
 class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
     type Dom f :: i -> i -> Type
@@ -18,6 +20,9 @@ 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
 
+runNat :: Nat q r f g -> forall a. Obj q a -> r (f a) (g a)
+runNat (Nat f) = f
+
 instance Semigroupoid r => Semigroupoid (Nat q r) where
     (.) (Nat f) (Nat g) = Nat \p -> (f p . g p)
 
@@ -58,15 +63,26 @@ 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 }
+newtype Const (cat :: i -> i -> Type) (a :: Type) (b :: i) = Const { getConst :: a }
 
-instance Functor (Const a) where
+instance Category cat => Functor (Const cat a) where
     -- FIXME
-    type Dom (Const a) = (:~:)
-    type Cod (Const a) = (->)
+    type Dom (Const cat a) = cat
+    type Cod (Const cat a) = (->)
     map _ (Const x) = Const x
 
-instance Functor Const where
-    type Dom Const = (->)
-    type Cod Const = Nat (:~:) (->)
+instance Category cat => Functor (Const cat) where
+    type Dom (Const cat) = (->)
+    type Cod (Const cat) = Nat cat (->)
     map f = Nat \_ -> \case (Const x) -> Const (f x)
+
+instance Functor Maybe where
+    type Dom Maybe = (->)
+    type Cod Maybe = (->)
+    map _ Nothing = Nothing
+    map f (Just x) = Just (f x)
+
+instance {-# OVERLAPPABLE #-} Pi ty => Functor (Ty ty) where
+    type Dom (Ty ty) = (:~:)
+    type Cod (Ty ty) = (->)
+    map Refl x = x

src/Data/Fin.hs

@@ -40,8 +40,8 @@ instance Corecursive Fin where
         FZF -> FZ
         (FSF r) -> FS r
 
-fin2nat :: Nat (:~:) (->) Fin (Const N)
+fin2nat :: Nat (:~:) (->) Fin (Const (:~:) N)
 fin2nat = cata (Nat \_ -> alg)
-    where alg :: FinF (Const N) n -> Const N n
+    where alg :: FinF (Const (:~:) N) n -> Const (:~:) N n
           alg FZF = Const Z
           alg (FSF (Const n)) = Const (S n)

src/Data/Nat.hs

@@ -2,57 +2,65 @@ module Data.Nat where
 
 import Category
 import Category.Functor.Foldable
+import Data.Kind (Type)
+import Data.Maybe (Maybe (Nothing, Just))
+import Quantifier
 
 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 Pi N where
+    type PiCat N = (->)
+    data Ty N :: N -> Type where
+        ZTy :: Ty N 'Z
+        STy :: Ty N n -> Ty N ('S n)
+    depi ZTy = Z
+    depi (STy n) = S (depi n)
+
+class NTyC n where
+    nTy :: Ty N n
+instance NTyC 'Z where
+    nTy = ZTy
+instance NTyC n => NTyC ('S n) where
+    nTy = STy nTy
+
+instance PiC N where
+    type TyC N = NTyC
+    depic = nTy
+
+data NTyF r n where
+    ZTyF :: NTyF r 'Z
+    STyF :: r n -> NTyF r ('S n)
+
+instance Functor (NTyF r) where
+    type Dom (NTyF r) = (:~:)
+    type Cod (NTyF r) = (->)
+    map Refl x = x
+
+instance Functor NTyF where
+    type Dom NTyF = Nat (:~:) (->)
+    type Cod NTyF = Nat (:~:) (->)
+    map (Nat f) = Nat \_ -> \case
+        ZTyF -> ZTyF
+        (STyF r) -> STyF (f Refl r)
+
+type instance Base N = Maybe
 
 instance Recursive N where
-    project Z = ZF
-    project (S n) = SF n
+    project Z = Nothing
+    project (S n) = Just n
 
 instance Corecursive N where
-    embed ZF = Z
-    embed (SF n) = S n
+    embed Nothing = Z
+    embed (Just 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
+type instance Base (Ty N) = NTyF
 
-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
+instance Recursive (Ty N) where
     project = Nat \_ -> \case
-        ZTy -> ZFTy
-        (STy r) -> SFTy r
+        ZTy -> ZTyF
+        (STy r) -> STyF r
 
-instance Corecursive NTy where
+instance Corecursive (Ty N) where
     embed = Nat \_ -> \case
-        ZFTy -> ZTy
-        (SFTy r) -> STy r
+        ZTyF -> ZTy
+        (STyF r) -> STy r

src/Data/Vec.hs

@@ -0,0 +1,62 @@
+module Data.Vec where
+
+import Category
+import Category.Functor.Foldable
+import Data.Fin
+import Data.Kind (Type)
+import Data.Nat
+import Quantifier
+
+data Vec a n where
+    VZ :: Vec a 'Z
+    VS :: a -> Vec a n -> Vec a ('S n)
+data VecF a r n where
+    VZF :: VecF a r 'Z
+    VSF :: a -> r n -> VecF a r ('S n)
+type instance Base (Vec a) = (VecF a)
+
+instance Functor (Vec a) where
+    type Dom (Vec a) = (:~:)
+    type Cod (Vec a) = (->)
+    map Refl x = x
+
+instance Functor Vec where
+    type Dom Vec = (->)
+    type Cod Vec = Nat (:~:) (->)
+    map f = Nat \_ -> \case
+        VZ -> VZ
+        (VS x r) -> VS (f x) (runNat (map f) Refl r)
+
+instance Functor (VecF a r) where
+    type Dom (VecF a r) = (:~:)
+    type Cod (VecF a r) = (->)
+    map Refl x = x
+
+instance Functor (VecF a) where
+    type Dom (VecF a) = Nat (:~:) (->)
+    type Cod (VecF a) = Nat (:~:) (->)
+    map (Nat f) = Nat \_ -> \case
+        VZF -> VZF
+        (VSF x r) -> VSF x (f Refl r)
+
+instance Functor VecF where
+    type Dom VecF = (->)
+    type Cod VecF = Nat (Nat (:~:) (->)) (Nat (:~:) (->))
+    map f = Nat \_ -> Nat \_ -> \case
+        VZF -> VZF
+        (VSF x r) -> VSF (f x) r
+
+newtype Ixr ty r a = Ixr { getIxr :: ty a -> r }
+
+instance Functor (Ixr ty r) where
+    type Dom (Ixr ty r) = (:~:)
+    type Cod (Ixr ty r) = (->)
+    map Refl x = x
+
+indexer :: Nat (:~:) (->) Fin (Ixr (Vec a) a)
+indexer = cata (Nat \_ -> \case
+    FZF -> Ixr \case VS x _ -> x
+    (FSF (Ixr r)) -> Ixr \case VS x xs -> r xs)
+
+index :: Fin n -> Vec a n -> a
+index = getIxr . runNat indexer Refl

src/Quantifier.hs

@@ -0,0 +1,22 @@
+module Quantifier where
+
+import Data.Kind (Constraint, Type)
+import Data.Maybe (Maybe (Nothing, Just))
+
+-- | An explicit dependent quantifier.
+class Pi (ty :: Type) where
+    type PiCat ty :: i -> i -> Type
+    data Ty ty :: ty -> Type
+    depi :: forall a. Ty ty a -> ty
+
+-- | An implicit dependent quantifier.
+class Pi ty => PiC (ty :: Type) where
+    type TyC ty :: ty -> Constraint
+    depic :: forall a. TyC ty a => Ty ty a
+
+instance Pi a => Pi (Maybe a) where
+    data Ty (Maybe a) :: Maybe a -> Type where
+        NothingTy :: Ty (Maybe a) 'Nothing
+        JustTy :: Ty a x -> Ty (Maybe a) ('Just x)
+    depi NothingTy = Nothing
+    depi (JustTy x) = Just (depi x)