Monads and Dependent Types

Stream: lean4

[Marcus Rossel]

I'm running into a pattern when using monads that I can't seem to resolve properly (it's not Lean specific).
I have something that's basically a specific state monad:

structure Context where
  x : Nat
  min : Nat

def Mon (α : Type) := Context → (Context × α)

I then want to write a function to set the value x. There should be a restriction though that it should only be possible to provide a value that is greater or equal to the bound min. With Mon I don't see how to enforce the restriction:

-- I would like to restrict x to be ≥ `min` of the context.
def Mon.setX (x : Nat) : Mon Unit :=
  fun ctx => ({ ctx with x := x }, ())

My current approach is to push min into the type of Context and Mon:

structure Context' (min : Nat) where
  x : Nat

def Mon' (min : Nat) (α : Type) := (Context' min) → (Context' min × α)

def Mon'.setX {min : Nat} (x : Nat) (_ : x ≥ min) : Mon' min Unit :=
  fun ctx => ({ ctx with x := x }, ())

The problem I have with this approach is that as I add more restrictions, I need to add more and more values into the type of Mon.
Is there an established solution to this kind of problem?

[Henrik Böving]

Why aren't you defining

structure Context where
  min : Nat
  x : Nat
  h : min <= x

?

[Marcus Rossel]

Henrik Böving said:

Why aren't you defining

structure Context where
  min : Nat
  x : Nat
  h : min <= x

?

Because it was just an example. My real use case is a bit different.

[Henrik Böving]

Well in general I would always try to keep the invariants packed with the values in some way, this can be by storing them or by defining some notion of well formedness like e.g. HashMap https://github.com/leanprover/lean4/blob/0925051c51e183a0b8c504ae53f5cab0525d6cac/src/Std/Data/HashMap.lean#L127-L128

and if that isn't enough this is #xy

[Chris Lovett]

PS: it looks like this Std folder was just renamed to Bootstrap https://github.com/lovettchris/lean4/blob/master/src/Bootstrap/Data/HashMap.lean which means any import Std.Data.HashMap will have to be replaced with import Bootstrap.Data.HashMap...

[Mario Carneiro]

Std is still under construction but hopefully in a few days import Std.Data.HashMap will work again

[Mario Carneiro]

import Bootstrap.Data.HashMap will also be outdated advice once lean4#1541 lands, it is moving to import Lean.Data.HashMap

[Marcus Rossel]

Henrik Böving said:

Well in general I would always try to keep the invariants packed with the values in some way, this can be by storing them or by defining some notion of well formedness like e.g. HashMap https://github.com/leanprover/lean4/blob/0925051c51e183a0b8c504ae53f5cab0525d6cac/src/Std/Data/HashMap.lean#L127-L128

and if that isn't enough this is #xy

I don't see how this solves the problem. If I add h : x ≥ min to Context, then how do I implement setX?

structure Context where
  x : Nat
  min : Nat
  h : x ≥ min

def Mon (α : Type) := Context → (Context × α)

def Mon.setX (x : Nat) : Mon Unit :=
  fun ctx => ({ ctx with x := x, h := ??? }, ()) -- How do I make sure x ≥ ctx.min?

[Henrik Böving]

It doesn't, I'd suggest to use a state monad as well as well as its modify function that accesses the state for stuff like this,that is of course a slightly different API than you are used to but in the end you need to expose details about your Context to the caller of setX if you want them to prove the invariant

[Andrés Goens]

I'm not entirely sure I understand your problem about adding things to Mon The way you are doing it already, adding more restrictions actually adds more values to the type of setX. I guess the point of having the invariants within the structure as @Henrik Böving suggests is that you push that to whoever constructs the term of that type (Context in this case). In your case @Marcus Rossel you could even do a third option and leverage the fact that it's a nat that keeps increasing and just take what's been added as a parameter and not the new value (which is specific to your case here, but since I know the use-case, I know that it's also how they do it in the other languages btw)

structure Context where
  x : Nat
  min : Nat
  h : x ≥ min

-- if you use `def` instead of `abbrev` you don't get the instances inferred
abbrev Mon := StateM Context

-- trivial (just using modify)
def Mon.setX' (ctx : Context) : Mon Unit := modify λ _ => ctx

-- might be a noop
def Mon.setX (x : Nat) : Mon Unit := do
  let ctx ← get
  if h : x ≥ ctx.min then
    set { ctx with x := x, h := h}
  -- you could also
  -- else
  --   panic! "invalid x"

def Mon.setXplus (plusX : Nat) : Mon Unit := do
  let ctx ← get
  let x' := plusX + ctx.x
  let h' : x' ≥ ctx.min := by
    apply Nat.le_trans ctx.h
    apply Nat.le_add_left ctx.x plusX
  set { x := x', h := h', min := ctx.min : Context }