Zulip Chat Archive

Stream: new members

Topic: ite return type


view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 16 2020 at 17:04):

This is basically a dependent type, like vector A n

view this post on Zulip Mario Carneiro (Oct 16 2020 at 17:04):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 16 2020 at 17:07):

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

view this post on Zulip Vaibhav Karve (Oct 18 2020 at 18:21):

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


Last updated: May 14 2021 at 23:14 UTC