Stream: Coq users

Topic: how was a type constructed?


view this post on Zulip Quinn (Nov 06 2021 at 14:29):

Why don't I have some sort of combinator that says "this type was constructed using Inductive" or "this type was constructed using CoInductive"?

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 14:30):

In what language? Gallina or Ltac?

view this post on Zulip Quinn (Nov 06 2021 at 14:30):

gallina

view this post on Zulip Quinn (Nov 06 2021 at 14:30):

i'm guessing in ltac i just call induction foo and if it fails it's not Inductive haha

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 14:30):

Well, that would break every nice property of CIC then.

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 14:30):

In theory you can add such a type-case primitive

view this post on Zulip Quinn (Nov 06 2021 at 14:31):

intriguing!

view this post on Zulip Quinn (Nov 06 2021 at 14:31):

also, what?

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 14:31):

(it's implementable as a syntactic model using induction recursion)

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 14:31):

but then you get a language that behaves like Python and lots of stuff become dead wrong

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 14:32):

there was a thread on Coq-club mildly related to that a few days ago

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 14:32):

with such a combinator it becomes trivial to break e.g. univalence

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 14:33):

since Inductive Box (A : Type) := box : A -> Box A is not equivalent to A anymore

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 14:34):

so, in a nutshell: yes you can, but you probably don't want that

view this post on Zulip Quinn (Nov 06 2021 at 14:34):

coq-club is the email list?

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 14:37):

yep

view this post on Zulip Karl Palmskog (Nov 06 2021 at 14:37):

list of all resources like mailing lists and forums: https://github.com/coq-community/awesome-coq#community

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 14:38):

https://sympa.inria.fr/sympa/arc/coq-club/2021-11/msg00003.html for the thread

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 14:38):

(the original question was about an axiom that makes equality of types commute with forall in the wrong direction)

view this post on Zulip Quinn (Nov 17 2021 at 09:29):

Note that we perform an additional check if v 2 is a constructor of an inductive type (possibly applied to some arguments)

The ConCert paper keeps suggesting to me that I am allowed to infer if a type was built using Inductive. Is there some MetaCoq facility that's throwing me off?

view this post on Zulip Paolo Giarrusso (Nov 17 2021 at 09:34):

This kind of analysis is indeed conceptually possible in metaprogramming — the “no” above was restricted to _normal_ programming (Gallina).

view this post on Zulip Paolo Giarrusso (Nov 17 2021 at 09:36):

and the paragraph with your quote appears to talk about an interpreter* — and interpreters are metaprograms for the language they are interpreting.

*It starts with:

The outline of the most interesting parts of our interpreter is given in Figure 2. Specifically, we show the evaluation of fixpoints and case-expressions.

view this post on Zulip Paolo Giarrusso (Nov 17 2021 at 09:38):

and it’s not even an interpreter for Coq, but for another language, embedded into Coq:

As an instance of our approach, we develop an embedding of the “core” of the Acorn smart contract language into Coq. We call this core language λsmart. This language contains all the essential features of a realistic functional language: System F type system, inductive types,

view this post on Zulip Paolo Giarrusso (Nov 17 2021 at 09:40):

I haven’t read much of the rest, but this much can be explained as follows: one can “embed an object language” (here lambda_smart) into another one (here Coq) — that is, define a type of ASTs, and functions that manipulate the AST.

view this post on Zulip Paolo Giarrusso (Nov 17 2021 at 09:40):

The semantics of λsmart is given as a definitional interpreter [18]. This gives us an executable semantics for the language. Moreover, since the core language we consider is sufficiently close to Acorn, our interpreter can serve as a reference interpreter. The interpreter is implemented in an environment-passing style and works both with named and nameless representations of variables.

view this post on Zulip Paolo Giarrusso (Nov 17 2021 at 09:46):

In this case, the inductive types of lambda_smart are presumably separate from the inductive types of Coq… and that’s why a Gallina program _can_ inspect them: if you embed lambda_smart in Coq, Gallina then can play the role of a metaprogramming language for lambda_smart programs.


Last updated: Jan 31 2023 at 14:03 UTC