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 

zanzix

-- We define uncurried versions of Pair and Either to help with type-checking
data Tuple : (Type, Type) -> Type where 
  MkTuple : a -> b -> Tuple (a, b)

data Sum : (Type, Type) -> Type where 
  Left : a -> Sum (a, b)
  Right : b -> Sum (a, b)

-- These are bifunctor versions of projections/injections
data Fst : (Type, Type) -> Type where 

zanzix

infixr 5 ~> -- Morphism of indexed functors
infixr 5 ~~> -- Morphism of graphs/doubly-indexed functors
infixr 5 :~> -- Morphism of multi-graphs
infixr 5 :~:> -- Morphism of poly-graphs 

namespace Fix1 
  -- Objects are Types

  -- Morphisms are functions between types (->)

zanzix

import Data.List.Elem 

data Ty = U | Base | Prod Ty Ty | Sum Ty Ty | Imp Ty Ty | Sub Ty Ty | S Ty 

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

infixr 5 ~> 
(~>) : Ty -> Ty -> Ty

zanzix

-- | Concategory
data Concat : List o -> List o -> Type where
  -- Identity
  Id : Concat as as
  -- Sequential composition
  Seq : Concat bs cs -> Concat as bs -> Concat as cs
  -- Par
  Par : {as, bs, cs, ds : List o} -> Concat as bs -> Concat cs ds -> Concat (as++cs) (bs++ds)
  -- Symmetry
  Sym : Concat (x ++ y) (y ++ x)

zanzix

-- Greatest fixpoint of (1 + a * x), "possibly-terminating streams"
data Colist : Type -> Type where 
  Nil : Colist a 
  (::) : a -> Inf (Colist a) -> Colist a 

-- Environment indexed by a colist
data CoAll : (p : k -> Type) -> Colist k -> Type where 
  Empty : CoAll p Nil
  Cons : {p : k -> Type} -> p x -> Inf (CoAll p xs) -> CoAll p (x :: xs)