Idiomatic way to unwrap options/results

Stream: general

[Greg Shuflin]

Is there a general idiomatic way to take an Option or Result value, and extract the inner value or crash? Something like the rust unwrap function?

[Ayhon]

I guess you could do

let some value := optionalValue | panic "error"

But this only works with do notation. So you would need a Id.run or similar.

If the monad you're working under impements Alternative though, you could do

let some value := optionalValue | failure

I learned of this syntax not too long ago, doing Advent of Code, and I'm not yet sure if it's idiomatic. But it's definitely concise

[Markus Himmel]

You can use docs#Option.get!.

[Greg Shuflin]

Markus Himmel said:

You can use docs#Option.get!.

looks like this only works if the type is Inhabited, and it just returns a default if the option is none.

[Greg Shuflin]

Indeed it looks like https://leanprover-community.github.io/mathlib4_docs/Init/Data/Option/BasicAux.html#Option.get! has different semantics than other get! functions defined on other types

[Ayhon]

Greg Shuflin said:

looks like this only works if the type is Inhabited, and it just returns a default if the option is none.

It think this restriction comes from the fact that panic requires Inhabitted, not that it returns a default value. That would be more getD

[Markus Himmel]

I don't think it's different from the get! functions on other types. In Lean, a panic does not actually terminate the program unless a specific command line argument is given, see docs#panic. Since Lean is a total language, even a panic has to produce a value of the expected type (even if it is never executed), otherwise Lean's type system would be unsound. For this reason, panic requires the type to be inhabited and returns the default value of the type.

[Greg Shuflin]

Markus Himmel said:

I don't think it's different from the get! functions on other types. In Lean, a panic does not actually terminate the program unless a specific command line argument is given, see docs#panic. Since Lean is a total language, even a panic has to produce a value of the expected type (even if it is never executed), otherwise Lean's type system would be unsound. For this reason, panic requires the type to be inhabited and returns the default value of the type.

So, is there a reasonable way to create an Inhabited variant of random custom types, purely for the purpose of making panic-causing unwraps work?

[Daniel Weber]

You can try deriving Inhabited, e.g.

structure Test where
  value : Nat
deriving Inhabited