Here follows a summary of what Coq implements in terms of record types, intended to serve as support to clarify the ideal design we'd like to implement.
Let's call "record type" a (possibly-parametric) type with a tuple constructor {| ... pi := ti ... |}
and projections t.(pi)
together with β-rules {| ... pi := ti ... |}.(pi) -> ti
and η-rule u == {| ... pi := u.(pi) ... |}
.
Let's say that a tuple constructor {| ... pi := ti ... |}
is algebraic if it is a proper construction involving all ti
at once and applicative if there is a tuple constructor name specific to the record type T
, say Build_T
such that {| ... pi := ti ... |}
is obtained by application Build_T ... ti ...
. In particular, Build_T
is a name for the applicative tuple constructor. The notion of name can be applied to algebraic tuple constructors also: we say that an algebraic tuple constructor is nameable if there is an alternative way to write {| ... pi := ti ... |}
as an algebraically-represented Build_T ... ti ...
.
Similarly, let's say that a projection t.(pi)
is algebraic if it is a proper construction involving t
and applicative if there is a projection name, say p
such that t.(p)
is obtained by application p t
. In both cases, the projections are named, thus nameable.
Let's say that an algebraic tuple is optimized if the parameters of the type are omitted in the representation and reconstructed from the context. Let's say that an algebraic projection t.(p)
is optimized if the parameters of the type are omitted in the representation and reconstructed from the type of t
.
The presence of a name is useful in particular to control evaluation of terms: by giving a name, one may activate or deactivate on demand the use of a β-rule in the evaluation (intuitively, as in cbv [p]
and cbv -[p]
). If the name can indeed be used to control a given evaluator, we say that the corresponding construction has controllable reduction.
With this terminology, Coq currently provides record types:
Construct(Build_T)
with all of:
Proj((p,folded),t)
Const(p)
Proj((p,unfolded),t)
where η is not supported for technical reasons for unit records (i.e. records w/o projections) and not supported for undecidability reasons for recursive records
Set Printing Unfolded Projection As Match
, suggesting that the role of 3. is to emulate one-constructor positive types (see below)Unset Printing Primitive Projection Parameters
Let's call "one-constructor positive type" a (possibly-parametric) type with one-constructor constructed terms C ... ti ...
and a positive eliminator match t with C ... xi ... => u end
together with β-rule match C ... ti ... with C ... xi ... => u end -> u[... xi:=ti ...]
and η-rule E[t] == match t with C ... xi ... => E[C ... xi ...] end
.
As before, let's say that a constructed term C ... ti ...
is algebraic if it is a proper construction involving all ti
at once and applicative if the constructor name C
is a stand-alone expression such that C ... ti ...
is obtained by application of C
. In both cases, there is an associated name: we do not consider here anonymously constructed terms.
Let's say that a positive eliminator match t with C ... xi ... => u end
is algebraic if it is a proper construction involving t
and u(...xi...)
and applicative if there is a constant name case
such that match t with C ... xi ... => u end
is obtained as the application case t (fun ...xi... => u)
. Here, match
is unnamed but case
has a name and is thus nameable.
As before, let's say that an algebraic constructed term C ... ti ...
is optimized if the parameters of the type are omitted in the representation and reconstructed from the context. Let's say that an algebraic positive eliminator match t with C ... xi ... => u end
is optimized if the parameters of the type are omitted in the representation and reconstructed from the type of t
.
Coq implements one-constructor positive types, with β but not η:
Construct(C)
Cases(t,[|...xi...,u|])
Record types with named tuple constructor can be simulated by one-constructor positive types:
Build_T ... ti ...
, Build_T
can directly be seen as the constructor of a constructed termt.(pi)
can be expressed as match t with Build_T ... xi ... => xi end
, if one accepts to lose the name, and, otherwise, by using a named form of match t with Build_T ... xi ... => xi end
beta
holds whenever it holds on one-constructor positive typeseta
holds whenever it holds on one-constructor positive typesCoq implements the simulation of record types as one-constructor positive types:
{| ... pi:=ti ... |}.(pi) -> ti
is in two steps, transiting via the anonymous projection, so that the simulation is not fully "complete"Conversely, one-constructor positive types can be simulated by record types:
C ... ti ...
, C
can directly be seen as the name of a named tuple constructormatch t with C ... xi ... => u end
can be simulated in two ways:let ... xi:=t.(pi) ... in u
u[...xi:=t.(pi)...]
, which has the property that the record simulation of the positive simulation of t.(pi)
is t.(pi)
itselfCoq has an emulation of one-constructor positive types as record types:
Proj((p,unfolded),t)
formmatch
is simulated in the shared way, except for the special cases match t with C ... xi ... => xi end
which are interpreted in the substituted wayzeta
Referring to the terminology above, what do we want to continue to support and what do we want to change in Coq?
Maybe a stupid remark, but:
why do we really care about emulating match
from positive records by projections in negative records? After all, the only thing we may care from the positive point of view, is to have optimized projections. So why not to recast the difference between unfolded and folded Proj
nodes in negative types as a difference between optimally-represented projections in positive types and optimally-represented projections in negative types, that is to reuse the Proj((p,true),t)
node for positive types rather than negative types as now? No more confusion between them then, since they would live in different types.
The same problem of transparently matching/unifying the Const
and folded Proj
nodes in negative types would then arrive for Const
and unfolded-recast-as-positive Proj
in positive types would appear, but we already have the code for that, so maybe not a so big deal. Moreover, this approach is exactly following the spirit of the Set Printing Unfolded Projection As Match
flag.
I checked what we do in the reduction functions, especially after the last cleaning by Rodolphe and Janno, and, taking also the last version of #18618 into account, the following invariant is currently satisfied:
Const
and Proj(folded)
forms behave like constants and both trigger an unfolding when the corresponding fPROJ
is set,Proj(unfolded)
of a Construct
or CoFix
respectively trigger a fMATCH
or fCOFIX
reduction, w/o caring about fPROJ
.This seems to give an intelligible reduction model and the urgency seems well to provide a nice way to reflect the difference between Proj(unfolded)
from Proj(folded)
. I got with the idea to use the notation t.(|p|)
which is relatively light and somehow matches the {| ... |}
notation.
Concretely, supporting such notation would mean adding a "folded" flag to CProj
, GProj
and NProj
and to propagate it back and forth to Proj
.
Last updated: Oct 13 2024 at 01:02 UTC