GHC.Core.Multiplicity

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.

Documentation

type Mult = Type

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.

pattern One :: Mult

pattern Many :: Mult

isMultMul :: Mult -> Maybe (Mult, Mult)

mkMultAdd :: Mult -> Mult -> Mult

mkMultMul :: Mult -> Mult -> Mult

mkMultSup :: Mult -> Mult -> Mult

mkMultSup w1 w2 returns a multiplicity such that mkMultSup w1 w2 >= w1 and mkMultSup w1 w2 >= w2. See Note [Overapproximating multiplicities].

data Scaled a

A shorthand for data with an attached Mult element (the multiplicity).

Constructors

Scaled !Mult a

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)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Scaled a)

toConstr :: Scaled a -> Constr

dataTypeOf :: Scaled a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Scaled a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Scaled a))

gmapT :: (forall b. Data b => b -> b) -> Scaled a -> Scaled a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scaled a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scaled a -> r

gmapQ :: (forall d. Data d => d -> u) -> Scaled a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Scaled a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a)

Outputable a => Outputable (Scaled a)

Defined in GHC.Core.TyCo.Rep

Methods

ppr :: Scaled a -> SDoc

scaledMult :: Scaled a -> Mult

scaledThing :: Scaled a -> a

unrestricted :: a -> Scaled a

Scale a payload by Many

linear :: a -> Scaled a

Scale a payload by One

tymult :: a -> Scaled a

Scale a payload by Many; used for type arguments in core

irrelevantMult :: Scaled a -> a

mkScaled :: Mult -> a -> Scaled a

scaledSet :: Scaled a -> b -> Scaled b

scaleScaled :: Mult -> Scaled a -> Scaled a

data IsSubmult

Constructors

Submult

Unknown

Instances

Show IsSubmult

Defined in GHC.Core.Multiplicity

Methods

showsPrec :: Int -> IsSubmult -> ShowS

show :: IsSubmult -> String

showList :: [IsSubmult] -> ShowS

Outputable IsSubmult

Defined in GHC.Core.Multiplicity

Methods

ppr :: IsSubmult -> SDoc

Eq IsSubmult

Defined in GHC.Core.Multiplicity

Methods

(==) :: IsSubmult -> IsSubmult -> Bool

(/=) :: IsSubmult -> IsSubmult -> Bool

submult :: Mult -> Mult -> IsSubmult

submult w1 w2 check whether a value of multiplicity w1 is allowed where a value of multiplicity w2 is expected. This is a partial order.

mapScaledType :: (Type -> Type) -> Scaled Type -> Scaled Type

Apply a function to both the Mult and the Type in a 'Scaled Type'