Sums and Products in Sets, Endofunctors, and Endoprofunctors using Kinds

ExponentialKind.idr

import Data.List.Elem 
import Data.List.Quantifiers

-- Kinds are categories
data Kind : Type where 
  Set : Kind -- Sets
  ProdK : Kind -> Kind -> Kind -- Product Category
  Exp : Kind -> Kind -> Kind -- Exponential Category

-- Types are functors
data Ty : Kind -> Type where 

  -- Algebraic data types
  Zero : Ty k 
  One : Ty k
  Sum : Ty k -> Ty k -> Ty k 
  Prod : Ty k -> Ty k -> Ty k

  -- Functor composition
  Ten : Ty (Exp Set Set) -> Ty (Exp Set Set) -> Ty (Exp Set Set)

  -- First and Second projections from a product category
  Fst : {k1, k2 : Kind} -> Ty (ProdK k1 k2) -> Ty k1
  Snd : {k1, k2 : Kind} -> Ty (ProdK k1 k2) -> Ty k2

export infixr 5 :*: 
(:*:) : Ty n -> Ty n -> Ty n 
(:*:) = Prod 

export infixr 5 :+: 
public export
(:+:) : Ty n -> Ty n -> Ty n
(:+:) = Sum 

const2 : Type -> Type -> Type -> Type 
const2 a b c = a

Hom : Type -> Type -> Type 
Hom a b = a -> b 

-- Kinds are interpreted into types
EvalKind : Kind -> Type 
EvalKind Set = Type -- Set is just Type
EvalKind (ProdK k1 k2) = (EvalKind k1, EvalKind k2) -- Product kind is a product of types
EvalKind (Exp k1 k2) = (EvalKind k1 -> EvalKind k2) -- Function kind is a function of types

EvalTy : (k : Kind) -> Ty k -> EvalKind k 
EvalTy Set One = Unit
EvalTy Set Zero  = Void
EvalTy Set (Sum x z)  = Either (EvalTy Set x ) (EvalTy Set z ) 
EvalTy Set (Prod x z)  = (EvalTy Set x , EvalTy Set z )

-- Higher order functors 
EvalTy (Exp Set Set) Zero  = const Unit
EvalTy (Exp Set Set) One  = id
EvalTy (Exp Set Set) (Sum f1 f2) = \a => 
  Either (EvalTy (Exp Set Set) f1 a) (EvalTy (Exp Set Set) f2 a)
EvalTy (Exp Set Set) (Prod f1 f2) = \a =>
  (EvalTy (Exp Set Set) f1 a, EvalTy (Exp Set Set) f2 a)
EvalTy (Exp Set Set) (Ten f1 f2)  
  = \y => EvalTy (Exp Set Set) f1  ((EvalTy (Exp Set Set) f2 ) y)

-- Functors over Prof
EvalTy (Exp Set (Exp Set Set)) Zero  = const2 Unit
EvalTy (Exp Set (Exp Set Set)) One  = Hom
EvalTy (Exp Set (Exp Set Set)) (Sum p1 p2) = \a, b =>
  Either (EvalTy (Exp Set (Exp Set Set)) p1 a b) (EvalTy (Exp Set (Exp Set Set)) p2 a b)
EvalTy (Exp Set (Exp Set Set)) (Prod p1 p2) = \a, b =>
  (EvalTy (Exp Set (Exp Set Set)) p1 a b, EvalTy (Exp Set (Exp Set Set)) p2 a b)
EvalTy (ProdK k1 k2) p = (EvalTy k1 (Fst p), EvalTy k2 (Snd p))
EvalTy s (Fst {k1=s, k2} a) = fst (EvalTy (ProdK s k2) a)
EvalTy s (Snd {k1, k2=s} a) = snd (EvalTy (ProdK k1 s) a)

-- What are functors in arbitrary functor categories?
EvalTy (Exp x y) e  = ?notyet 

-- Given a kind, we need to determine the morphisms of its category
EvalArr : (k : Kind) -> EvalKind k -> EvalKind k -> Type 
EvalArr Set a b = a -> b  -- Sets and functions
EvalArr (ProdK k1 k2) l r = -- Product category k1 k2 has a pair of morphisms from k1 and k2
  (EvalArr k1 (fst l) (fst r), EvalArr k2 (snd l) (snd r))
EvalArr (Exp Set Set) f g = {a : Type} -> f a -> g a -- natural transforms between functors
EvalArr (Exp Set (Exp Set Set)) p q = {a, b : Type} -> p a b -> q a b -- natural transforms between profunctors
--  what are the hom objects of general functor categories?
EvalArr (Exp x y) p q = ?undefined'


infixr 5 *** 
infixr 5 +++

data Term : Ty k -> Ty k -> Type where
  Id : Term x x
  (.) : {b : Ty k} -> Term b c -> Term a b -> Term a c

  (***) : {a, b, c : Ty k} -> Term a b -> Term a c -> Term a (b :*: c)
  PrjL : {a, b : Ty k} -> Term (a :*: b) a
  PrjR : {a, b : Ty k} -> Term (a :*: b) b

  (+++) : {a, b, c : Ty k} -> Term a c -> Term b c -> Term (a :+: b) c
  InjL : Term a (a :+: b)
  InjR : Term b (a :+: b)

factorPair : (a -> b) -> (a -> c) -> a -> (b, c) 
factorPair f g a = (f a, g a) 

factorSum : (b -> a) -> (c -> a) -> Either b c -> a  
factorSum f g (Left x) = f x 
factorSum f g (Right x) = g x 

-- Terms are evaluated in a category based on their kind
partial
eval : (k : Kind) -> {s, t : Ty  k}  
    -> Term s t -> EvalArr k (EvalTy k s) (EvalTy k t) 
eval Set Id   = id -- identity for functions id : a -> a
eval Set (f . g)  = (eval Set f ) . (eval Set g)
eval Set (f *** g)  = factorPair (eval Set f) (eval Set g)
eval Set  PrjL  = fst
eval Set  PrjR  = snd
eval Set (f +++ g)  = factorSum (eval Set f ) (eval Set g )  
eval Set  InjL  = Left 
eval Set  InjR  = Right 

-- evaluate terms into the category of endofunctors
eval (Exp Set Set) Id  = id -- identity for functors id : {a : Type} -> f a -> f a  
eval (Exp Set Set) (f . g)  = 
  (eval (Exp Set Set) f ) . (eval (Exp Set Set) g )
eval (Exp Set Set) (f *** g)  = 
  factorPair (eval (Exp Set Set) f ) (eval (Exp Set Set) g )
eval (Exp Set Set)  PrjL  = fst
eval (Exp Set Set)  PrjR  = snd
eval (Exp Set Set) (f +++ g)  = 
  factorSum (eval (Exp Set Set) f ) (eval (Exp Set Set) g )  
eval (Exp Set Set) InjL  = Left 
eval (Exp Set Set) InjR  = Right

-- evaluate terms into the category of endo profunctors
eval (Exp Set (Exp Set Set)) Id  = id -- identity for profunctors id : {a, b : Type} -> p a b -> p a b 
eval (Exp Set (Exp Set Set)) (f . g)  = 
  (eval (Exp Set (Exp Set Set)) f ) . (eval (Exp Set (Exp Set Set)) g )
eval (Exp Set (Exp Set Set)) (f *** g)  = 
  factorPair (eval (Exp Set (Exp Set Set)) f) (eval (Exp Set (Exp Set Set)) g )
eval (Exp Set (Exp Set Set)) PrjL  = fst
eval (Exp Set (Exp Set Set)) PrjR  = snd
eval (Exp Set (Exp Set Set)) (f +++ g)  = 
  factorSum (eval (Exp Set (Exp Set Set)) f) (eval (Exp Set (Exp Set Set)) g )  
eval (Exp Set (Exp Set Set)) InjL  = Left 
eval (Exp Set (Exp Set Set)) InjR  = Right

eval (ProdK k1 k2) Id = (eval k1 Id, eval k2 Id)