map.idr

public export
data Fix : (Type -> Type) -> Type where
  Fx : f (Fix f) -> Fix f

public export
unfix : Fix f -> f (Fix f)

public export
interface (Functor f) => Recursive (f : Type -> Type) (t : Type) where
  project : t -> f t

public export
data ListF : Type -> Type -> Type where
  NilF : ListF a r
  ConsF : a -> r -> ListF a r

public export
List : Type -> Type
List a = Fix (ListF a)

public export
nil : List a
nil = Fx NilF

public export
cons : a -> List a -> List a
cons x xs = Fx $ ConsF x xs

public export
implementation Functor (ListF a) where
  map f NilF = NilF
  map f (ConsF x xs) = ConsF x (f xs)

public export
implementation {a: _} -> Recursive (ListF a) (List a) where
  project (Fx x) = x

public export
cata :
  {f : _} -> {t : _} ->
  (Recursive f t) =>
  (f a -> a) -> t -> a
cata algebra x = algebra . map (cata algebra) . project $ x

public export
foldr :
  {a : _} -> {b : _} ->
  (a -> b -> b) -> b -> List a -> b
foldr f z = cata alg
  where
    alg : (ListF a b) -> b
    alg NilF = z
    alg (ConsF x xs) = f x xs

public export
implementation Functor List where
  map {a} {b} f = foldr applyCons nil
    where
      applyCons : a -> List b -> List b
      applyCons a = cons $ f a