Free Monads in Lean4

Stream: new members

[James Caldwell]

Trying to formalize the free monad in Lean4. The obvious definition doesn't work. Here's what I have

inductive Free (f : Type → Type ) : (α : Type ) → Type :=
| pure: α→ Free f α
| impure : (f (Free f α)) → Free f α

(kernel) arg #3 of 'Free.impure' contains a non valid occurrence of the datatypes being declaredLean 4

... any suggestions

[Eric Wieser]

One suggestion would be to search this Zulip for "free monad", which finds a recent thread on the same topic, https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Free.20monad/near/349327430

[James Caldwell]

Thanks @Eric Wieser I knew about the negative occurrence of Free in the definition of impure. The posts you shared from the search indicate that it's very difficult to get around this .