bottom type (⊥)

Stream: Is there code for X?

[Robert Osazuwa Ness]

Is there a bottom type ⊥ in Lean4?

For example, in Haskell you might write:
f:: Bool -> Bool f = undefined
and that works because "undefined" evaluates to bottom, which is a member of Bool and any type.
But in lean I tried
def f (α : Bool) : Bool := none
and got a type mismatch. So I guess "none" isn't it.

[Yaël Dillies]

Do you mean False?

[Yaël Dillies]

Or maybe you're looking for ⊥ (docs#has_bot in mathlib)

[Mario Carneiro]

No, there is no bottom value in the haskell sense. Indeed if there was you could use it to prove any proposition and hence trivialize the logical content of the theory

[Mario Carneiro]

(nit: undefined is a bottom value inhabiting every type, not a bottom type. As Yael says, a bottom type is one with no elements and lean has False for the bottom type in the universe of propositions and Empty for the bottom type in Type.)

[Robert Osazuwa Ness]

So Lean must then have some mechanism prohibiting non-terminating expressions? What is that? Sorry, I think I read about this somewhere but can't recall where, I'm coming back to learning Lean a brief pause.

[Mario Carneiro]

All recursive functions have to decrease along some well founded metric

[Mario Carneiro]

in many cases lean can infer an appropriate relation on its own but if it fails you can use the termination_by clause to supply your own

[Mario Carneiro]

in particular def foo : p := foo is not accepted

[Calvin Lee]

err
lean has sorry which functions almost exactly the same as undefined in haskell. It is an axiom which can inhabit any value, and you use it when you can't prove something yet.
but it should never be used in proofs or code that exists (and in fact you can figure this out by checking if the definition depends on sorryAx)

[Calvin Lee]

I suppose sorry is an answer to any thread in this channel
but I think it deserves special mention as a potential "bottom value"

[Mario Carneiro]

that's true, but sorry has special handling and lean will give you grief if you use it

[Mario Carneiro]

you can also make your own axioms and use them to prove false things if you want. Lean won't even complain in that case