zanzix

module Term
import Ty

export infixr 5 ~>

public export
data Ctx : Type where
  Nil : Ctx
  (::) : {k : Kind} -> Ty k -> Ctx -> Ctx

zanzix

import Data.Relevant.Cover as Rel
import Data.Linear.Cover as Lin

import Data.Vect

Ctx : Type
Ctx = List String

export infixr 5 ~>
data Ty : (typeVars : Ctx) -> Type where

zanzix

namespace OpKind
  data Kind : Type where 
    Set : Kind -- Set
    Op : Kind -> Kind -- Set^op
  
  data Ty : Kind -> Type where 
    NAT : Ty k 
    Zero : Ty k
    Add : Ty k -> Ty k -> Ty k 
    One : Ty k

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

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

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