Quinn (Nov 06 2021 at 14:29): 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"?
Pierre-Marie Pédrot (Nov 06 2021 at 14:30):In what language? Gallina or Ltac?
Quinn (Nov 06 2021 at 14:30):gallina
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
Pierre-Marie Pédrot (Nov 06 2021 at 14:30):Well, that would break every nice property of CIC then.
Pierre-Marie Pédrot (Nov 06 2021 at 14:30):In theory you can add such a type-case primitive
Quinn (Nov 06 2021 at 14:31):intriguing!
Quinn (Nov 06 2021 at 14:31):also, what?
Pierre-Marie Pédrot (Nov 06 2021 at 14:31):(it's implementable as a syntactic model using induction recursion)
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
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
Pierre-Marie Pédrot (Nov 06 2021 at 14:32):with such a combinator it becomes trivial to break e.g. univalence
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
Pierre-Marie Pédrot (Nov 06 2021 at 14:34):so, in a nutshell: yes you can, but you probably don't want that
Quinn (Nov 06 2021 at 14:34):coq-club is the email list?
Pierre-Marie Pédrot (Nov 06 2021 at 14:37):yep
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
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
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)
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?
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).
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.
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,
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.
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.
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: Apr 20 2024 at 09:01 UTC