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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Irrelevance

Contents

- Operations on `Dom`.
- Operations on `Context`.
- Propositions

Description

Compile-time irrelevance.

In type theory with compile-time irrelevance à la Pfenning (LiCS 2001), variables in the context are annotated with relevance attributes. @`Γ = r₁x₁:A₁, ..., rⱼxⱼ:Aⱼ` `To handle irrelevant projections, we also record the current relevance attribute in the judgement. For instance, this attribute is equal to to `Irrelevant` if we are in an irrelevant position, like an irrelevant argument.` `Γ ⊢r t : A` `Only relevant variables can be used:` @

(Relevant x : A) ∈ Γ -------------------- Γ ⊢r x : A @`Irrelevant global declarations can only be used if` r = Irrelevant@.

When we enter a `r'`-relevant function argument, we compose the `r` with `r'` and (left-)divide the attributes in the context by `r'`. @`Γ ⊢r t : (r' x : A) → B r' Γ ⊢(r'·r) u : A --------------------------------------------------------- Γ ⊢r t u : B[u/x]` `No surprises for abstraction:` @

Γ, (r' x : A) ⊢r : B ----------------------------- Γ ⊢r λxt : (r' x : A) → B @@

This is different for runtime irrelevance (erasure) which is ``flat'`, meaning that once one is in an irrelevant context, all new assumptions will be usable, since they are turned relevant once entering the context. See Conor McBride (WadlerFest 2016), for a type system in this spirit:

We use such a rule for runtime-irrelevance: @`Γ, (q q') x : A ⊢q t : B ------------------------------ Γ ⊢q λxt : (q' x : A) → B` @

Conor's system is however set up differently, with a very different variable rule:

@@

(q x : A) ∈ Γ -------------- Γ ⊢q x : A

Γ, (q·p) x : A ⊢q t : B ----------------------------- Γ ⊢q λxt : (p x : A) → B

Γ ⊢q t : (p x : A) → B Γ' ⊢qp u : A ------------------------------------------------- Γ + Γ' ⊢q t u : B[u/x] @@

Synopsis

- hideAndRelParams :: Dom a -> Dom a
- workOnTypes :: TCM a -> TCM a
- workOnTypes' :: Bool -> TCM a -> TCM a
- applyRelevanceToContext :: (MonadTCEnv tcm, LensRelevance r) => r -> tcm a -> tcm a
- applyRelevanceToContextOnly :: MonadTCEnv tcm => Relevance -> tcm a -> tcm a
- applyRelevanceToJudgementOnly :: MonadTCEnv tcm => Relevance -> tcm a -> tcm a
- applyRelevanceToContextFunBody :: (MonadTCM tcm, LensRelevance r) => r -> tcm a -> tcm a
- applyQuantityToContext :: (MonadTCEnv tcm, LensQuantity q) => q -> tcm a -> tcm a
- applyQuantityToContextOnly :: MonadTCEnv tcm => Quantity -> tcm a -> tcm a
- applyQuantityToJudgementOnly :: MonadTCEnv tcm => Quantity -> tcm a -> tcm a
- applyModalityToContext :: (MonadTCEnv tcm, LensModality m) => m -> tcm a -> tcm a
- applyModalityToContextOnly :: MonadTCEnv tcm => Modality -> tcm a -> tcm a
- applyModalityToJudgementOnly :: MonadTCEnv tcm => Modality -> tcm a -> tcm a
- applyModalityToContextFunBody :: (MonadTCM tcm, LensModality r) => r -> tcm a -> tcm a
- wakeIrrelevantVars :: MonadTCEnv tcm => tcm a -> tcm a
- class UsableRelevance a where
  - usableRel :: Relevance -> a -> TCM Bool
- class UsableModality a where
  - usableMod :: Modality -> a -> TCM Bool
- isPropM :: (LensSort a, MonadReduce m) => a -> m Bool
- isIrrelevantOrPropM :: (LensRelevance a, LensSort a, MonadReduce m) => a -> m Bool

# Operations on `Dom`.

hideAndRelParams :: Dom a -> Dom a Source #

Prepare parts of a parameter telescope for abstraction in constructors and projections.

# Operations on `Context`.

workOnTypes :: TCM a -> TCM a Source #

Modify the context whenever going from the l.h.s. (term side) of the typing judgement to the r.h.s. (type side).

workOnTypes' :: Bool -> TCM a -> TCM a Source #

Internal workhorse, expects value of --experimental-irrelevance flag as argument.

applyRelevanceToContext :: (MonadTCEnv tcm, LensRelevance r) => r -> tcm a -> tcm a Source #

(Conditionally) wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.

Also allow the use of irrelevant definitions.

applyRelevanceToContextOnly :: MonadTCEnv tcm => Relevance -> tcm a -> tcm a Source #

(Conditionally) wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.

Precondition: `Relevance /= Relevant`

applyRelevanceToJudgementOnly :: MonadTCEnv tcm => Relevance -> tcm a -> tcm a Source #

Apply relevance `rel` the the relevance annotation of the (typing/equality) judgement. This is part of the work done when going into a `rel`-context.

Precondition: `Relevance /= Relevant`

applyRelevanceToContextFunBody :: (MonadTCM tcm, LensRelevance r) => r -> tcm a -> tcm a Source #

Like `applyRelevanceToContext`, but only act on context if `--irrelevant-projections`. See issue #2170.

applyQuantityToContext :: (MonadTCEnv tcm, LensQuantity q) => q -> tcm a -> tcm a Source #

(Conditionally) wake up erased variables and make them unrestricted. For instance, in an erased function argument otherwise erased variables may be used, so they are awoken before type checking the argument.

Also allow the use of erased definitions.

applyQuantityToContextOnly :: MonadTCEnv tcm => Quantity -> tcm a -> tcm a Source #

(Conditionally) wake up erased variables and make them unrestricted. For instance, in an erased function argument otherwise erased variables may be used, so they are awoken before type checking the argument.

Precondition: `Quantity /= Quantity1`

applyQuantityToJudgementOnly :: MonadTCEnv tcm => Quantity -> tcm a -> tcm a Source #

Apply quantity `q` the the quantity annotation of the (typing/equality) judgement. This is part of the work done when going into a `q`-context.

Precondition: `Quantity /= Quantity1`

applyModalityToContext :: (MonadTCEnv tcm, LensModality m) => m -> tcm a -> tcm a Source #

(Conditionally) wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.

Also allow the use of irrelevant definitions.

applyModalityToContextOnly :: MonadTCEnv tcm => Modality -> tcm a -> tcm a Source #

(Conditionally) wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.

Precondition: `Modality /= Relevant`

applyModalityToJudgementOnly :: MonadTCEnv tcm => Modality -> tcm a -> tcm a Source #

Apply modality `m` the the modality annotation of the (typing/equality) judgement. This is part of the work done when going into a `m`-context.

Precondition: `Modality /= Relevant`

applyModalityToContextFunBody :: (MonadTCM tcm, LensModality r) => r -> tcm a -> tcm a Source #

Like `applyModalityToContext`, but only act on context if `--irrelevant-projections`. See issue #2170.

wakeIrrelevantVars :: MonadTCEnv tcm => tcm a -> tcm a Source #

Wake up irrelevant variables and make them relevant. This is used when type checking terms in a hole, in which case you want to be able to (for instance) infer the type of an irrelevant variable. In the course of type checking an irrelevant function argument `applyRelevanceToContext` is used instead, which also sets the context relevance to `Irrelevant`. This is not the right thing to do when type checking interactively in a hole since it also marks all metas created during type checking as irrelevant (issue #2568).

class UsableRelevance a where Source #

Check whether something can be used in a position of the given relevance.

This is a substitute for double-checking that only makes sure relevances are correct. See issue #2640.

Used in unifier (`unifyStep Solution{}`).

At the moment, this implements McBride-style irrelevance, where Pfenning-style would be the most accurate thing. However, these two notions only differ how they handle bound variables in a term. Here, we are only concerned in the free variables, used meta-variables, and used (irrelevant) definitions.

Methods

usableRel :: Relevance -> a -> TCM Bool Source #

Instances

UsableRelevance LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> LevelAtom -> TCM Bool Source #
UsableRelevance PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> PlusLevel -> TCM Bool Source #
UsableRelevance Level Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Level -> TCM Bool Source #
UsableRelevance Sort Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Sort -> TCM Bool Source #
UsableRelevance Term Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Term -> TCM Bool Source #
UsableRelevance a => UsableRelevance [a] Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> [a] -> TCM Bool Source #
UsableRelevance a => UsableRelevance (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Dom a -> TCM Bool Source #
UsableRelevance a => UsableRelevance (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Arg a -> TCM Bool Source #
UsableRelevance a => UsableRelevance (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Type' a -> TCM Bool Source #
(Subst t a, UsableRelevance a) => UsableRelevance (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Abs a -> TCM Bool Source #
UsableRelevance a => UsableRelevance (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Elim' a -> TCM Bool Source #
(UsableRelevance a, UsableRelevance b) => UsableRelevance (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> (a, b) -> TCM Bool Source #

class UsableModality a where Source #

Check whether something can be used in a position of the given modality.

This is a substitute for double-checking that only makes sure modalities are correct. See issue #2640.

Used in unifier (`unifyStep Solution{}`).

This uses McBride-style modality checking. It does not differ from Pfenning-style if we are only interested in the modality of the free variables, used meta-variables, and used definitions.

Methods

usableMod :: Modality -> a -> TCM Bool Source #

Instances

UsableModality Level Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Level -> TCM Bool Source #
UsableModality Sort Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Sort -> TCM Bool Source #
UsableModality Term Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Term -> TCM Bool Source #
UsableModality a => UsableModality [a] Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> [a] -> TCM Bool Source #
UsableModality a => UsableModality (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Dom a -> TCM Bool Source #
UsableModality a => UsableModality (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Arg a -> TCM Bool Source #
UsableRelevance a => UsableModality (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Type' a -> TCM Bool Source #
(Subst t a, UsableModality a) => UsableModality (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Abs a -> TCM Bool Source #
UsableModality a => UsableModality (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Elim' a -> TCM Bool Source #
(UsableModality a, UsableModality b) => UsableModality (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> (a, b) -> TCM Bool Source #

# Propositions

isPropM :: (LensSort a, MonadReduce m) => a -> m Bool Source #

Is a type a proposition? (Needs reduction.)

isIrrelevantOrPropM :: (LensRelevance a, LensSort a, MonadReduce m) => a -> m Bool Source #