How to better compose/pipeline monads

Stream: lean4

[Nicolas Rouquette]

Background:

I am writing a Lean4 DSL for my modeling language, the Ontological Modeling Language, which I would like to define as a subset of the OWL2-DL description logic: https://github.com/opencaesar/oml

Unlike a programming language DSL where it would be sensible to embed the DSL as Lean expressions, this is a different kind of DSL problem in that the semantics of the language is a kind of logic, not executable program. So, what matters here is computing logical consistency, entailments, subsumption, ...

I have made baby steps using a monadic style -- thanks so much for the books/doc in progress; it's been hugely helpful!

My problem:

I have several monads that I wrote to resolve OML syntax into an intermediate representations (logical axioms).
For details, see: https://github.com/NicolasRouquette/oml.lean4

I have these definitions of context (input OML syntax) & state (logical axioms)

abbrev MCore := EStateM Exception State
abbrev M     := ReaderT Context MCore

In https://github.com/NicolasRouquette/oml.lean4/blob/master/src/Oml/Resolver.lean, there are a few toplevel resolvers to analyze the input OML syntax from the context and update the state of logical axioms:

def validateVocabularyDeclarations: M State := do
  (← read).vocabularies.foldlM validateVocabularyDeclaration (← get)

def validateVocabularyStatementDeclarations: M State := do
  (← read).vocabularies.foldlM validateStatementDeclarationsIn (← get)

def validateVocabularySpecializations: M State := do
  (← read).vocabularies.foldlM validateVocabularySpecializationsIn (← get)

I wrote tests to exercise these resolver monads in https://github.com/NicolasRouquette/oml.lean4/blob/master/src/Oml/testResolver.lean

def c1 : Context := { vocabularies := [testSyntax.rdfs, testSyntax.xsd, testSyntax.base, testSyntax.mission ] }
def s0 : State := {}

def r1a : EStateM.Result Exception State State := validateVocabularyDeclarations |>.run c1 |>.run s0

Next, I need to get the result of the above and run validateVocabularyStatementDeclarations.

This is where things get a wee bit ugly:

One way is to extract the result, assuming it is OK and run the next resolver.

def s1 : State := match r1a with | EStateM.Result.ok s _ => s | _ => {}
def r1b : EStateM.Result Exception State State := validateVocabularyStatementDeclarations |>.run c1 |>.run s1

def s2 : State := match r1b with | EStateM.Result.ok s _ => s | _ => {}
def r1c : EStateM.Result Exception State State := validateVocabularySpecializations |>.run c1 |>.run s2

Surely, there must be better way to compose these monads; though it is unclear to me how to do this.

I managed to two monads successfully, e.g.:

def validateVocabularyStatementDeclarations': M State := do
  let c: Context ← read
  validateVocabularyDeclarations >>= (fun s => c.vocabularies.foldlM validateStatementDeclarationsIn s)

This allows me to write instead:

def r1b' : EStateM.Result Exception State State := validateVocabularyStatementDeclarations' |>.run c1 |>.run s0

But this does not to work for composing 3 monads:

def validateVocabularySpecializations': M State := do
  let c: Context ← read
  validateVocabularyDeclarations
  >>= (fun s => c.vocabularies.foldlM validateStatementDeclarationsIn s)
  >>= (fun s => c.vocabularies.foldlM validateVocabularySpecializationsIn s)

It seems that it is running the 1st and 3rd, skipping the 2nd.

What would be a better way to write this?

[Mario Carneiro]

Unlike a programming language DSL where it would be sensible to embed the DSL as Lean expressions, this is a different kind of DSL problem in that the semantics of the language is a kind of logic, not executable program. So, what matters here is computing logical consistency, entailments, subsumption, ...

Just regarding this point: it doesn't really matter what your DSL represents, since it's basically going to facilitate turning expressions into syntax that you can do whatever with. There isn't any special attention paid to syntax that represents executable programs when we are talking about a custom DSL - it all just turns into an AST

[Mario Carneiro]

As a terminological point, you aren't composing monads, you are composing monadic operations (using bind). Composing monads is stuff like ReaderT r (StateT s (Except e m))

[Mario Carneiro]

The usual way to write your example is:

def validateVocabularySpecializations': M State := do
  let c: Context ← read
  let mut s <- validateVocabularyDeclarations
  for x in c.vocabularies do
    s <- validateStatementDeclarationsIn s x
  for x in c.vocabularies do
    s <- validateVocabularySpecializationsIn s x
  pure s

(I think - untested since there is no #mwe)

[Mario Carneiro]

But this is a bit fishy, because you have State appearing twice: it is in the monad M (which wraps MCore which wraps a state monad over State) and it is also the return value of the function. This is most likely where the missing state is going

[Mario Carneiro]

If you want the state to be part of the monad, then you shouldn't be returning M State, it should be M Unit and you don't need to get s all the time

def validateVocabularySpecializations': M Unit := do
  validateVocabularyDeclarations
  for x in c.vocabularies do
    validateStatementDeclarationsIn x
  for x in c.vocabularies do
    validateVocabularySpecializationsIn x

[Nicolas Rouquette]

Thanks for the terminology correction and the suggestions, which worked very well.

def validateVocabularySpecializations': M Unit := do
  let c: Context ← read
  validateVocabularyDeclarations
  for v in c.vocabularies do
    validateStatementDeclarationsIn v
  for v in c.vocabularies do
    validateVocabularySpecializationsIn v

Applying your suggestion to other functions, e.g.:

def validateVocabularyDeclarations: M Unit := do
  for x in (← read).vocabularies do
    validateVocabularyDeclaration x

I can further simplify it to just:

def validateVocabularySpecializations'': M Unit := do
  validateVocabularyDeclarations
  validateVocabularyStatementDeclarations
  validateVocabularySpecializations

This is really nice!

For testing purposes, I am wondering what is the proper way to extract the monad's state outside of ado?

With the above, I get nothing:

def r1c'': EStateM.Result Exception State Unit := validateVocabularySpecializations'' |>.run c1 |>.run s0
#eval r1c''

I know that I can write a simple accessor like this so that I can check the resulting state:

def resolverGet: M State := do
  pure (← get)

def validateVocabularySpecializations''Get: M State := do
  validateVocabularySpecializations''
  resolverGet

def r1c2 : EStateM.Result Exception State State := validateVocabularySpecializations''Get |>.run c1 |>.run s0
#eval r1c2

Is there a way to write the equivalent of validateVocabularySpecializations''Getwithout defining resolverGet?

[Mario Carneiro]

I'm not sure what you mean by "I get nothing" there

[Mario Carneiro]

That result object should contain the final state; you can pattern match on it to get at it

[Nicolas Rouquette]

Oh right! I was a bit confused with the output:

def r1c'': EStateM.Result Exception State Unit := validateVocabularySpecializations'' |>.run c1 |>.run s0
#eval r1c''
-- EStateM.Result.ok ()

Indeed, with pattern matching I can extract the state from the result:

def s1c'' : State := match r1c'' with | EStateM.Result.ok _ s => s | _ => {}
#eval s1c''
-- { .... }

Thanks!