Structures in TPIL

Stream: general

[Heather Macbeth]

In #tpil, chapter 4 it is stated,

a non-recursive inductive type that contains only one constructor is called a structure

@Rob Lewis and I were just discussing the following example, which is a non-recursive inductive type with one constructor; we couldn't figure out how to express it as a structure. Is there a missing hypothesis in the TPIL statement?

variable (α β : Type) (f : β → α → α)

inductive Foo : α → α → Prop
  | bar (b : β) (a : α) : Foo a (f b a)

[Kyle Miller]

"without indices"

[Kyle Miller]

That's if you mean "structure" as "able to be expressed with the structure command". These are confusingly different concepts! (Issue lean4#5891 tracks trying to get the terminology to be less confusing.)

[Kyle Miller]

In the next release, the structure command can create recursive inductive types, but it still can't define any that have indices. Also, in general you will be able to use numeric projection notation for any one-constructor inductive type (so long as it's logically valid to do so). It won't work with Foo since it's Prop-valued, but if it were Type-valued then given f : Foo you would be able to do f.1 and f.2.

[Heather Macbeth]

Oh! I didn't realize there was another meaning of "structure". Yes, I meant "able to be expressed with the structure command".

Should this be considered a typo in TPIL? Should I open an issue?

[Kyle Miller]

There's a notion of a "structure-like", which is a one-constructor non-recursive inductive type with no indices (even if it was defined using inductive). These have an eta rule in the kernel.

Then there's the notion of "structures", which may or may not be structure-likes. These will always be one-constructor inductive types with no indices, recursive or non-recursive. Until this week, they were always non-recursive. These have special elaborator support for { ... } notation and automatically-created named projection functions.

Lastly, there's there's the unnamed notion of inductive types with one constructor. These allow numeric projection notation. (For the kernel enthusiasts, the kernel allows primitive projections to be used on these.)

[Kyle Miller]

Heather Macbeth said:

Should I open an issue?

Yeah, I think that would be good