Option.toExcept or similar

Stream: lean4

[Jannis]

Hi,
I was wondering whether there was a way of getting around the following match pattern, which looks a bit redundant:

import Std.Data.HashMap.Basic

def lookup₁ (table: Std.HashMap String (Std.HashMap String Int)) : Except String Int := do
  let x <- match table["x"]? with
    | none => throw "x not in table"
    | some assignment => pure assignment
  let y <- match x["y"]? with
    | none => throw "y not in x"
    | some assignment => pure assignment
  return y

I came up with the following definition:

def Option.toExcept [Monad m] [MonadExcept ε m] : Option α -> ε -> m α
| none,     err => throw err
| some val, _   => pure val

This then lets me do the following:

def lookup₂ (table: Std.HashMap String (Std.HashMap String Int)) : Except String Int := do
  let x <- table["x"]?.toExcept "x not in table"
  let y <- x["y"]?.toExcept "y not in x"
  return y

Coming from other programming languages, I would expect Option to have a similar method already, but I couldn't find it.
If it doesn't exist, are there any reasons Option shouldn't be used in that way?
I'm kinda new to Monads, so maybe my usage isn't idiomatic.

[Eric Paul]

Here are two builtin approaches to doing this:

import Std.Data.HashMap.Basic

def lookup₁ (table: Std.HashMap String (Std.HashMap String Int)) : Except String Int := do
  let x <- table["x"]?.getDM (throw "x not in table")
  let y <- x["y"]?.getDM (throw "y not in x")
  return y

import Std.Data.HashMap.Basic

def lookup₁ (table: Std.HashMap String (Std.HashMap String Int)) : Except String Int := do
  let .some x := table["x"]?
    | throw "x not in table"
  let .some y := x["y"]?
    | throw "y not in x"
  return y

[Jovan Gerbscheid]

(Note that you don't need the . in .some)

import Std.Data.HashMap.Basic

def lookup₁ (table: Std.HashMap String (Std.HashMap String Int)) : Except String Int := do
  let some x := table["x"]?
    | throw "x not in table"
  let some y := x["y"]?
    | throw "y not in x"
  return y