Safe Haskell | None |
---|---|

Language | Haskell2010 |

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.

## Synopsis

- data ProjectionView
- unProjView :: ProjectionView -> Term
- projView :: HasConstInfo m => Term -> m ProjectionView
- reduceProjectionLike :: Term -> TCM Term
- elimView :: Bool -> Term -> TCM Term
- eligibleForProjectionLike :: HasConstInfo m => QName -> m Bool
- makeProjection :: QName -> TCM ()

# Documentation

data ProjectionView Source #

View for a `Def f (Apply a : es)`

where `isProjection f`

.
Used for projection-like `f`

s.

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

- 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 :: Term -> TCM 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.)

elimView :: Bool -> Term -> TCM 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`

:

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

s body may not mention the paramters.

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 test*Succeed*NotProjectionLike.agda