understanding implementing instances of Monad

Stream: new members

[JJ]

Hi! I'm fairly new to the Haskell tradition of functional programming (my background is in Scheme and Rust) and am learning about monads and monad transformers for a parser combinator library I am porting over to Lean.

What is the issue with the following code? I am trying to declare that my custom Parser.Result type (equivalent to Except ε (σ × α)) is a monad. I know that Except ε (σ × α) is a monad, and I think I've defined pure and bind correctly wrt. it (though the utility of pure is not quite clear to me, and I may later want to not treat it as a monad...)

inductive Parser.Result σ α ε where
| success (val : α) (rest : σ)
| failure (msg : ε)

def Parser.Result.pure (input: σ) (val : α) : Parser.Result σ α ε :=
  .success val input

def Parser.Result.bind : Parser.Result σ α ε -> (σ -> α -> Parser.Result σ β ε) -> Parser.Result σ β ε
| .success val rest, f => f rest val
| .failure msg, _ => .failure msg

instance Parser.Result.Monad : Monad (Parser.Result σ α ε) where
  pure := Parser.Result.pure
  bind := Parser.Result.bind

The error message I am getting is the following.

Application type mismatch: The argument
  Result σ α ε
has type
  Sort (max (max (max 1 ?u.1599) ?u.1598) ?u.1597)
but is expected to have type
  Type ?u.1596 → Type ?u.1595
in the application
  Monad (Result σ α ε)Lean 4

I think what this is telling me is I need to let Parser.Result σ α ε be a function, so like... σ -> α -> Parser.Result σ α ε. But I'm not quite sure how to reconcile that with σ α being the first two arguments to Parser.Result, and being two arguments instead of one. Does anyone have some tips here?

[Aaron Liu]

It's because Parser.Result is too universe general

[Robin Arnez]

I don't think Except ε (σ × α) is a monad, rather σ → Except ε (σ × α) is a monad. Why is Except ε (σ × α) not a monad? Well remember how do notation works: When you have x : m α for a monad m, you can use let a : α ← x to perform the monadic action and get the result of type α. There's no place for σ here! With σ → Except ε (σ × α) though you can pass the state of type σ to the continuation. Also, regarding the actual error message you got: a monad is not just a type but rather a function from a type α to a type m α of monadic actions returning α (not Sort ... but Type _ → Type _). So you'd need to wrap it into a lambda, or really make the α parameter the last in your type definition and simply omit it. Here's your original code updated:

inductive Parser.Result (σ ε α : Type) where
  | success (val : α) (rest : σ)
  | failure (msg : ε)

def ParserM (σ ε α : Type) : Type := σ → Parser.Result σ ε α

@[inline]
def ParserM.pure (val : α) : ParserM σ ε α :=
  fun input => .success val input

@[inline]
def ParserM.bind (x : ParserM σ ε α) (f : α → ParserM σ ε β) : ParserM σ ε β :=
  fun state =>
    match x state with
    | .success val rest => f val rest
    | .failure msg => .failure msg

instance : Monad (ParserM σ ε) where
  pure := ParserM.pure
  bind := ParserM.bind

As you can see, instead of using Parser.Result directly, we wrap it in a function type in ParserM. Also, the parameter order of Parser.Result and ParserM is adjusted so that α comes last. Then we can define ParserM.pure as the stateful function that simply returns val and ParserM.bind as the stateful function that first runs x and then f with the result of x and finally define the monad instance for m := ParserM σ ε where a monadic action returning α is m α = ParserM σ ε α = σ → Parser.Result σ ε α.

[JJ]

Thanks! I'll chew on this. As it turns out, this σ → Parser.Result σ ε α type is exactly what I've called Parser later on. I was thinking both it and Parser.Result would form a monad, but I guess it makes sense that only Parser does.

[JJ]

That does explain why Except is Except ε α, too, rather than the Result[α, ε] I've come to expect from Rust and the like.

[Matt Diamond]

note that your original signature for bind doesn't really make sense... it should have the overall form m a → (a → m b) → m b, but your version has two arguments in the function parameter