zanzix

-- Original: https://gist.github.com/MonoidMusician/6c02a07b366813491143c3ad991753e7

-- Natural transformations between presheaves
(~>) : {k : Type} -> (k -> Type) -> (k -> Type) -> Type  
(~>) f g = {a : k} -> f a -> g a 

-- | First define a left kan extension from Type to Presheaves (k -> Type)

-- Takes two functors (Type -> (k -> Type) to a functor (k -> Type) -> (k -> Type) 
data PshLan  : (j, f : Type -> (k -> Type)) -> ((k -> Type) -> (k -> Type))  where 

zanzix

import Data.List.Elem 

-- | Lets start by defining some boilerplate data-types.

-- | Contexts/Variable Environments 
data All : {a : Type} -> (p : a -> Type) -> List a -> Type where 
  Nil : All p [] 
  (::) : {x : a} -> (px : p x) -> (pxs : All p xs) -> All p (x :: xs)

lookup : All p ctx -> Elem x ctx -> p x

zanzix

-- Our goal is to show the common machinery between three different fixpoints:
-- Endofunctors, the universe of regular functors, and (simple) IR codes

-- This is the type of nat. transforms from descriptions to their corresponding functor
Nt : Type -> Type 
Nt u = (desc : u) -> (Type -> Type)

-- our general fixpoint is parametrised by a universe, an interpetation function, and a term of that universe
data Fix : {u : Type} -> Nt u -> (desc : u) -> Type where
  In : {nt : Nt u} -> {desc : u} -> (nt desc) (Fix nt desc) -> Fix nt desc 

zanzix

-- So, let's say we have our data type of terms
data Expr : (Nat -> Type) -> Nat -> Type where 
  Var : Fin n -> Expr f n
  In : f n -> (Fin n -> Expr f m) -> Expr f m 

-- And we have the data types of patterns. So far they're identical, but they'll diverge later. 
data Pat : (Nat -> Type) -> Nat -> Type where 
  PVar : Fin n -> Pat f n
  Nest : f n -> (Fin n -> Pat f m) -> Pat f m 

zanzix

import Data.Fin 

-- Free operad over a signature
data Op : (Nat -> Type) -> Nat -> Type where 
  Var : Fin n -> Op f n 
  In : {n : Nat} -> f n -> (Fin n -> Op f m) -> Op f m

-- Algebra over a functor f
Algebra : (Type -> Type) -> Type -> Type 
Algebra f a = f a -> a 

zanzix

-- Our data-type for signatures
data Signature a = Sig (List a) a

-- Synonym for first-order signatures
infix 4 |-
(|-) : List a -> a -> Signature a
(|-) = Sig

-- Synonym for second-order signatures
infix 4 ||-

zanzix

infixr 5 ~~> -- Morphisms of graphs

-- | Boilerplate for recursion schemes

-- Objects are graphs 
Graph : Type -> Type 
Graph o = o -> o -> Type 

-- Morphisms are vertex-preserving transformations between graphs

zanzix

-- standard algebra 
Algebra : (Type -> Type) -> Type -> Type  
Algebra f a = f a -> a

-- Mendler Algebra == Algebra (Coyoneda f) a
MAlgebra : (Type -> Type) -> Type -> Type
MAlgebra f c = {x : Type} -> (x -> c) -> f x -> c

data Coyoneda : (Type -> Type) -> Type -> Type  where
  Coyo : (a -> b) -> f a -> Coyoneda f b

zanzix

-- Profunctor composition
data CompP : (k1 -> k2 -> Type) -> (k2 -> k3 -> Type) -> k1 -> k3 -> Type where 
InComp : {k1, k2, k3 : Type} -> {a : k1} -> {b : k2} -> {c : k3} -> {p : k1 -> k2 -> Type} -> {q : k2 -> k3 -> Type} 
  -> p a b -> q b c -> CompP p q a c 

-- Natural transformations over profunctors
Nt : {k1, k2 : Type} -> {arr : t -> t -> Type} -> (k1 -> k2 -> t) -> (k1 -> k2 -> t) -> Type  
Nt f g = {a : k1} -> {b : k2} -> arr (f a b) (g a b) 

-- Category of idris functions

zanzix

infixr 5 +++
infixr 5 ***

-- A list over a type
-- data List : Type -> Type where 
--   Nil : List a 
--   (::) : a -> List a -> List a 

Graph : Type -> Type 
Graph obj = obj -> obj -> Type