| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
GHC.Core.Multiplicity
Description
This module defines the semi-ring of multiplicities, and associated functions. Multiplicities annotate arrow types to indicate the linearity of the arrow (in the sense of linear types).
Mult is a type synonym for Type, used only when its kind is Multiplicity. To simplify dealing with multiplicities, functions such as mkMultMul perform simplifications such as Many * x = Many on the fly.
Synopsis
- type Mult = Type
- pattern One :: Mult
- pattern Many :: Mult
- isMultMul :: Mult -> Maybe (Mult, Mult)
- mkMultAdd :: Mult -> Mult -> Mult
- mkMultMul :: Mult -> Mult -> Mult
- mkMultSup :: Mult -> Mult -> Mult
- data Scaled a = Scaled Mult a
- scaledMult :: Scaled a -> Mult
- scaledThing :: Scaled a -> a
- unrestricted :: a -> Scaled a
- linear :: a -> Scaled a
- tymult :: a -> Scaled a
- irrelevantMult :: Scaled a -> a
- mkScaled :: Mult -> a -> Scaled a
- scaledSet :: Scaled a -> b -> Scaled b
- scaleScaled :: Mult -> Scaled a -> Scaled a
- data IsSubmult
- submult :: Mult -> Mult -> IsSubmult
- mapScaledType :: (Type -> Type) -> Scaled Type -> Scaled Type
Documentation
Mult is a type alias for Type.
Mult must contain Type because multiplicity variables are mere type variables (of kind Multiplicity) in Haskell. So the simplest implementation is to make Mult be Type.
Multiplicities can be formed with: - One: GHC.Types.One (= oneDataCon) - Many: GHC.Types.Many (= manyDataCon) - Multiplication: GHC.Types.MultMul (= multMulTyCon)
So that Mult feels a bit more structured, we provide pattern synonyms and smart constructors for these.
mkMultSup :: Mult -> Mult -> Mult Source #
mkMultSup w1 w2 returns a multiplicity such that mkMultSup w1
w2 >= w1 and mkMultSup w1 w2 >= w2. See Note [Overapproximating multiplicities].
A shorthand for data with an attached Mult element (the multiplicity).
Instances
| Data a => Data (Scaled a) # | |
Defined in GHC.Core.TyCo.Rep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Scaled a -> c (Scaled a) Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Scaled a) Source # toConstr :: Scaled a -> Constr Source # dataTypeOf :: Scaled a -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Scaled a)) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Scaled a)) Source # gmapT :: (forall b. Data b => b -> b) -> Scaled a -> Scaled a Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scaled a -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scaled a -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Scaled a -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Scaled a -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a) Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a) Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a) Source # | |
| Outputable a => Outputable (Scaled a) # | |
scaledMult :: Scaled a -> Mult Source #
scaledThing :: Scaled a -> a Source #
unrestricted :: a -> Scaled a Source #
Scale a payload by Many
irrelevantMult :: Scaled a -> a Source #