Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.ProjectionLike

Description

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.

Synopsis

- data ProjectionView
  - = ProjectionView {
    - projViewProj :: QName
    - projViewSelf :: Arg Term
    - projViewSpine :: Elims
    }
  - | LoneProjectionLike QName ArgInfo
  - | NoProjection Term
- unProjView :: ProjectionView -> Term
- projView :: HasConstInfo m => Term -> m ProjectionView
- reduceProjectionLike :: PureTCM m => Term -> m Term
- data ProjEliminator
  - = EvenLone
  - | ButLone
  - | NoPostfix
- elimView :: PureTCM m => ProjEliminator -> Term -> m Term
- eligibleForProjectionLike :: HasConstInfo m => QName -> m Bool
- makeProjection :: QName -> TCM ()
- inferNeutral :: (PureTCM m, MonadBlock m) => Term -> m Type
- computeDefType :: (PureTCM m, MonadBlock m) => QName -> Elims -> m Type

# Documentation

data ProjectionView Source #

View for a `Def f (Apply a : es)` where `isRelevantProjection f`. Used for projection-like `f`s.

Constructors

ProjectionView | A projection or projection-like function, applied to its principal argument

Fields

- projViewProj :: QName
- projViewSelf :: Arg Term
- projViewSpine :: Elims

LoneProjectionLike QName ArgInfo | Just a lone projection-like function, missing its principal argument (from which we could infer the parameters).
NoProjection Term | Not a projection or projection-like thing.

unProjView :: ProjectionView -> Term Source #

Semantics of `ProjectionView`.

projView :: HasConstInfo m => Term -> m ProjectionView Source #

Top-level `ProjectionView` (no reduction).

reduceProjectionLike :: PureTCM m => Term -> m Term Source #

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

data ProjEliminator Source #

Constructors

EvenLone |
ButLone |
NoPostfix |

#### Instances

Instances details

Eq ProjEliminator Source # |
Instance details Defined in Agda.TypeChecking.ProjectionLike Methods (==) :: ProjEliminator -> ProjEliminator -> Bool Source # (/=) :: ProjEliminator -> ProjEliminator -> Bool Source #

elimView :: PureTCM m => ProjEliminator -> Term -> m Term Source #

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.

eligibleForProjectionLike :: HasConstInfo m => QName -> m Bool Source #

Which `Def`types are eligible for the principle argument of a projection-like function?

makeProjection :: QName -> TCM () Source #

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. `f`s 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

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

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.

computeDefType :: (PureTCM m, MonadBlock m) => QName -> Elims -> m Type Source #

Compute the head type of a Def application. For projection-like functions this requires inferring the type of the principal argument.