GHC 10.0.0.20260917 · lts/ghc-10.0.x · 77a8662 · 2026-10-31
ModuleAgda-2.8.0.2Haskell2010
Dropping initial arguments (`parameters') from a function which can be
easily reconstructed from its principal argument.
A function which has such parameters is called ``projection-like''.
The motivation for this optimization comes from the use of nested records.
First, let us look why proper projections need not store the parameters:
The type of a projection f is of the form
f : Γ → R Γ → C
where R is the record type and C is the type of the field f.
Given a projection application
p pars u
we know that the type of the principal argument u is
u : R pars
thus, the parameters pars are redundant in the projection application
if we can always infer the type of u.
For projections, this is case, because the principal argument u must be
neutral; otherwise, if it was a record value, we would have a redex,
yet Agda maintains a β-normal form.
The situation for projections can be generalized to ``projection-like''
functions f. Conditions:
The type of f is of the form f : Γ → D Γ → ... for some
type constructor D which can never reduce.
For every reduced welltyped application f pars u ...,
the type of u is inferable.
This then allows pars to be dropped always.
Condition 2 is approximated by a bunch of criteria, for details see function makeProjection.
Typical projection-like functions are compositions of projections which arise from nested records.
Notes:
This analysis could be dualized to ``constructor-like'' functions whose parameters are reconstructable from the target type. But such functions would need to be fully applied.
A more general analysis of which arguments are reconstructible can be found in
Jason C. Reed, Redundancy elimination for LF LFTMP 2004.
View for a Def f (Apply a : es) where isRelevantProjection f.
Used for projection-like fs.
ProjectionViewA projection or projection-like function, applied to its principal argument
LoneProjectionLike QName ArgInfoJust a lone projection-like function, missing its principal argument (from which we could infer the parameters).
NoProjection TermNot a projection or projection-like thing.
Semantics of ProjectionView.
Top-level ProjectionView (no reduction).
Reduce away top-level projection like functions. (Also reduces projections, but they should not be there, since Internal is in lambda- and projection-beta-normal form.)
Eq ProjEliminatorDefined in Agda-2.8.0.2 · Agda.TypeChecking.ProjectionLikeTurn prefix projection-like function application into postfix ones.
This does just one layer, such that the top spine contains
the projection-like functions as projections.
Used in compareElims in TypeChecking.Conversion
and in Agda.TypeChecking.CheckInternal.
If the Bool is True, a lone projection like function will be turned into a lambda-abstraction, expecting the principal argument. If the Bool is False, it will be returned unaltered.
No precondition. Preserves constructorForm, since it really does only something on (applications of) projection-like functions.
Which Deftypes are eligible for the principle argument
of a projection-like function?
Turn a definition into a projection if it looks like a projection.
Conditions for projection-likeness of f:
The type of f must be of the shape Γ → D Γ → C for D
a name (Def) which is eligibleForProjectionLike:
data record postulate.
The application of f should only get stuck if the principal argument is inferable (neutral). Thus:
a. f cannot have absurd clauses (which are stuck even if the principal
argument is a constructor).
b. f cannot be abstract as it does not reduce outside abstract blocks
(always stuck).
c. f cannot match on other arguments than the principal argument.
d. f cannot match deeply.
e. fs body may not mention the parameters.
f. A rhs of f cannot be a record expression, since this will be
translated to copatterns by recordExpressionsToCopatterns.
Thus, an application of f waiting for a projection
can be stuck even when the principal argument is a constructor.
g. f cannot be an irrelevant definition (Andreas, 2022-03-07, #5809),
as those are not reduced.
For internal reasons:
f cannot be constructor headed
f cannot be recursive, since we have not implemented a function
which goes through the bodies of the f and the mutually recursive
functions and drops the parameters from all applications of f.
Examples for these reasons: see testSucceedNotProjectionLike.agda
Infer type of a neutral term.
See also infer in Agda.TypeChecking.CheckInternal, which has a very similar
logic but also type checks all arguments.
Compute the head type of a Def application. For projection-like functions this requires inferring the type of the principal argument.