CODEWITHSUNDEEP
haskellmonadscategory-theoryleancomonad
André Muricy
André Muricy

Reputation: 131

How to define free monads and cofree comonads in Lean4?

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?

Upvotes: 5

Views: 383

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33519

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

Upvotes: 9

Related Questions