I am struggling to understand the ideas behind inductive types in pcuic:

First I imagine the interesting part is:

```
Inductive term :=
...
| tInd (ind : inductive) (ui : Instance.t)
| tConstruct (ind : inductive) (n : nat) (ui : Instance.t)
```

I am also trying to connect that to: https://coq.inria.fr/refman/language/core/inductive.html#theory-of-inductive-definitions in quest of implementing my own version of inductive types in my toy language (no mutual induction)

I will start from the first one: `tInd`

It is not clear what is the point of `ui`

, I imagined, the inductive type basically a list list of terms ? (list of arrows)

then the inductive type `inductive`

which is basically a name and a number, and I cannot see how that relates to the list of lists idea,

The same goes to `tConstruct`

, I imagined it to be list of constructors, but I cannot understand how this relate to the current definition.

P.S. I am also looking at the 1997 paper by dybjer on inductive families and trying to link that to this presentation, and it does not make sense.

`inductive`

is the pair of a kername and a natural : the kername is the address of the definition of the [mutual] inductive in the global environment and the natural is simply the index of the inductive among the mutual inductives.

The `Instance.t`

element is the universe instantiation for universe polymorphism.

The additional natural for constructors is the index among constructors for the specific inductive

The inductive information you were expecting here are all only present in the inductive definition, in the entry of the environment (Environment.v, `InductiveDecl`

)

I am not sure I understand what you mean by 'universe polymorphism' in this context, I assumed that pcuic has comulative universes and it does not support universe polymorphism.

also I wonder why are inductive types not defined as normal types and only refereed to by name (as opposed to pi types, for instance where is refered to by the data itself)

Inductive types are nominal: if you define two pair types with "the same" definition, they'll be distinct

you can't literally use "the same" definition in the same module, but you can just rename constructors, or define the types in different modules

(EDITED)

```
Module M1.
Inductive V := A.
Definition T := unit.
End M1.
Module M2.
Inductive V := A.
Definition T := unit.
End M2.
Fail Definition f (x : M1.V) : M2.V := x.
Definition f (x : M1.T) : M2.T := x.
```

in this examples, `M1.T`

and `M2.T`

are normal type definitions — conversion checking can delta-reduce `M1.T`

to its body (`unit`

), so `f`

's 2nd version typechecks — while `M1.V`

and `M2.V`

aren't definitions, so `f`

's 1st version does not typecheck

walker said:

I am not sure I understand what you mean by 'universe polymorphism' in this context, I assumed that pcuic has comulative universes and it does not support universe polymorphism.

pcuic has both cumulative universes and universe polymorphism

Paolo Giarrusso said:

you can't literally use "the same" definition in the same module, but you can just rename constructors, or define the types in different modules

but why would that be a desirable property for inductive types ? wouldn't it be nice to always have eta equality ? It sounds like limitation to me

(deleted)

Gaëtan Gilbert said:

walker said:

I am not sure I understand what you mean by 'universe polymorphism' in this context, I assumed that pcuic has comulative universes and it does not support universe polymorphism.

pcuic has both cumulative universes and universe polymorphism

but coq itself does not have universe polymorphism does it ? just to make sure we are talking about the same thing, I am imagining this:

https://agda.readthedocs.io/en/v2.6.0/language/universe-levels.html#id2

Coq has universe polymorphism, although 2nd class where agda is more 1st class

https://coq.github.io/doc/master/refman/addendum/universe-polymorphism.html

basically agda has this special `Level`

type, but in Coq universe quantification is prenex on global references and separate from `forall`

/`fun`

quantifiers

noted, in this the only question I have left is why eta equivalence are not used for inductive types? that is if two types are defined exactly the same (syntactically) then they are not equal.

with syntactic equality? what would even be the point?

so as I understand inductive types are not defined the same way pi type is defined. for inductive types, the type is kept in the environment, while only reference to it it used by `tInd`

.

As Paolo just said, this is done so that if two inductive types are the defined the same way (they are syntactically the same) they still cannot be equal in coq. but this feels like artificial limitation,and I don't see the point.

it's more efficient, easier to implement and probably produces better errors

noted, thanks for the clarification

1 last question, is there a way to quickly convert coq terms to pcuic tree, I find it hard to statically read the code and want a way to quickly test stuff (ie see how nats , lists ...etc are represented)

for instance, many pieces of this structure `one_inductive_body`

does not make sense, and while It will be nice to ask direct question about the parts that does not make sense, I want to know how to use pcuic in relation to coq directly

is there a way to quickly convert coq terms to pcuic tree

`From MetaCoq.TemplatePCUIC Require Import Loader. Check <% 0 %>. Check <# 0 #>.`

I am not sure if `Template`

and `TemplatePCUIC`

are the same thing, but there is no path called `TemplatePCUIC`

at least from package installed metacoq,

Also is there a way to nicely display strings? The ones coming from metacoq looks a bit distracting

```
(Kernames.MPfile
(bytestring.String.String "D"
(bytestring.String.String "a"
(bytestring.String.String "t"
(bytestring.String.String "a"
...
```

Also I was more interested in seeing the internal details of `\Sigma`

and that is not viewable when quoting

You need to import the string notation from the bytestring module (can’t remember exactly what it is)

found it, just simple `Import bytestring.`

, thanks a lot!

I noticed there is no distinction made between applyig constructor to arguments and applying function to argument, both are done using `tApp`

, shouldn't they be completely different thing ?

from my understanding applying lambas to argument has computational meaning and reduce to something simpler, while applying constructors to arguments are actually in normal form

for instance `S : nat -> nat`

exists as a term, you don't have to eta expand to use it unlike eg ocaml

I am not sure I am following the point, I understand why `S`

does not eta expand, but I imagined that `S Z`

will be different from say `pred Z`

at least in the internal logical representation,

But `S`

is somehow represented as a product type and that confuses me when thinking of reduction and other metatheoritic properties.

Well there is no need to distinguish them so no.

If you want to distinguish constructor and function application, how do you represent `fun f : nat -> nat => f 1`

? How `(fun f : nat -> nat => f 1) S`

and how `(fun f : nat -> nat => f 1) pred`

walker said:

I am not sure I am following the point, I understand why

`S`

does not eta expand, but I imagined that`S Z`

will be different from say`pred Z`

at least in the internal logical representation,

But`S`

is somehow represented as a product type and that confuses me when thinking of reduction and other metatheoritic properties.

I don't understand this. The type of S is a function type in Coq, no?

`S`

*does* $\eta$-expand.

my point of confusion i that function application are usually defined as neutral values? in this case, would it be possible for funtion applications to be values, neutral values, or reducible terms ?

What Gaëtan said is that you don't *need* to $\eta$-expand it to consider it at type `nat -> nat`

.

walker said:

my point of confusion i that function application are usually defined as neutral values? in this case, would it be possible for funtion applications to be values, neutral values, or reducible terms ?

Function applications are neutral when the term in function position is neutral. A constructor is not neutral.

walker said:

my point of confusion i that function application are usually defined as neutral values? in this case, would it be possible for funtion applications to be values, neutral values, or reducible terms ?

The syntax of PCUIC doesn't distinguish these things. Terms are just terms. If you want to define these notions you have to start again, or use predicates.

Some of them might be defined already in the metatheory, but when thinking about the definition of syntax you shouldn't think about these notions

I think I just confused my self, it all now makes sense.

Last updated: Jul 23 2024 at 20:01 UTC