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

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

-- 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

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

-- 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

-- 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

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

-- 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

data Kind : Type where 
  Set : Kind -- Sets
  ProdK : Kind -> Kind -> Kind -- Product Category

data Ty : Kind -> Type where 
  -- 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
  -- Cartesian product of two types

zanzix

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