Bypass proof

Stream: lean4

[eduardo]

Is by sorry the semantic way to bypass proofs when creating instances from types that require proofs in unsafe functions?

[Henrik Böving]

We usually use lcProof for this type of stuff in the core language. Of course I would generally advise against doing this and instead trying to find a way around it, can you maybe detail what you are dong and why you need a proof?

[eduardo]

I'm trying to use lean4 for now as a general-purpose functional language, so I'm encoding refinement types using evidence. There are some cases where I just want to say to the compiler, "It's ok. Even coming from the runtime, these values are correct; if not, you can just explode the program ." SerDes is a good example of that.

[Markus Schmaus]

An alternative design could be similar to docs#List.head!:

structure NonEmptyString where
  value : String
  ev : value.length > 0 := by decide
deriving Repr

instance : Inhabited NonEmptyString := ⟨{value := "_"}⟩

def NonEmptyString.mk! (value : String) : NonEmptyString :=
  if ev : value.length > 0 then
    ⟨value, ev⟩
  else
    panic "empty string"

#eval NonEmptyString.mk! "a"

docs#panic prints an error message and then continues the program with the default value provided by the Inhabited instance.

[James Gallicchio]

+1 to relying on panic in these situations, but having to insert these ifs is not super ergonomic. If you do it anyways, it might be a good case study for how we can improve this via metaprogramming :big_smile:

[eduardo]

Do we have alternatives to stopping the execution, like error in Haskell or throw in Scala? It's not yet clear to me whether the separation (if it exists) between errors and defects in Lean exists outside of the IO monad.

[eduardo]

James Gallicchio said:

+1 to relying on panic in these situations, but having to insert these ifs is not super ergonomic. If you do it anyways, it might be a good case study for how we can improve this via metaprogramming :big_smile:

I would love to achieve that, but I think it's a long way until reach there. :smile:

[Eric Wieser]

eduardo said:

Do we have alternatives to stopping the execution, like error in Haskell or throw in Scala? It's not yet clear to me whether the separation (if it exists) between errors and defects in Lean exists outside of the IO monad.

You can throw from docs#Except

[eduardo]

Hmm, based on the docs, it seems we don't have a definition of defects for pure code because of logic consistency. This seems weird in general-purpose languages but is necessary for the theorems. I'm sure it leads to safer code and a paradigm shift since the constraints to achieve ergonomics are different. Cool! :smiley: .
Thank you, folks!

[Eric Wieser]

One thing to remember is that lean has very powerful do notation, so working in Except everywhere is surprisingly pleasant