Applying post invariant to Hoare State Monad

Stream: lean4

[Gary Haussmann]

I'm working through "The Hoare State Monad" by Wouter Swierstra and have written up a Lean version:

-- Hoare logic pre and post invariants
def Pre (s : Type) : Type := s → Prop
def Post (s α : Type) : Type := s → α → s → Prop

-- Hoare Logic State monad returns a (s × α × post) structure
structure HLOut (s α : Type) (postCondition : Post s α) (stateIn : s) where
  (stateOut : s) (retVal : α) (postInvariant : postCondition stateIn retVal stateOut)

-- state monad with pre/post invariants
def HLStateM (s : Type) (pre : Pre s) (α : Type) (post : Post s α) : Type :=
  (s₁ : s) → (p : pre s₁) → HLOut s α post s₁

I'd like to move the monad result type α to the end of the HLStateM type so that I can make Functor and Monad instances:

def HLStateM (s : Type) (pre : Pre s) (post : Post s α) (α : Type) : Type :=
  (s₁ : s) → (p : pre s₁) → HLOut s α post s₁

However, this is a problem since now the post invariant Post s α shows up in the declaration earlier thanα upon which it depends . In fact I think Lean makes a second α instance specifically for Post s α. Of course the two α don't match so that's a no-go.

The natural solution is to remove the α from Post s α so that it only depends on the state s but then I lose the ability to apply the invariant to the monad result α. I'm not well-versed in dependent type programming so I thought to check here to see if there are any alternatives or useful tricks I could use here.

[Simon Hudon]

I think you should swap the two declarations (α : Type) (post : Post s α). It's annoying if you want (α : Type) to be the last declaration because it's the output type of the monad but you can think of the output to be the pair (α, post). You could encode that in the types by combining α and post into post : { α : Type // Post s α } but I would be careful going down that road because you risk intertwining the proof and the program definition.

[Gary Haussmann]

I know I can always just use raw bind or (>>=) but I would sad to lose do notation. I could just embed the postcondition into the output type HLOut but that might make it difficult to infer types/proofs?

[Simon Hudon]

I don't think you can fit the Hoare state monad into Haskell-style monads. The good news is that the notation system in Lean 4 is very flexible and you can make adapted notation for your monads.