gistfile1.txt

data FreeA : (Type -> Type) -> Type -> Type where
  Ap : f a -> FreeA f (a -> b) -> FreeA f b
  Pure : a -> FreeA f a

implementation Functor (FreeA f) where
  map f (Pure x) = Pure (f x)
  map f (Ap x y) = Ap x ((f .) <$> y) -- y <*> x

implementation Applicative (FreeA f) where
  pure = Pure
  (Pure f) <*> y = map f y
  (Ap x y) <*> z = assert_total $ Ap x (flip <$> y <*> z)

data ListF : Type -> Type -> Type where
  Empty : ListF b a
  Cons : b -> a -> ListF b a

liftAp : f a -> FreeA f a
liftAp x = Ap x (Pure id)

empty : FreeA (ListF a) ()
empty = liftAp Empty

cons : b -> FreeA (ListF b) ()
cons x = liftAp (Cons x ())

foo : FreeA (ListF Int) Int
foo = [| id empty (cons (+1)) |]