in Haskell we can define both of these in this way:
data Free (f :: Type -> Type) (a :: Type) = Pure a | Free (f (Free f a))
data Cofree (f :: Type -> Type) (a :: Type) = Cofree a (f (Cofree f a))
But attempting the same definition in lean4 gives some kernel errors which I don't understand. I suspect it has something to do with the termination checker but can't be sure because the errors are not clear:
-- error: (kernel) arg #3 of 'Free.free' contains a non valid occurrence of the datatypes being declared
inductive Free (f : Type → Type) (α : Type) where
| pure : α → Free f α
| free : f (Free f α) → Free f α
-- (kernel) arg #4 of 'Cofree.cofree' contains a non valid occurrence of the datatypes being declaredLean 4
inductive Cofree (f : Type → Type) (α : Type) where
| cofree : α → f (Cofree f α) → Cofree f α
Is there something similar to Agda's TERMINATING pragma? Or is this error related to something else?
A variant of the free monad expressible in terminating languages is the following, aka. the operational monad or the freer monad:
inductive Free (f : Type → Type) (α : Type) where
| pure : α → Free f α
| free : ∀ x, f x -> (x -> Free f α) → Free f α
Free comonad variant using the same trick:
inductive Cofree (f : Type → Type) (α : Type) where
| cofree : ∀ x, α → f x -> (x -> Cofree f α) → Cofree f α
The problem with the original definition is that its well-formedness requires f to be a functor (which is more restrictive than any Type -> Type) satisfying a "strict positivity" condition (which cannot even be expressed in the type system).
If that definition were allowed, you could instantiate Free with the type function f a = a -> a, so that Free f empty is isomorphic to the following illegal type (using Haskell syntax below):
data Bad where
Bad :: (Bad -> Bad) -> Bad
which is bad because it contains the untyped lambda calculus. It can encode non-normalizable terms such as (\x. x x) (\x. x x):
selfapply :: Bad -> Bad
selfapply (Bad x) = x (Bad x)
omega :: Bad
omega = selfapply (Bad selfapply)
The legal variant above doesn't require f to be a functor. It composes the free monad construction with a free functor (also known in Haskell as Coyoneda), which satisfies the strict positivity condition required of inductive types.
data FreeFunctor (f :: Type -> Type) (a :: Type) where
Free :: f x -> (x -> a) -> FreeFunctor f a