HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.ProjectionLike

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:

  1. The type of f is of the form f : Γ → D Γ → ... for some type constructor D which can never reduce.

  2. 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:

  1. 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.

  2. A more general analysis of which arguments are reconstructible can be found in

    Jason C. Reed, Redundancy elimination for LF LFTMP 2004.

  • 2 types
  • 8 values
  • PackageAgda-2.7.0.1
  • Exports10
  • LanguageHaskell2010
  • LicenceMIT
  • SourceProjectionLike.hs
valuereduceProjectionLike :: PureTCM m => Term -> m Term
#

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.)

valueelimView :: PureTCM m => ProjEliminator -> Term -> m Term
#

Turn 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.

valuemakeProjection :: QName -> TCM ()
#

Turn a definition into a projection if it looks like a projection.

Conditions for projection-likeness of f:

  1. The type of f must be of the shape Γ → D Γ → C for D a name (Def) which is eligibleForProjectionLike: data record postulate.

  2. 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:

  1. f cannot be constructor headed

  2. 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

valueinferNeutral :: (PureTCM m, MonadBlock m) => Term -> m Type
#

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.