## Stream: new members

### Topic: ite return type

#### Vaibhav Karve (Oct 16 2020 at 16:17):

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 (Oct 16 2020 at 16:41):

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 (Oct 16 2020 at 16:44):

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 (Oct 16 2020 at 17:04):

This is basically a dependent type, like vector A n

#### Mario Carneiro (Oct 16 2020 at 17:04):

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

#### Mario Carneiro (Oct 16 2020 at 17:06):

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 (Oct 16 2020 at 17:07):

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