ite return type

Stream: new members

[Vaibhav Karve]

I accidentally discovered that the type of a function can be an if ... then ... else ... expression. Is there some reason why we don't use this all the time? To me it looks like this ite return type (as seen in f₁) is more expressive than a function of type ℕ → ℕ ⊕ ℤ (as show in f₂).

def f₁ (n : ℕ) : ite (n=0) ℕ ℤ :=
begin
  split_ifs,
  exact 4,
  exact -3,
end

def f₂ : ℕ → (ℕ ⊕ ℤ)
| 0 := sum.inl 4
| _ := sum.inr (-3)

[Anne Baanen]

It is more expressive, but quickly it becomes more annoying to work with because you have to carry around proofs everywhere. For example, you can try defining f₂ : ℕ -> ℤ as f₂ n = f₁ (n + 1).

[Anne Baanen]

I still have hope that one day there will be a smart enough system that ite (n = 0) ℕ ℤ is a useful type, but Lean isn't it yet.

[Mario Carneiro]

This is basically a dependent type, like vector A n

[Mario Carneiro]

they have the danger that you can't rewrite in the dependent argument

[Mario Carneiro]

It's not really "more expressive" as long as the function body itself is "white boxed" (as definitions are in lean unless they are [irreducible]). Note that you can define f_1 using f_2 by cases

[Mario Carneiro]

i.e. you can prove that f_2 has the same behavior as f_1

[Vaibhav Karve]

Thanks to both of you. Your answers have given me more to thing about :+1: