| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Polarity
Description
Computing the polarity (variance) of function arguments, for the sake of subtyping.
Synopsis
- computePolarity :: [QName] -> TCM ()
- composePol :: Polarity -> Polarity -> Polarity
- nextPolarity :: [Polarity] -> (Polarity, [Polarity])
- purgeNonvariant :: [Polarity] -> [Polarity]
- polFromOcc :: Occurrence -> Polarity
Polarity computation
computePolarity :: [QName] -> TCM () 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 #