Zulip Chat Archive

Stream: Type theory

Topic: The `{}` annotation for inductive types


view this post on Zulip Gihan Marasingha (Dec 20 2020 at 15:26):

Can someone give a simple example to show where the {} annotation for constructors of inductive types is necessary? For instance, what works with

inductive sum (α : Type u) (β : Type v)
| inl {} : α  sum
| inr {} : β  sum

that doesn't work for

inductive sum' (α : Type u) (β : Type v)
| inl : α  sum'
| inr : β  sum'

?

view this post on Zulip Kenny Lau (Dec 20 2020 at 15:40):

implicit arguments

view this post on Zulip Kevin Buzzard (Dec 20 2020 at 15:42):

#tpil explains an example here.

...erm, except that indeed the {} (in list.nil) seems to have no effect in their example either.

universes u

namespace hidden

inductive list (α : Type u)
| nil {} : list
| cons : α  list  list

inductive list' (α : Type u)
| nil : list' -- get {} brackets
| cons : α  list'  list'


inductive list'' (α : Type*)
| nil [] : list'' -- get () brackets :D
| cons : α  list''  list''

view this post on Zulip Kevin Buzzard (Dec 20 2020 at 15:45):

I think some change was made in core Lean relatively recently and perhaps TPIL was not updated.

view this post on Zulip Gihan Marasingha (Dec 20 2020 at 16:11):

Right, that's what I thought. The [] annotation does make a difference, but just removing {} doesn't seem to do anything. Should the definitions in mathlib be updated to remove the {} annotation?

Unless there really is a difference and I just don't understand what it is.

view this post on Zulip Kevin Buzzard (Dec 20 2020 at 16:18):

universes u v

namespace hidden

inductive sum1 (α : Type u) (β : Type v)
| inl {} : α  sum1
| inr {} : β  sum1

inductive sum2 (α : Type u) (β : Type v)
| inl : α  sum2
| inr : β  sum2

#print prefix hidden.sum1
#print prefix hidden.sum2

end hidden

Make the infoview big and move your cursor between the two #print statements to see...no change at all other than 1<->2

view this post on Zulip Gihan Marasingha (Dec 20 2020 at 16:22):

Yes and ignore my previous comment. I see that the constructors for sum and list don't take the {} annotation in core Lean.

view this post on Zulip Gihan Marasingha (Dec 20 2020 at 16:26):

@Jeremy Avigad can you confirm that the {} annotation for constructors of implicit types doesn't do anything in the current version of Lean? Does tpil need to be updated?

view this post on Zulip Kevin Buzzard (Dec 20 2020 at 16:27):

so one can use git blame to find out when that changed, and one is led here.

view this post on Zulip Kevin Buzzard (Dec 20 2020 at 16:32):

Looking at the diff, you see that it was clearly the right decision.

view this post on Zulip Jeremy Avigad (Dec 22 2020 at 17:47):

Sorry, I have been dragging my feet on this. The semester is over now, and my grades are in. Within the next day or two I'll update TPIL to compile with the latest version of mathlib, and I'll update this in the text.

view this post on Zulip Jeremy Avigad (Dec 23 2020 at 02:20):

I just updated TPIL to Lean 3.23.0, removed the discussion of {}, and merged a number of pull requests I had been neglecting. @Gihan Marasingha thanks for pinging me on this.


Last updated: May 08 2021 at 23:10 UTC