Algebras and paramorphisms for a simple class of signatures in Idris2

Para.idr

import Data.Fin
import Data.Vect
import Data.Vect.Quantifiers

-- No telescopes, no indexing (parameters still possible), no displayed
-- algebras, just paramorphisms.

-- This is the type of descriptions/signatures for constructor data.
-- Each operation (constructor) is a sequence of arguments, either data or
-- recursive calls.
data Op : Type where
  Return : Op
  Data : (b : Type) -> (b -> Op) -> Op
  Rec : Op -> Op
  
-- A signature is a vector of operations. We can have more data here like
-- constructor name or other attributes.
Sig : Nat -> Type
Sig n = Vect n Op

-- The type of inputs for the given operation, for carrier type `f`
data Input : Op -> Type -> Type where
  InpReturn : Input Return f
  InpData : (x : b) -> Input (op x) f -> Input (Data b op) f
  InpRec : f -> Input op f -> Input (Rec op) f

-- Input is an endofunctor---the interpretation of a description Op
Functor (Input op) where
  map f InpReturn = InpReturn
  map f (InpData x y) = InpData x (map f y)
  map f (InpRec x y) = InpRec (f x) (map f y)

-- The type of algebras for the given signature `sig`
--
-- We reuse vector quantifiers from stdlib because this is pretty
-- convenient: for each operation in the signature, we have an algebra
-- of Input. Overall we call the whole thing an algebra for the signature.
Alg : Sig n -> Type -> Type
Alg sig t = All (\op => Input op t -> t) sig

-- The initial algebra for a signature is just a 'free' algebra for
-- each constructor in the signature.
data Initial : Sig n -> Type where
  Ctor : (i : Fin n) -> (inp : Input (index i sig) (Initial sig)) -> Initial sig
  
-- The initial algebra is an algebra
initialAlg : {n : _} -> {sig : Sig n} -> Alg sig (Initial sig)
initialAlg = tabulate Ctor

-- Recursor for algebras
rec : Alg sig a -> Initial sig -> a
rec alg (Ctor i inp) = index i alg (map (rec alg) inp)

-- Paramorphisms

-- This is similar to the type of algebras but includes an extra bit
-- of data each time a recursive call is made: the original argument.
-- We also make the recursive call lazy here to avoid computing what we
-- don't need.

Para : Sig n -> Type -> Type -> Type
Para sig a f = All (\op => Input op (a, Lazy f) -> f) sig

para : Para sig (Initial sig) f -> Initial sig -> f
para paraAlg (Ctor i inp) = index i paraAlg (map (\i => (i, delay $ para paraAlg i)) inp)

-- Natural numbers

NatSig : Sig 2
NatSig = [Return, Rec Return]

NAT : Type
NAT = Initial NatSig

ZE : NAT
ZE = Ctor FZ InpReturn

SU : NAT -> NAT
SU n = Ctor (FS FZ) (InpRec n InpReturn)

natRec : a -> (a -> a) -> NAT -> a
natRec z s = rec [\InpReturn => z, \(InpRec x InpReturn) => s x]

natPara : a -> (NAT -> a -> a) -> NAT -> a
natPara z s = para [\InpReturn => z, \(InpRec (w, x) InpReturn) => s w x]

-- Lists

ListSig : Type -> Sig 2
ListSig a = [Return, Data a (\_ => Rec Return)]

LIST : Type -> Type
LIST a = Initial (ListSig a)

NIL : LIST a
NIL = Ctor FZ InpReturn

CONS : a -> LIST a -> LIST a
CONS x xs = Ctor (FS FZ) (InpData x (InpRec xs InpReturn))

listRec : b -> (a -> b -> b) -> LIST a -> b
listRec n c = rec [\InpReturn => n, \(InpData x (InpRec xs InpReturn)) => c x xs]

listPara : b -> (a -> LIST a -> b -> b) -> LIST a -> b
listPara n c = para [\InpReturn => n, \(InpData x (InpRec (w, xs) InpReturn)) => c x w xs]