Free monad

Stream: lean4

[Tage Johansson]

I didn't find any free monad type implemented, so I tried to implement one myself. However, I get a strange error:

inductive FreeM (m : Type u → Type u) (α : Type u) : Type u where
  | pure : α → FreeM m α
  | joined : m (FreeM m α) → FreeM m α

(kernel) arg #3 of 'FreeM.joined' contains a non valid occurrence of the datatypes being declared

Can someone please explain what's wrong and how to make a free monad type in Lean?

Thanks,
Tage

[Eric Wieser]

Adding the word unsafe would presumably fix it

[Jannis Limperg]

This is the strict positivity restriction, which (necessarily) disallows this type. Do we have any documentation on this? #positivity?

[Tage Johansson]

I can add unsafe. But what implications would that have. I think that someone needs to know what he/she is doing when using such a keyword.
Or is there any other way to implement free monads in Lean that is more safe?

[Eric Wieser]

unsafe means "anything that uses this construction will also be unsafe", and any proof marked unsafe cannot be trusted. If all you care about is executing (rather than verifying) code, then unsafe is no concern

[Eric Wieser]

Lean forces you to add unsafe here in the first place because inductive types that recurse in this way cannot be trusted in proofs

[Jannis Limperg]

This blog post shows how (some representation of) the free monad can be defined in a way that doesn't fall foul of strict positivity.

[Eric Rodriguez]

funny thing I discovered whilst trying to learn from the blogpost: why does this code work?

import Mathlib.Logic.Unique

instance : Inhabited (∀ α, α → α) := ⟨fun _ ↦ id⟩

example : Unique (∀ α, α → α) :=
⟨inferInstance,
 fun h ↦ by apply h
            rfl⟩

but if you comment out the apply h, it doesn't? :)

[Eric Rodriguez]

I found this in Lean3 where this solution was originally given by hint, but I think the sneaky thing is even less obvious in Lean4

[Eric Rodriguez]

(oh, this isn't true, don't mind me - I did a very cursory reading of the thing and now realise that this is nonsense... - the Lean issue caused is funny though!)

[Eric Rodriguez]

but without choice, ∀ α, α → α is unique, right?

[Eric Rodriguez]

or well it's undecidable whether it has anything else than id

[Kevin Buzzard]

This sounds like the "theorems for free" paper. If you don't allow stuff like "if alpha = nat then \lam x, 0 else id" then yes, you can only have id. I guess the theorems for free paper explains the assumptions necessary to make this true (but possibly not provable).

[Arthur Adjedj]

It's false with choice, undecidable without, and true with parametricity, though I do not know of any proof-assistant that implements parametricity in its core theory.

[Eric Rodriguez]

the blogpost actually mentions theorems for free

[Verity Scheel]

parametricity (which gives you uniqueness of ∀ α, α → α) and LEM are essentially opposites, and you can prove a strong result about this in HoTT for example: <https://homotopytypetheory.org/2016/02/24/parametricity-and-excluded-middle/>

but parametricity is a hard result to internalize into a theory (in particular, if you had a generic proof of parametricity for polymorphic functions, the proof won’t itself be parametric)

[Verity Scheel]

also, undecidable isn’t the right word to be using here, it should technically be called independent (of the axioms), as in the independence of the continuum hypothesis

[Eric Wieser]

@Eric Rodriguez, that works because you didn't write what you intended to:

def oops : Unique (∀ α, α → α) :=
⟨inferInstance,
 fun h ↦ by apply h
            rfl⟩

#check oops -- oops : Unique (∀ (α : Prop), α → α)

[Eric Wieser]

If you use Unique (∀ α : Sort u, α → α) then you'll find you can't prove it

[Eric Rodriguez]

no, I know Eric, just thought it was an interesting thing that may be overlooked if you're on autopilot :)

[Eric Rodriguez]

I think it adds weight to the "Sort _ should not mean a free universe metavariable but just a newly instantiated universe" argument

[Kyle Miller]

Jannis Limperg said:

This is the strict positivity restriction, which (necessarily) disallows this type.

Is strict positivity too strict in this case? Is it possible to prove a contradiction if it were allowed as a type?

Ah, maybe if α = Empty, you could have m := fun X => if card X = 0 then Unit else Empty.

[Eric Rodriguez]

Verity Scheel said:

parametricity (which gives you uniqueness of ∀ α, α → α) and LEM are essentially opposites, and you can prove a strong result about this in HoTT for example: <https://homotopytypetheory.org/2016/02/24/parametricity-and-excluded-middle/>

but parametricity is a hard result to internalize into a theory (in particular, if you had a generic proof of parametricity for polymorphic functions, the proof won’t itself be parametric)

this proof reminds me of Diaconescu's theorem!

[Tage Johansson]

I was finally able to implement my FreeM based on the article you posted. The definition is quite uggly but I have implemented Monad for it and I have also made a run function FreeM.run [Monad m] (FreeM m a) : m a.
I have not implemented LawfulMonad though so I can't be absolutely sure it is correct.

Thans for the help!

/--
 - A free monad, which turns any functor `m` into a monad.
 - The usual inductive definition of `FreeM` doesn't work in Lean due to strict positivity checking.
 - Therefore we use an EQUIVALENT formulation as described
 - [here](https://blog.poisson.chat/posts/2021-10-20-initial-final-free-monad.html).
 -/
def FreeM (m : Type u → Type v) (α : Type u) : Type _ :=
  ((FreeMonad : Type u → Type u) → [Monad FreeMonad] → ((a : Type u) → m (FreeMonad a) → FreeMonad a) → FreeMonad α)

def FreeM.pure (x : α) : FreeM m α :=
  fun _ _ _ => Pure.pure x

def FreeM.bind (x : FreeM m α) (f : α → FreeM m β) : FreeM m β :=
  fun FreeMonad _ join => Bind.bind (m := FreeMonad) (x FreeMonad join) (fun a => f a FreeMonad join)

def FreeM.run [Monad m] (f : FreeM m α) : m α :=
  f m fun _ x => x >>= id

instance : Monad (FreeM m) where
  pure := FreeM.pure
  bind := FreeM.bind

[Kyle Miller]

@Tage Johansson Here's it cleaned up a little:

class FreeMonad (f : Type u → Type v) (m : Type w → Type u) extends Monad m where
  is_free : (a : Type w) → f (m a) → m a

def FreeM (f : Type u → Type v) (α : Type u) : Type _ :=
  ((m : Type u → Type u) → [FreeMonad f m] → m α)

def FreeM.pure (x : α) : FreeM f α :=
  fun _ _ => Pure.pure x

def FreeM.bind (x : FreeM f α) (g : α → FreeM f β) : FreeM f β :=
  fun m _ => x m >>= fun y => g y m -- or `x m >>= (g · m)` for short

instance [Monad m] : FreeMonad m m where
  is_free _ := Monad.join -- or `(· >>= id)` to be mathlib-free

def FreeM.run [Monad m] (f : FreeM m α) : m α := f m

instance : Monad (FreeM f) where
  pure := FreeM.pure
  bind := FreeM.bind

(I also switched m to f when it's just a function rather than a monad.)

[Kyle Miller]

To define a LawfulMonad instance I think FreeM needs to be modified to be

def FreeM (f : Type u → Type v) (α : Type u) : Type _ :=
  ((m : Type u → Type u) → [FreeMonad f m] → [LawfulMonad m] → m α)

[Kyle Miller]

Yep, with this it's lawful:

class FreeMonad (f : Type u → Type v) (m : Type w → Type u) extends Monad m where
  is_free : (a : Type w) → f (m a) → m a

def FreeM (f : Type u → Type v) (α : Type u) : Type _ :=
  ((m : Type u → Type u) → [FreeMonad f m] → [LawfulMonad m] → m α)

def FreeM.pure (x : α) : FreeM f α :=
  fun _ _ => Pure.pure x

def FreeM.bind (x : FreeM f α) (g : α → FreeM f β) : FreeM f β :=
  fun m _ => x m >>= (g · m)

instance [Monad m] : FreeMonad m m where
  is_free _ := (· >>= id)

def FreeM.run [Monad m] [LawfulMonad m] (f : FreeM m α) : m α := f m

instance : Monad (FreeM f) where
  pure := FreeM.pure
  bind := FreeM.bind

-- Probably there are more precise proofs!
instance : LawfulMonad (FreeM f) where
  map_const := rfl
  id_map x := by funext m; funext; simp [Functor.map, FreeM.bind, FreeM.pure]
  comp_map g h x := by funext m; funext; simp [Functor.map, FreeM.bind, FreeM.pure]
  seqLeft_eq x y := by funext m; funext; simp [Functor.map, FreeM.bind, FreeM.pure, Seq.seq, SeqLeft.seqLeft]
  seqRight_eq x y := by funext m; funext; simp [Functor.map, FreeM.bind, FreeM.pure, Seq.seq, SeqRight.seqRight]
  pure_seq g x := by funext m; funext; simp [Functor.map, FreeM.bind, FreeM.pure, Seq.seq, pure]
  bind_pure_comp f x := by funext m; funext; simp [Functor.map, FreeM.bind, FreeM.pure, pure, bind]
  bind_map f x := by funext m; funext; simp [Functor.map, FreeM.bind, FreeM.pure, pure, bind, Seq.seq]
  pure_bind x f := by funext m; funext; simp [Functor.map, FreeM.bind, FreeM.pure, pure, bind]
  bind_assoc x f g := by funext m; funext; simp [Functor.map, FreeM.bind, FreeM.pure, pure, bind]

[Eric Wieser]

isn't extends Monad m unsafe there because Lean can't infer f?

[Kyle Miller]

Hmm, I suppose so from the FreeMonad.toMonad instance; that's an unfortunate restriction. It shouldn't be hard to turn that into a [Monad m] argument to the class and fix everything else up.

[Tage Johansson]

Eric Wieser said:

isn't extends Monad m unsafe there because Lean can't infer f?

Sorry, but what do you mean? What is unsafe? Why is it "unsafe" to extend with Monad?

[Eric Wieser]

It's the standard "don't write Foo (A B) extends Bar A because the generated Foo.toBar instance has a B that Lean has no way of solving" problem