Monad over prop?

Stream: lean4

[James Gallicchio]

Is there a reason monads can't be defined for constructors of type Sort u -> Type v instead of Type u -> Type v?

I tried redefining them over sort, but ended up with a strange error message about default implementations having metavariables. MWE:

class PBind (m : Sort u → Type v) where
  bind : {p q : Sort u} → m α → (α → m β) → m β

class PPure (f : Sort u → Type v) where
  pure {α : Sort u} : α → f α

class PFunctor (f : Sort u → Type v) : Type (max (u+1) v) where
  map      : {α β : Sort u} → (α → β) → f α → f β

class PApplicative (f : Sort u → Type v) extends PFunctor f, PPure f

class PMonad (m : Sort u → Type v) extends PApplicative m, PBind m : Type (max (u+1) v) where
  map {α β} f x := PBind.bind x fun a => PPure.pure (f a)

[Henrik Böving]

Making a Monad that operates on Prop doesn't seem too useful to me, consider:

  pure {α : Sort u} : α → f α

if α is from Prop this cannot be a regular function that eliminates into meaningful data (i.e. Type u) due to proof irrelevance right?

[Mario Carneiro]

I get a unused variable warning on p q : Sort u in bind, that should be a clue

[Mario Carneiro]

if you remove them then it compiles

[James Gallicchio]

oh LOL I renamed them and never changed the uses... thanks

[James Gallicchio]

Henrik Böving said:

if α is from Prop this cannot be a regular function that eliminates into meaningful data (i.e. Type u) due to proof irrelevance right?

Not computationally useful data, no. In my use case I have some computationally useful data (whether a test passed or not) but I'm also carrying proof terms around to make sure I'm actually testing the property I say I'm testing.

[Henrik Böving]

Oh that's fun yes, I did some work regarding this over here: https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/Testing/SlimCheck

[James Gallicchio]

Yes, exactly that! :big_smile:

[James Gallicchio]

After fixing the typo mario pointed out, it seems like everything is working fine. So now I'm wondering why Monad in the prelude isn't defined for type constructors on Prop (@Leonardo de Moura ?)

It'd be nice to be able to use do notation on my structure.

Drop in replacement:

namespace Hidden

class Bind (m : Sort u → Type v) where
  bind : {α β : Sort u} → m α → (α → m β) → m β

class Pure (f : Sort u → Type v) where
  pure {α : Sort u} : α → f α

class Functor (f : Sort u → Type v) : Type (max (u+1) v) where
  map      : {α β : Sort u} → (α → β) → f α → f β
  mapConst : {α β : Sort u} → α → f β → f α := Function.comp map (Function.const _)

class Seq (f : Sort u → Type v) : Type (max (u+1) v) where
  seq  : {α β : Sort u} → f (α → β) → (Unit → f α) → f β

class SeqLeft (f : Sort u → Type v) : Type (max (u+1) v) where
  seqLeft : {α β : Sort u} → f α → (Unit → f β) → f α

class SeqRight (f : Sort u → Type v) : Type (max (u+1) v) where
  seqRight : {α β : Sort u} → f α → (Unit → f β) → f β

class Applicative (f : Sort u → Type v) extends Functor f, Pure f, Seq f, SeqLeft f, SeqRight f where
  map      := fun x y => Seq.seq (Pure.pure x) fun _ => y
  seqLeft  := fun a b => Seq.seq (Functor.map (Function.const _) a) b
  seqRight := fun a b => Seq.seq (Functor.map (Function.const _ id) a) b

class Monad (m : Sort u → Type v) extends Applicative m, Bind m : Type (max (u+1) v) where
  map      {α β} f x := Bind.bind x (fun a => Pure.pure (f a))
  seq      {α β} f x := Bind.bind f fun y => Functor.map y (x ())
  seqLeft  {α β} x y := Bind.bind x fun a => Bind.bind (y ()) (fun _ => Pure.pure a)
  seqRight {α β} x y := Bind.bind x fun _ => y ()

[Mario Carneiro]

I don't see an issue with this generalization on its own, although I have significant doubts about its usefulness

[Leonardo de Moura]

@James Gallicchio

So now I'm wondering why Monad in the prelude isn't defined for type constructors on Prop (@Leonardo de Moura ?

As Mario pointed out, it didn't look very useful. BTW, I don't have time to investigate the impact of this change right now.

[Mario Carneiro]

To elaborate more on why it isn't very useful: a monad with type Prop -> Type can only be used to bind propositions. You almost certainly want to be able to bind both propositions and regular types in a do block, but this generalization won't give you that

[Mario Carneiro]

the usual trick I use to bind propositions in a do block uses pattern matching and PLift:

import Lean
open Lean

def checkPos (n : Nat) : MetaM (PLift (0 < n)) :=
  if h : 0 < n then pure ⟨h⟩ else failure

def usesProp : MetaM {n // 0 < n} := do
  let n ← pure 37
  let ⟨h⟩ ← checkPos n
  pure ⟨n, h⟩

[James Gallicchio]

Ahh, I see