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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Polarity

Contents

- Polarity computation
- Auxiliary functions

Description

Computing the polarity (variance) of function arguments, for the sake of subtyping.

Synopsis

- computePolarity :: (HasOptions m, HasConstInfo m, HasBuiltins m, MonadTCEnv m, MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m, MonadDebug m, MonadPretty m) => [QName] -> m ()
- composePol :: Polarity -> Polarity -> Polarity
- nextPolarity :: [Polarity] -> (Polarity, [Polarity])
- purgeNonvariant :: [Polarity] -> [Polarity]
- polFromOcc :: Occurrence -> Polarity

# Polarity computation

computePolarity :: (HasOptions m, HasConstInfo m, HasBuiltins m, MonadTCEnv m, MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m, MonadDebug m, MonadPretty m) => [QName] -> m () Source #

Main function of this module.

# Auxiliary functions

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

What is the polarity of a function composition?

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

polFromOcc :: Occurrence -> Polarity Source #