Stream: MetaCoq

Topic: understanding inductive types


view this post on Zulip walker (Apr 10 2023 at 16:52):

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.

view this post on Zulip Yann Leray (Apr 10 2023 at 17:08):

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

view this post on Zulip Yann Leray (Apr 10 2023 at 17:10):

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

view this post on Zulip walker (Apr 10 2023 at 19:33):

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.

view this post on Zulip walker (Apr 10 2023 at 19:35):

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)

view this post on Zulip Paolo Giarrusso (Apr 10 2023 at 19:37):

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

view this post on Zulip Paolo Giarrusso (Apr 10 2023 at 19:38):

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

view this post on Zulip Paolo Giarrusso (Apr 10 2023 at 19:40):

(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.

view this post on Zulip Paolo Giarrusso (Apr 10 2023 at 19:43):

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

view this post on Zulip Gaëtan Gilbert (Apr 10 2023 at 20:03):

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

view this post on Zulip walker (Apr 10 2023 at 20:06):

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

view this post on Zulip walker (Apr 10 2023 at 20:16):

(deleted)

view this post on Zulip walker (Apr 10 2023 at 20:18):

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

view this post on Zulip Gaëtan Gilbert (Apr 10 2023 at 20:19):

Coq has universe polymorphism, although 2nd class where agda is more 1st class
https://coq.github.io/doc/master/refman/addendum/universe-polymorphism.html

view this post on Zulip Gaëtan Gilbert (Apr 10 2023 at 20:20):

basically agda has this special Level type, but in Coq universe quantification is prenex on global references and separate from forall/fun quantifiers

view this post on Zulip walker (Apr 10 2023 at 20:23):

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.

view this post on Zulip Gaëtan Gilbert (Apr 10 2023 at 20:25):

with syntactic equality? what would even be the point?

view this post on Zulip walker (Apr 10 2023 at 20:28):

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.

view this post on Zulip Gaëtan Gilbert (Apr 10 2023 at 20:48):

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

view this post on Zulip walker (Apr 10 2023 at 20:52):

noted, thanks for the clarification

view this post on Zulip walker (Apr 10 2023 at 21:57):

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)

view this post on Zulip walker (Apr 10 2023 at 21:59):

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

view this post on Zulip Jason Gross (Apr 11 2023 at 00:16):

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

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

view this post on Zulip walker (Apr 11 2023 at 08:13):

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

view this post on Zulip Matthieu Sozeau (Apr 11 2023 at 09:32):

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

view this post on Zulip walker (Apr 11 2023 at 09:50):

found it, just simple Import bytestring., thanks a lot!

view this post on Zulip walker (Apr 11 2023 at 10:51):

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 ?

view this post on Zulip walker (Apr 11 2023 at 10:53):

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

view this post on Zulip Gaëtan Gilbert (Apr 11 2023 at 11:03):

for instance S : nat -> nat exists as a term, you don't have to eta expand to use it unlike eg ocaml

view this post on Zulip walker (Apr 11 2023 at 11:11):

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.

view this post on Zulip Théo Winterhalter (Apr 11 2023 at 11:13):

Well there is no need to distinguish them so no.

view this post on Zulip Yannick Forster (Apr 11 2023 at 11:13):

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

view this post on Zulip Yannick Forster (Apr 11 2023 at 11:14):

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?

view this post on Zulip Théo Winterhalter (Apr 11 2023 at 11:16):

S does η\eta-expand.

view this post on Zulip walker (Apr 11 2023 at 11:17):

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 ?

view this post on Zulip Théo Winterhalter (Apr 11 2023 at 11:17):

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

view this post on Zulip Théo Winterhalter (Apr 11 2023 at 11:18):

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.

view this post on Zulip Yannick Forster (Apr 11 2023 at 11:18):

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.

view this post on Zulip Yannick Forster (Apr 11 2023 at 11:18):

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

view this post on Zulip walker (Apr 11 2023 at 11:27):

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


Last updated: Jul 23 2024 at 20:01 UTC