Defining a `Monad` Instance for a `Quotient`ed type

Stream: lean4

[Alex Keizer]

I have some type function Raw : Type → Type, with Q : Type → Type := fun α => Quotient _ defined as a Quotient over the Raw type. I've managed to define bind (x : Raw α) (f : α → Raw β) : Raw β, but I'm struggling with how to lift this function into a bind over Q.

Quotient.lift\2 does not work as-is, because it expects both arguments to be quotients, and in my case f is not a quotient, but a function returning a quotient.

I've found Quotient.choice, which allows me to convert the "function-of-quotients" into a "quotient of functions", which I can then successfully lift. However, it's noncomputable, and I really want to be able to both reason about and compute with Q.

I what I'm trying just fundamentally impossible? Or have I missed some other option?

[Eric Wieser]

Can you make a mwe?

[Alex Keizer]

Sure! Here's a very simplified version (in reality, Raw is not just Option, and the quotient relation is not just equality, but I think it still has the same problem as I'm facing)

/-- The `Raw` type, let's just take `Option` for the `MWE` -/
def Raw := Option

def Raw.bind : Raw α → (α → Raw β) → Raw β :=
  Option.bind

/-- For simplicity, we're just quotienting through equality -/
def Raw.setoid α : Setoid (Raw α) where
  r := Eq
  iseqv := {
    refl := fun _ => rfl
    symm := Eq.symm
    trans := Eq.trans
  }

/-- Define `Q` as a quotient over `Raw` -/
def Q (α : Type) := Quotient (Raw.setoid α)

/-- Now, how do I actually define `bind` over `Q`? -/
def Q.bind (x : Q α) (f : α → Q β) : Q β :=
  sorry

[Alex Keizer]

My first instinct was to use Quotient.lift₂, but that doesn't work with f a function

def Q.bind (x : Q α) (f : α → Q β) : Q β :=
  Quotient.lift₂ _ _ x f
--                     ^ `application type mismatch` (i.e., `f` is not a quotient)

[Eric Wieser]

I think your missing piece is

def missing (x : Raw (Q α)) : Q α :=

or perhaps

def missing (x : Raw (Q α)) : Q (Raw α) :=

[Alex Keizer]

Hmm, I'm trying for Raw (Raw α) -> Raw α at the moment, which sould be easy, since Raw is a Monad (just not a lawful one). Thanks for the extra inspiration!

[Alex Keizer]

And then, hopefully I should be able to lift that into Q (Q \a) -> Q(\a)

[Eric Wieser]

Something like

/-- Now, how do I actually define `bind` over `Q`? -/
def Q.bind (x : Q α) (f : α → Q β) : Q β := by
  refine Quotient.lift
    (fun a => Quotient.map' (Raw.bind · id) ?_ (missing (a.map f))) ?_ x
  · intros a a' ha
    dsimp
    sorry
  · simp
    sorry

[Eric Wieser]

Raw (Raw α) -> Raw α is Raw.bind · id

[Alex Keizer]

Thanks! Unfortunately in my real code, Raw involves a universe bump, so I'm not quite there yet, but your snippet gives me a new direction to explore!

[Adam Topaz]

I think if Raw bumps the universe then the only option you really have is to define bind and get the monad instance that way, since Raw (Raw A) wouldn't work

[Alex Keizer]

I have defined bind on Raw, but how would I do so for the quotient Q, without going through Raw (Raw A)? Would Raw (Q A) work? I'd guess not, since Q also bumps the universe

[Adam Topaz]

hmmmm I see the issue now.

[Adam Topaz]

to define bind directly you would need to lift along the family A -> Q B which would involve choice.

[Adam Topaz]

are your Raw A actually in a higher universe, or only by accident due to some inductive construction? In other words, can you get rid of the universe bump?

[Alex Keizer]

I suspect I can't get rid of the universe bump, but don't know for sure.

To add some context: I'm trying to define a monad for potentially non-terminating computations which is both computable, and can be reasoned about. The design so far is to represent computations as state machines, so Raw is actually:

structure PartialM.Raw (α : Type u) : Type (u+1) where
  {σ : Type u}
  (next : σ → PartialStep σ α)
  (state : σ)

I want to hide this state-machine encoding from the user, so I've made the state type \sigma a field of the structure, and that is what causes the bump

[Alex Keizer]

The quotient comes in because there can be different state machines that represent the same computation / final result, so I have to quotient the type to get a lawful monad

[Alex Keizer]

Ooh, I might have a solution: if I fix the state \sigma to live in Type, rather than the polymorphic Type u, then it might work out.

[Adam Topaz]

No, the universe of this Raw will still be one higher since you're quantifying over sigma.

[Alex Keizer]

The universe bump still happens, but I should be able to define join : Raw (Raw A) -> A regardless.

[Adam Topaz]

oh I see

[Adam Topaz]

but then you will need Raw to be universe polymorphic.

[Alex Keizer]

The problem I was running into was not the universe of the result, but rather that the joined state machine has to store the state of the originally nested state machine, which could have state in a higher universe

[Alex Keizer]

Adam Topaz said:

but then you will need Raw to be universe polymorphic.

Indeed, and it is (just not in the MWE, sorry for the confusion there)

[Markus Schmaus]

Alex Keizer said:

To add some context: I'm trying to define a monad for potentially non-terminating computations which is both computable, and can be reasoned about.

This sounds a lot like what I have been trying to do recently. Very recently, I have come to the conclusion that there is a better approach. It should be possible to generalize the concept of a monad somewhat to allow for some heterogeneity, such that it's possible to use the state machine directly in monadic computations.

[Alex Keizer]

Cool! I vaguely remember some talk about heterogenous bind on this chat, was that you? Is this available somewhere, I'd love to have a look.
Still, I would like to use this monad in a an existing development, which extensively uses Monad and LawfulMonad, so I'm still hoping I can get this through somehow

[Markus Schmaus]

It wasn't me. This idea is very new, so I don't have any code yet, but I sent you a DM with the general outline.