Skip to content

Instantly share code, notes, and snippets.

@zanzix
zanzix / Fixpoints.idr
Last active January 19, 2024 12:12
Comparison of several fixpoints in Idris
View Fixpoints.idr
-- 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
zanzix / Pattern.idr
Created November 25, 2023 17:53
Pattern Matching Operads
View Pattern.idr
-- 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
zanzix / Operad.idr
Created November 10, 2023 20:40
Free Operad as a free relative monad over Fin
View Operad.idr
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
zanzix / SOAT.idr
Created October 29, 2023 18:09
Second-Order Algebraic Theories
View SOAT.idr
-- 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
zanzix / CartCata.idr
Last active October 27, 2023 07:39
Free Cartesian Categories using Recursion Schemes
View CartCata.idr
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
zanzix / Fix.idr
Last active October 20, 2023 16:29
Recursion schemes in Idris starter pack
View Fix.idr
-- 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
zanzix / ProfBicat.idr
Last active September 30, 2023 02:56
Bicategory of Profunctors
View ProfBicat.idr
-- 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
zanzix / MonoidalTricategory.idr
Last active October 23, 2023 20:07
From monoid to monoidal tricategory
View MonoidalTricategory.idr
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
zanzix / Bicat.idr
Last active September 26, 2023 22:16
Bicategory constraint issue
View Bicat.idr
-- 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
zanzix / Fix.idr
Last active September 23, 2023 01:17
Fixpoints of indexed functors, graphs, multi-graphs, poly-graphs
View Fix.idr
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 (->)