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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Polarity

Contents

- Polarity lattice.
- Auxiliary functions
- Computing the polarity of a symbol.
- Sized types

Synopsis

- (/\) :: Polarity -> Polarity -> Polarity
- neg :: Polarity -> Polarity
- composePol :: Polarity -> Polarity -> Polarity
- polFromOcc :: Occurrence -> Polarity
- nextPolarity :: [Polarity] -> (Polarity, [Polarity])
- purgeNonvariant :: [Polarity] -> [Polarity]
- polarityFromPositivity :: QName -> TCM ()
- computePolarity :: [QName] -> TCM ()
- enablePhantomTypes :: Defn -> [Polarity] -> [Polarity]
- dependentPolarity :: Type -> [Polarity] -> [Polarity] -> TCM [Polarity]
- relevantInIgnoringNonvariant :: Nat -> Type -> [Polarity] -> TCM Bool
- sizePolarity :: QName -> [Polarity] -> TCM [Polarity]
- checkSizeIndex :: QName -> Nat -> Type -> TCM Bool
- class HasPolarity a where
  - polarities :: Nat -> a -> TCM [Polarity]
- polarity :: HasPolarity a => Nat -> a -> TCM Polarity

# Polarity lattice.

(/\) :: Polarity -> Polarity -> Polarity Source #

Infimum on the information lattice. `Invariant` is bottom (dominant for inf), `Nonvariant` is top (neutral for inf).

neg :: Polarity -> Polarity Source #

`Polarity` negation, swapping monotone and antitone.

composePol :: Polarity -> Polarity -> Polarity Source #

What is the polarity of a function composition?

polFromOcc :: Occurrence -> Polarity Source #

# Auxiliary functions

nextPolarity :: [Polarity] -> (Polarity, [Polarity]) Source #

Get the next polarity from a list, `Invariant` if empty.

purgeNonvariant :: [Polarity] -> [Polarity] Source #

Replace `Nonvariant` by `Covariant`. (Arbitrary bias, but better than `Invariant`, see issue 1596).

polarityFromPositivity :: QName -> TCM () Source #

A quick transliterations of occurrences to polarities.

# Computing the polarity of a symbol.

computePolarity :: [QName] -> TCM () Source #

Main function of this module.

enablePhantomTypes :: Defn -> [Polarity] -> [Polarity] Source #

Data and record parameters are used as phantom arguments all over the test suite (and possibly in user developments). `enablePhantomTypes` turns `Nonvariant` parameters to `Covariant` to enable phantoms.

dependentPolarity :: Type -> [Polarity] -> [Polarity] -> TCM [Polarity] Source #

Make arguments `Invariant` if the type of a not-`Nonvariant` later argument depends on it. Also, enable phantom types by turning `Nonvariant` into something else if it is a data/record parameter but not a size argument. [See issue 1596]

Precondition: the "phantom" polarity list has the same length as the polarity list.

relevantInIgnoringNonvariant :: Nat -> Type -> [Polarity] -> TCM Bool Source #

Check whether a variable is relevant in a type expression, ignoring domains of non-variant arguments.

# Sized types

sizePolarity :: QName -> [Polarity] -> TCM [Polarity] Source #

Hack for polarity of size indices. As a side effect, this sets the positivity of the size index. See testsucceedPolaritySizeSucData.agda for a case where this is needed.

checkSizeIndex :: QName -> Nat -> Type -> TCM Bool Source #

`checkSizeIndex d i a` checks that constructor target type `a` has form `d ps (↑ⁿ i) idxs` where `|ps| = np(d)`.

Precondition: `a` is reduced and of form `d ps idxs0`.

class HasPolarity a where Source #

`polarities i a` computes the list of polarities of de Bruijn index `i` in syntactic entity `a`.

Methods

polarities :: Nat -> a -> TCM [Polarity] Source #

Instances

HasPolarity LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> LevelAtom -> TCM [Polarity] Source #
HasPolarity PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> PlusLevel -> TCM [Polarity] Source #
HasPolarity Level Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Level -> TCM [Polarity] Source #
HasPolarity Type Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Type -> TCM [Polarity] Source #
HasPolarity Term Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Term -> TCM [Polarity] Source #
HasPolarity a => HasPolarity [a] Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> [a] -> TCM [Polarity] Source #
HasPolarity a => HasPolarity (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Dom a -> TCM [Polarity] Source #
HasPolarity a => HasPolarity (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Arg a -> TCM [Polarity] Source #
HasPolarity a => HasPolarity (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Abs a -> TCM [Polarity] Source #
HasPolarity a => HasPolarity (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Elim' a -> TCM [Polarity] Source #
(HasPolarity a, HasPolarity b) => HasPolarity (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> (a, b) -> TCM [Polarity] Source #

polarity :: HasPolarity a => Nat -> a -> TCM Polarity Source #

`polarity i a` computes the polarity of de Bruijn index `i` in syntactic entity `a` by taking the infimum of all `polarities`.