Restricted Monads

Stream: Is there code for X?

[Oskar Goldhahn]

I have something that looks like a monad, but am only able to implement the monad functions when the generic types implement a certain typeclass/set of typeclasses. Does there exist code for something like a "restricted monad"?

[Yaël Dillies]

Unfortunately, no, but @Eric Wieser and I have wanted one before. The typical example is docs#finset.monad which could be made computable if we could restrict to types with decidable equality.

[Scott Morrison]

I would say this is exactly what docs4#CategoryTheory.Monad is designed for: it's a monad in an arbitrary category, not just in Type u. :-)

[Scott Morrison]

Then if you need typeclasses, you can build the category of bundled objects, as we do throughout the algebra / order / topology hierarchies.

[Oskar Goldhahn]

Decidable equality is exactly what I need as well. At least at first.

Does the Category Theoretical Monad also support things like do notation?

[Scott Morrison]

No, no do notation. I have no idea whether something might be possible. Sounds fun. :-)

[Eric Wieser]

The thread about refactoring monads to support this is at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Changing.20the.20functor.20typeclasses/near/265813573

[Eric Wieser]

Note that this hits two birds with one stone; it supports restricting monads to specific types, but also removes the universe restrictions that currently force some awkward ulift dances.

[Eric Wieser]

I think #lean4 > universe polymorphic IO discusses the latter aspect, in the context of Lean 4 instead of Lean 3

[Eric Wieser]

Particularly this message:

Leonardo de Moura said:

Eric Wieser I would also be very happy if you could explore the is_monadic approach you suggested. I could only find preliminary experiments in the commit you posted above. You had compelling examples above. Again, I think even if the experiments are not successful, I think we would learn a lot from them. For is_monadic, I am also curious about the interaction with all "gadgets" we use (e.g., transformers, MonadLift, MonadControl, etc). It would also be great to explore whether the two approaches could coexist. I suspect it should be feasible, but I didn't have time to play with your approach yet.

I unfortunately never did find time to look at this, so feel free to explore it yourself if you're particularly motivated

[Oskar Goldhahn]

I'm using lean4 anyways. I might have a look, but I'm just a beginner (literally started two days ago, though I've been eyeing it for a while and have some experience with other proofassistants). I'll probably steal the workaround from finset. Is it right that it's impossible to prove that some predicates are undecidable?

[Eric Wieser]

All predicates are decidable if you assume the axiom of choice (docs4#Classical.decPred)

[Oskar Goldhahn]

That's what I thought. If you want to actually prove things like undecidability of equality for the reals you would need a separate definition of decidable, am I right?

[Kevin Buzzard]

The axiom of choice is neither provable nor disprovable using only lean's logic, so you won't be able to prove anything which contradicts it. In particular you can't prove undecidability of equality for the reals using lean's logic.

[Oskar Goldhahn]

It wouldn't let you prove false, no. Here's how Coq are doing it: https://github.com/uds-psl/coq-library-undecidability

[Eric Wieser]

It wouldn't let you prove false,

Sure it does:

import Mathlib.Data.Real.Basic

example (h : DecidableEq ℝ → False) : False :=
h $ Classical.decEq _

[Eric Wieser]

So at least you need a different meaning of "decidable" to docs4#Decidable if you want to do so

[Oskar Goldhahn]

If you use the same definition for decidability it does. If you use a different one it might not. The reference I linked defines undecidable by reduction to a non-controversial undecidable problem.

[Oskar Goldhahn]

This means that classically everything would be undecidable according to their definition.

[Scott Morrison]

One could implement the following sort of syntactic transformation, providing a version of do notation in an arbitrary category.

Here let's have:

C : Type
[Category C]
W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
m : Monad C

Then one could write something like

def foo : X ⟶ m.obj Z := Do w =>
  let x ← f w
  let y ← g x
  h  y

Note here I'm writing an imaginary Do rather than do, and it acts like a binder with a "variable" w : X, although of course X need not even have an underlying type.
This would be interpreted as if you had written

def foo : X ⟶ m.obj Z := f ≫ m.map g ≫ m.μ.app Y ≫ m.map h ≫ m.μ.app Z

Additional "features" (e.g. using the result of a let binding in a statement later than the subsequent one) would require additional structure on the category C. (e.g. at very least a monoidal category with diagonals).

We would have to call this "Do unchained", rather than "do unchained". Are there existing implementations for general categories/monads in other languages?

[Scott Morrison]

(If anyone would like to try implementing this in Lean 4, please count me in! :-)

[Eric Wieser]

I don't (yet) speak CategoryTheory, but this was something I found myself wanting when using unbundled universal properties

[Adam Topaz]

Fun idea! Here's the "ascii-art" analogue, which is quite easy to define:

import Mathlib.CategoryTheory.Monad.Basic

open CategoryTheory

variable {C : Type u} [Category.{v} C] (M : Monad C)

def CategoryTheory.pure {X Y : C} (f : X ⟶ Y) : X ⟶ M.obj Y := f ≫ M.η.app _

def CategoryTheory.bind {X Y Z : C} (f : X ⟶ M.obj Y) (g : Y ⟶ M.obj Z) : X ⟶ M.obj Z :=
  f ≫ M.map g ≫ M.μ.app _

infixl:55  " >>= " => CategoryTheory.bind

[Adam Topaz]

Where is Lean4's do syntax actually defined?

[Mario Carneiro]

Elab/Do.lean

[Adam Topaz]

Thanks!

[Mario Carneiro]

it's quite complicated, since it supports if, for, try-finally and mutation on top

[Adam Topaz]

yeah, I figured as much

[Mario Carneiro]

for the basic bind sequence thing you don't need most of it

[Mario Carneiro]

I haven't read up on the context here

[Mario Carneiro]

is this about compiling to CCCs?

[Adam Topaz]

I'm just going off of Scott's last message. I also haven't kept up with the whole thread.

[Scott Morrison]

Mario Carneiro said:

is this about compiling to CCCs?

Yes, although the fragment I was talking about required much less than a CCC. (In fact just a monad in any category.)