# Zulip Chat Archive

## Stream: general

### Topic: Inductive constructions

#### Patrick Johnson (Jan 15 2022 at 15:47):

Is it true that only a small number of inductive types is enough to implement all other inductive types? I was playing with this idea, and I managed to use only `false`

, `nat`

and `psigma`

to re-implement all inductive types and props from `core.lean`

. Is there a type that can't be implemented using those three types? If there's no such type, why do we have inductive constructions as a part of the kernel?

#### Yaël Dillies (Jan 15 2022 at 15:49):

Set theory would tell you that docs#pSet is enough to reimplement everything. :wink:

#### Chris B (Jan 15 2022 at 16:57):

The part of the kernel that handles inductives implements general rules for checking inductives and constructing recursors. If you're willing to trust them (and the theory) to handle `false`

, `nat`

, and `psigma`

, it seems like you've already bought and paid for the underlying theory, so you might as well use it. The post-mortem on e.g. Lean 3's mutual inductives seems to suggest that the "implement complex constructions as machine-generated compositions of simpler elements" is not without tradeoffs. Inductive types are pretty central to the user experience in Lean; in terms of getting actionable feedback and communicating with users and stuff, I would assume a direct implementation is much better.

#### Reid Barton (Jan 15 2022 at 17:06):

How did you make `eq`

?

#### Patrick Johnson (Jan 15 2022 at 18:30):

Set theory would tell you that docs#pSet is enough to reimplement everything.

Maybe I don't understand the Lean type theory enough, but as far as I can tell, you can't implement `nat`

using only `pSet`

without any other inductive types. Being able to inductively construct an infinite type (such as `nat`

) using Lean inductive constructions basically implies the ZFC axiom of infinity.

Inductive types are pretty central to the user experience in Lean; in terms of getting actionable feedback and communicating with users and stuff, I would assume a direct implementation is much better.

Of course. But I'm not talking about the user interface at all. When you define an inductive type, all that you get back from the kernel are some constants and their types. The meta level code then proves other things, noconfusion, induction, dcases, and similar lemmas. My point is that we can only have a small number of builtin constants and define everything other in terms of that. User would not see any difference (except that a recursor of a type will actually have a concrete definition).

How did you make eq?

Here is my definition:

```
def eq {α} (x y : α) := ∀ (P : α → Prop), iff (P x) (P y)
```

Here are other definitions (there may be some mistake, I haven't formally proved they are equivalent to the actual definitions from `core.lean`

):

Definitions

#### Mario Carneiro (Jan 15 2022 at 18:35):

This is covered in #leantt, chapter 5.

#### Mario Carneiro (Jan 15 2022 at 18:36):

Specifically, you need 8 inductive types:

`false`

`psigma`

`psum`

`ulift`

`nonempty`

`W_type`

(docs#W_type)`eq`

`acc`

(docs#acc)

#### Mario Carneiro (Jan 15 2022 at 18:38):

The main one is `W_type`

, but then you need all the others to actually put stuff together into the form needed by `W_type`

#### Mario Carneiro (Jan 15 2022 at 18:45):

Regarding your constructions:

- The
`true`

construction works as a type that is bijective with`true`

, but it doesn't have all the right defeqs. The W-type reduction includes all the same defeqs as a genuine inductive type. - Same thing for
`and`

and`or`

, and in particular those constructions are not intuitionistic, they require LEM to prove the recursor and such - Your definition of
`eq`

is not strong enough: in lean you can prove`eq.subst`

when`P : A -> Sort u`

, not just`Prop`

. I believe your construction is equivalent to lean's`eq`

, but you need to use lean's`eq`

to prove the equivalence... - The
`unit`

construction is wrong,`Sort u`

is not a singleton type `punit`

isn't actually universe polymorphic like lean's- The
`bool`

model will make`bool.cases`

noncomputable - The
`option`

model makes`option.cases`

noncomputable

#### Trebor Huang (Jan 15 2022 at 18:51):

I think it's worth reading how all the (non-dependent) inductive types can be encoded in an impredicative type theory like the Calculus of Constructions -- It doesn't even have any built-in inductive types!

However, with Lean, you have universe level problems, and also defeqs and computability will break. `eq`

doesn't work as Carneiro points out, and I think (handwavingly) that this is connected to the fact that to make a category finitely complete, you need a terminal object, binary products and equalizers.

#### Mario Carneiro (Jan 15 2022 at 18:58):

You should also check out Church encodings, which are a general mechanism for encoding inductive types in lambda calculus or System F (i.e. a haskell-like type theory). Unfortunately it doesn't work properly in the presence of a universe hierarchy, which is why CIC builds it in instead

#### Chris B (Jan 15 2022 at 19:01):

Patrick Johnson said:

Of course. But I'm not talking about the user interface at all. When you define an inductive type, all that you get back from the kernel are some constants and their types. The meta level code then proves other things, noconfusion, induction, dcases, and similar lemmas. My point is that we can only have a small number of builtin constants and define everything other in terms of that. User would not see any difference (except that a recursor of a type will actually have a concrete definition).

Recursors are already given a concrete definition by the kernel, they get lambda/value-level term(s) in the form of a reduction rule.

The point of the lean 3 mutual inductives example was that the introduction of an intermediate mapping between what's going on in the kernel and what the user sees has a high chance of bleeding through into the UX. Giving users feedback or letting them look at lower level information about their inductive now requires you to go back and forth through this translation layer in a manner that's completely transparent.

If the idea was that users would write their inductives explicitly in terms of the primitives you (or Mario) mentioned then that wouldn't be the case, but you would have a different proof assistant at that point.

#### Eric Wieser (Jan 16 2022 at 00:23):

Note that by using `dite`

in your definitions above, you're using another inductive type, docs#decidable

Last updated: Aug 03 2023 at 10:10 UTC