Stream: Coq users

Topic: error message, product vs. lambda

Quinn (Nov 06 2021 at 13:39):

Definition lattop {A} `{Lattice A} : A :=
  fun (a b : A) => meet a b.

Error message: The type of this term is a product while it is expected to be A.

Questions:

• does this mean product as in dependent product as in Pi?
• does this meanproduct in the sense that a lambda is an exponential which is a special case of a product?
• is this error message considered good or ideal?

Gaëtan Gilbert (Nov 06 2021 at 13:40):

does this mean product as in dependent product as in Pi?

yes

Paolo Giarrusso (Nov 06 2021 at 14:32):

on point “3”: Probably not ideal, I’ve also noticed it before negatively. @Jim Fehrle might have insights.

Paolo Giarrusso (Nov 06 2021 at 14:34):

on point 2: “Pis” are called products because Pi (x : A) -> B x is equivalent to the product of B x_1, B x2, …, B x_n, … for all elements x_i of A.

Li-yao (Nov 06 2021 at 15:38):

I agree, "product" in that error message also makes me think of pairs before functions. I would find it clearer to say something like "this term is a function (of type "forall a ...") while it is expected to be of type A".

Quinn (Nov 06 2021 at 17:50):

@Paolo Giarrusso that's what I meant by "in the sense that a lambda is an exponential which is a special case of a product"

Jim Fehrle (Nov 07 2021 at 04:15):

@Paolo Giarrusso I know very little about this. It would be good to add the message to the documentation. A cursory search of the source code shows it is one of about 20 pretyping errors. For that matter, the documentation should say something about pretyping! cc: @Théo Zimmermann

Théo Zimmermann (Nov 08 2021 at 08:09):

FWIW, always feel free to open issues on GitHub for error messages that could be improved and / or documented.

Théo Zimmermann (Nov 08 2021 at 08:16):

@Jim Fehrle Today, I would say that pretyping is a mostly internal name (internal in the same sense as vernac, constr, etc.) for something that is called "elaboration" in user-facing documentation (https://coq.inria.fr/refman/language/extensions/index.html). Yes, we should add more documentation on some aspects of elaboration, in particular on unification. Some documentation of unification has been written by @Hugo Herbelin as part of https://github.com/coq/ceps/pull/59. It would be good if it could eventually end up in the refman (at least for the parts that are most relevant to the users), probably as a new sub-chapter of the "Language extensions" chapter.

Karl Palmskog (Nov 08 2021 at 08:17):

I always thought of pretyping as "one of the main steps in Coq's implementation of elaboration" (which nearly every proof assistant does, i.e., nearly every proof assistant has elaboration)

Jim Fehrle (Nov 08 2021 at 20:20):

OK, then the doc should mention that pretyping is part of elaboration. Also elaboration should be in the glossary.

Théo Winterhalter (Nov 08 2021 at 20:22):

Why should it mention the pretyping? The error message never says it's about pretyping does it?

Jim Fehrle (Nov 08 2021 at 22:10):

The doc should mention the term for the benefit of those who read the source code.

Théo Winterhalter (Nov 09 2021 at 06:55):

Oh I see.

Théo Zimmermann (Nov 09 2021 at 07:33):

The doc should mention the term for the benefit of those who read the source code.

Théo Zimmermann (Nov 09 2021 at 07:34):

Why not but then the same reasoning could be done on other internal terms like vernac, which we've recently removed from the refman...

Paolo Giarrusso (Nov 09 2021 at 07:49):

I guess an "internals" glossary would need to be larger

Paolo Giarrusso (Nov 09 2021 at 07:50):

Anyway, I tagged @Jim Fehrle because I guessed that error messages fall into a bucket close to the manual.

Paolo Giarrusso (Nov 09 2021 at 07:50):

And the language should be consistent.

Gaëtan Gilbert (Nov 09 2021 at 08:13):

it would make sense to have the doc mention the phase separation in elaboration: first intern then "pretyping" (tbh I would like to find a good name to rename pretyping to)
this is sometimes relevant, eg Ltac foo := exact c. will intern c but only pretypes when running the tactic, which means notations are resolved at Ltac definition time but it uses the coercions available at tactic execution time.

Paolo Giarrusso (Nov 09 2021 at 09:54):

Indeed, phase separation is crucial at other points too.

Paolo Giarrusso (Nov 09 2021 at 09:55):

Eg, parsing comes before notation scopes are resolved (including Bind Scope), which comes before any actual typechecking; at least AFAICT from blackbox testing.

Karl Palmskog (Nov 09 2021 at 10:06):

Andrej Bauer had a nice abstract breakdown of vernacular -[elboration]-> formalism -[verification]-> kernel at http://math.andrej.com/asset/data/the-dawn-of-formalized-mathematics.pdf#page=23

Karl Palmskog (Nov 09 2021 at 10:17):

Emilio summarized Coq's elaboration here: https://github.com/ejgallego/coq-serapi/blob/v8.13/FAQ.md#how-many-asts-does-coq-have

Jim Fehrle (Nov 09 2021 at 19:40):

Why not but then the same reasoning could be done on other internal terms like vernac, which we've recently removed from the refman...

I consider each term on a case-by-case basis. Pretyping is one of the main steps of elaboration, so naming it will be helpful in the exposition of elaboration. "Vernac" didn't appear to be as useful a concept. If you or others want to include "vernac" in the doc, I'm openminded.

Théo Zimmermann (Nov 10 2021 at 09:30):

Not my point. This was a reply to your suggestion that we needed to "mention the term for the benefit of those who read the source code".

Théo Zimmermann (Nov 10 2021 at 09:32):

Documenting pretyping as a phase in elaboration is also beneficial for users who want to understand how Coq works without reading the source code. Like Gaëtan, I am not so fond of the name. But if we don't have a good replacement, we can keep it.

Gaëtan Gilbert (Nov 10 2021 at 09:34):

"interpretation" is used in a few places (INTERPRETED BY)
using this would mean renaming interp/, which considering it seems to be more appropriately named intern/ should not be a problem

Gaëtan Gilbert (Nov 10 2021 at 09:43):

https://github.com/coq/coq/pull/15158

Paolo Giarrusso (Nov 10 2021 at 09:44):

EDIT: how does pretyping relate to type inference?

Gaëtan Gilbert (Nov 10 2021 at 09:46):

they are similar concepts, but pretyping is defined by the code organization whereas you could include things like implicit argument insertion in inference

Paolo Giarrusso (Nov 10 2021 at 09:48):

I was wondering if more conventional terms could suffice, or if Coq-specific jargon is necessary…

Paolo Giarrusso (Nov 10 2021 at 09:49):

A benefit of “pretyping” seems that it can’t be misunderstood by, say, a POPL audience, while interpretation likely would be misunderstood (without some context)

Last updated: Sep 30 2023 at 05:01 UTC