-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Representational subtyping relations and variance roles.
--
-- This lets you coerce containers (among other things) from stronger
-- types to weaker types with zero runtime cost when it's safe to do so,
-- e.g. [Fin n] -> [Int]. This primarily comes into play when
-- using newtypes to impose additional invariants on existing types.
@package attenuation
@version 0.2.0
-- | Internal implementation details of attenuation.
--
-- Prefer Data.Type.Attenuation and
-- Data.Type.Attenuation.Unsafe instead whenever possible. This
-- exports the constructor of Attenuation, which is much easier to
-- misuse by accident than unsafeToCoercion.
module Data.Type.Attenuation.Internal
-- | Attenuation a b is a unidirectional Coercion from
-- a to b.
--
-- "Attenuate: reduce the force, effect, or value of." An
-- Attenuation takes a stronger, stricter type to a weaker, more
-- lax type. It's meant to sound a bit like Coercion, while
-- conveying that it weakens the type of its argument.
--
-- This arises from newtypes that impose additional invariants on their
-- representations: if we define Fin :: Nat -> Type as a
-- newtype over Int, such as in fin-int, then it's safe to
-- coerce Fins to Ints, and Fins to other
-- Fins with larger Nat parameters, but not vice versa.
--
-- Within the module defining this Fin type, we can obtain
-- Coercible between any two Fin types regardless of
-- their roles, because their newtype constructors are in scope, but if
-- we've taken appropriate precautions (namely not exporting the
-- constructor), we can't obtain it outside the module. We can relax this
-- and make the coercion "opt-in" by exporting it in the form of a
-- Coercion with a scary name like unsafeCoFin, but this
-- is still error-prone.
--
-- Instead, we introduce a newtype wrapper around Coercion which
-- restricts it to be used only in the forward direction, and carefully
-- design its API so that it can only be obtained under the appropriate
-- circumstances.
--
-- Attenuation a b can be seen as a witness that a is,
-- semantically and representationally, a subtype of b: that is,
-- any runtime object that inhabits a also inhabits b
-- without any conversion.
newtype Attenuation a b
Attenuation :: Coercion a b -> Attenuation a b
-- | Attenuable a b is satisfiable iff there exists an
-- Attenuation a b.
--
-- Since an Attenuation is unique for a given pair of types (as
-- it's internally just a wrapper around a Coercible instance),
-- any way of obtaining an Attenuation gives exactly the same
-- result. This means all Attenuable instances that could
-- exist for a pair of types are also identical. In turn, this means that
-- even "incoherent" instances for Attenuable are actually
-- coherent after all: any arbitrary choice of an instance gives the same
-- result. As such, it's perfectly fine for instances of
-- Attenuable to be marked INCOHERENT, as long as it
-- results in good instance resolution behavior. This is used to provide
-- some convenient "fallback" instances filling in the (numerous) gaps in
-- the set of specific instances: specifically, automatic demotion of
-- Coercible to Attenuable; and automatic lifting of
-- Attenuable across Functors and Bifunctors.
--
-- The word "satisfiable" in the first paragraph is chosen carefully: not
-- all instances that are satisfiable will be solved automatically by
-- GHC. One can obtain Attenuable instances by \\ or by an
-- entailment (:-), for some types that wouldn't be solved by any
-- of the "real" instances. In particular, this is useful for
-- compositions of attenuations and for lifting attenuations across
-- Contravariants and Profunctors.
class Attenuable a b
attenuation :: Attenuable a b => Attenuation a b
attenuation :: (Attenuable a b, Coercible a b) => Attenuation a b
-- | A witness that a occurs representationally in s and
-- that, when substituting it for b, you get t.
--
-- These compose like Lenses from the "lens" package, so you can e.g.
-- lift Attenuations through several Functors by
-- co.co.co $ x.
type Variance s t a b = Attenuation a b -> Attenuation s t
-- | A constraint that behaves like type role f representational.
--
-- This means that if we have this constraint in context and GHC can
-- solve Coercible for some types a and b, it
-- will also lift the coercion to f a and f b.
type Representational f = (forall a b. Coercible a b => Coercible (f a) (f b) :: Constraint)
-- | A constraint that behaves like type role f representational
-- _.
--
-- See also Representational.
type Representational0 f = (forall a b x. Coercible a b => Coercible (f a x) (f b x) :: Constraint)
-- | A constraint that behaves like type role f _
-- representational.
--
-- See also Representational.
type Representational1 f = (forall a b x. Coercible a b => Coercible (f x a) (f x b) :: Constraint)
-- | Any type is unidirectionally-coercible to itself.
refl :: Attenuation a a
-- | Transitivity of Attenuations. See also the Category
-- instance.
trans :: Attenuation a b -> Attenuation b c -> Attenuation a c
-- | Lift an Attenuation covariantly over a type constructor
-- f.
--
-- Although we don't use the Functor constraint, it serves
-- an important purpose: to guarantee that the type parameter a
-- doesn't appear contravariantly in f a; otherwise it'd be
-- impossible to write a Functor instance. This is used as a
-- standin for more-detailed "covariant" and "contravariant" type roles,
-- which GHC doesn't have because there's no built-in notion of subtyping
-- to use them with. Representational1 provides the actual lifting
-- of coercions, and Functor guarantees we've got the variance
-- right.
co :: (Functor f, Representational f) => Variance (f a) (f b) a b
-- | Lift an Attenuation covariantly over the left of a
-- Bifunctor.
--
-- Like with co and contra, we require a not-actually-used
-- constraint as proof that the type has the appropriate variance. Since
-- there's not a commonly-used class for functors over the last-but-one
-- parameter, we use Bifunctor. Sadly, this rules out types which
-- are covariant in parameter -1 and contravariant in parameter -0.
fstco :: (Bifunctor f, Representational0 f) => Variance (f a x) (f b x) a b
-- | Lift an Attenuation covariantly over the last-but-one type
-- parameter.
--
-- Like with co and contra, we require a not-actually-used
-- constraint as proof that the type has the appropriate variance. Since
-- there's not a commonly-used class for functors over the last-but-one
-- parameter, we use Bifunctor. Sadly, this rules out types which
-- are covariant in parameter -1 and contravariant in parameter -0.
--
-- Note that any particular type with a Bifunctor f instance
-- should also have Functor (f x), so co should work on
-- any type that sndco works on, but in polymorphic contexts, the
-- Functor instance may not be available.
sndco :: (Bifunctor f, Representational1 f) => Variance (f x a) (f x b) a b
-- | Lift an Attenuation contravariantly over the argument of a
-- functiwon.
domain :: Variance (b -> x) (a -> x) a b
-- | Lift an Attenuation covariantly over the result of a function.
--
-- This is just a specialization of co.
codomain :: Variance (x -> a) (x -> b) a b
-- | Lift a Coercion over a type constructor.
rep :: Representational f => Coercion a b -> Coercion (f a) (f b)
-- | Lift a Coercion over the last-but-one parameter of a type
-- constructor.
rep0 :: Representational0 f => Coercion a b -> Coercion (f a x) (f b x)
-- | Lift an Attenuation to a constraint within a subexpression.
--
-- This is just specialization of withDict; consider using that or
-- (\\).
withAttenuation :: Attenuation a b -> (Attenuable a b => r) -> r
instance forall k (a :: k) (b :: k). GHC.Show.Show (Data.Type.Attenuation.Internal.Attenuation a b)
instance forall k (a :: k) (b :: k). GHC.Classes.Ord (Data.Type.Attenuation.Internal.Attenuation a b)
instance forall k (a :: k) (b :: k). GHC.Classes.Eq (Data.Type.Attenuation.Internal.Attenuation a b)
instance forall k (a :: k) (b :: k). GHC.Types.Coercible a b => Data.Type.Attenuation.Internal.Attenuable a b
instance Data.Type.Attenuation.Internal.Attenuable a a
instance forall k (a :: k) (b :: k). Data.Constraint.HasDict (Data.Type.Attenuation.Internal.Attenuable a b) (Data.Type.Attenuation.Internal.Attenuation a b)
instance (GHC.Base.Functor f, Data.Type.Attenuation.Internal.Representational f, Data.Type.Attenuation.Internal.Attenuable x y) => Data.Type.Attenuation.Internal.Attenuable (f x) (f y)
instance (Data.Bifunctor.Bifunctor f, Data.Type.Attenuation.Internal.Representational0 f, Data.Type.Attenuation.Internal.Representational1 f, Data.Type.Attenuation.Internal.Attenuable a c, Data.Type.Attenuation.Internal.Attenuable b d) => Data.Type.Attenuation.Internal.Attenuable (f a b) (f c d)
instance (Data.Type.Attenuation.Internal.Attenuable c a, Data.Type.Attenuation.Internal.Attenuable b d) => Data.Type.Attenuation.Internal.Attenuable (a -> b) (c -> d)
instance (Data.Type.Attenuation.Internal.Attenuable a a', Data.Type.Attenuation.Internal.Attenuable b b') => Data.Type.Attenuation.Internal.Attenuable (a, b) (a', b')
instance (Data.Type.Attenuation.Internal.Attenuable a a', Data.Type.Attenuation.Internal.Attenuable b b', Data.Type.Attenuation.Internal.Attenuable c c') => Data.Type.Attenuation.Internal.Attenuable (a, b, c) (a', b', c')
instance Control.Category.Category Data.Type.Attenuation.Internal.Attenuation
-- | Representational subtyping relations and variance roles.
module Data.Type.Attenuation
-- | Attenuation a b is a unidirectional Coercion from
-- a to b.
--
-- "Attenuate: reduce the force, effect, or value of." An
-- Attenuation takes a stronger, stricter type to a weaker, more
-- lax type. It's meant to sound a bit like Coercion, while
-- conveying that it weakens the type of its argument.
--
-- This arises from newtypes that impose additional invariants on their
-- representations: if we define Fin :: Nat -> Type as a
-- newtype over Int, such as in fin-int, then it's safe to
-- coerce Fins to Ints, and Fins to other
-- Fins with larger Nat parameters, but not vice versa.
--
-- Within the module defining this Fin type, we can obtain
-- Coercible between any two Fin types regardless of
-- their roles, because their newtype constructors are in scope, but if
-- we've taken appropriate precautions (namely not exporting the
-- constructor), we can't obtain it outside the module. We can relax this
-- and make the coercion "opt-in" by exporting it in the form of a
-- Coercion with a scary name like unsafeCoFin, but this
-- is still error-prone.
--
-- Instead, we introduce a newtype wrapper around Coercion which
-- restricts it to be used only in the forward direction, and carefully
-- design its API so that it can only be obtained under the appropriate
-- circumstances.
--
-- Attenuation a b can be seen as a witness that a is,
-- semantically and representationally, a subtype of b: that is,
-- any runtime object that inhabits a also inhabits b
-- without any conversion.
data Attenuation a b
-- | An operator form of Attenuation, by analogy to (:~:).
type (:⊆:) = Attenuation
-- | Coerce along an Attenuation.
--
-- This is really, truly a coercion when it reaches Core.
attenuateWith :: Attenuation a b -> a -> b
-- | Any coercible types have an Attenuation.
coercible :: Coercible a b => Attenuation a b
-- | Transitivity of Attenuations. See also the Category
-- instance.
trans :: Attenuation a b -> Attenuation b c -> Attenuation a c
-- | Any type is unidirectionally coercible to itself.
repr :: (a :~: b) -> Attenuation a b
-- | Bidirectional coercions can be weakened to unidirectional coercions.
coer :: Coercion a b -> Attenuation a b
-- | If Attenuations in both directions exist, they're actually a
-- Coercion.
iso :: Attenuation a b -> Attenuation b a -> Coercion a b
-- | Attenuations across type constructors can be instantiated.
--
-- This means Attenuations across type constructors lift equality
-- of type parameters to Attenuation of the applied result.
--
-- This is analogous to how Coercible f g works.
inst :: Attenuation f g -> Attenuation (f x) (g x)
-- | A constraint that behaves like type role f representational.
--
-- This means that if we have this constraint in context and GHC can
-- solve Coercible for some types a and b, it
-- will also lift the coercion to f a and f b.
type Representational f = (forall a b. Coercible a b => Coercible (f a) (f b) :: Constraint)
-- | A constraint that behaves like type role f representational
-- _.
--
-- See also Representational.
type Representational0 f = (forall a b x. Coercible a b => Coercible (f a x) (f b x) :: Constraint)
-- | A constraint that behaves like type role f _
-- representational.
--
-- See also Representational.
type Representational1 f = (forall a b x. Coercible a b => Coercible (f x a) (f x b) :: Constraint)
-- | A witness that a occurs representationally in s and
-- that, when substituting it for b, you get t.
--
-- These compose like Lenses from the "lens" package, so you can e.g.
-- lift Attenuations through several Functors by
-- co.co.co $ x.
type Variance s t a b = Attenuation a b -> Attenuation s t
-- | Lift an Attenuation covariantly over a type constructor
-- f.
--
-- Although we don't use the Functor constraint, it serves
-- an important purpose: to guarantee that the type parameter a
-- doesn't appear contravariantly in f a; otherwise it'd be
-- impossible to write a Functor instance. This is used as a
-- standin for more-detailed "covariant" and "contravariant" type roles,
-- which GHC doesn't have because there's no built-in notion of subtyping
-- to use them with. Representational1 provides the actual lifting
-- of coercions, and Functor guarantees we've got the variance
-- right.
co :: (Functor f, Representational f) => Variance (f a) (f b) a b
-- | Lift an Attenuation contravariantly over a type constructor
-- f.
--
-- Regarding the Contravariant constraint, see co, and
-- interchange mentions of covariance and contravariance.
contra :: (Contravariant f, Representational f) => Variance (f b) (f a) a b
-- | Lift an Attenuation covariantly over the left of a
-- Bifunctor.
--
-- Like with co and contra, we require a not-actually-used
-- constraint as proof that the type has the appropriate variance. Since
-- there's not a commonly-used class for functors over the last-but-one
-- parameter, we use Bifunctor. Sadly, this rules out types which
-- are covariant in parameter -1 and contravariant in parameter -0.
fstco :: (Bifunctor f, Representational0 f) => Variance (f a x) (f b x) a b
-- | Lift an Attenuation covariantly over the last-but-one type
-- parameter.
--
-- Like with co and contra, we require a not-actually-used
-- constraint as proof that the type has the appropriate variance. Since
-- there's not a commonly-used class for functors over the last-but-one
-- parameter, we use Bifunctor. Sadly, this rules out types which
-- are covariant in parameter -1 and contravariant in parameter -0.
--
-- Note that any particular type with a Bifunctor f instance
-- should also have Functor (f x), so co should work on
-- any type that sndco works on, but in polymorphic contexts, the
-- Functor instance may not be available.
sndco :: (Bifunctor f, Representational1 f) => Variance (f x a) (f x b) a b
-- | Lift an Attenuation contravariantly over the argument of a
-- functiwon.
domain :: Variance (b -> x) (a -> x) a b
-- | Lift an Attenuation covariantly over the result of a function.
--
-- This is just a specialization of co.
codomain :: Variance (x -> a) (x -> b) a b
-- | Attenuation of Void to any type.
--
-- If you have Void appearing covariantly in a type, you can
-- replace it with any other lifted type with a coercion, because the
-- value can't contain any non-bottom Void values (there are
-- none), and any value that is bottom can "work" (i.e. throw or
-- fail to terminate) just as well at any other lifted type.
--
-- For example, if you have a [Doc Void] (from pretty),
-- you know it doesn't have any annotations (or they're errors), so you
-- can use it as [Doc a] without actually traversing the list
-- and Doc structure to apply absurd to all of the
-- Voids.
attVoid :: forall a. Attenuation Void a
-- | Attenuation of any type to Any.
--
-- Similarly to attVoid, you can weaken any type to Any for
-- free, since any value is a valid value of type Any.
attAny :: forall a. Attenuation a Any
-- | Attenuable a b is satisfiable iff there exists an
-- Attenuation a b.
--
-- Since an Attenuation is unique for a given pair of types (as
-- it's internally just a wrapper around a Coercible instance),
-- any way of obtaining an Attenuation gives exactly the same
-- result. This means all Attenuable instances that could
-- exist for a pair of types are also identical. In turn, this means that
-- even "incoherent" instances for Attenuable are actually
-- coherent after all: any arbitrary choice of an instance gives the same
-- result. As such, it's perfectly fine for instances of
-- Attenuable to be marked INCOHERENT, as long as it
-- results in good instance resolution behavior. This is used to provide
-- some convenient "fallback" instances filling in the (numerous) gaps in
-- the set of specific instances: specifically, automatic demotion of
-- Coercible to Attenuable; and automatic lifting of
-- Attenuable across Functors and Bifunctors.
--
-- The word "satisfiable" in the first paragraph is chosen carefully: not
-- all instances that are satisfiable will be solved automatically by
-- GHC. One can obtain Attenuable instances by \\ or by an
-- entailment (:-), for some types that wouldn't be solved by any
-- of the "real" instances. In particular, this is useful for
-- compositions of attenuations and for lifting attenuations across
-- Contravariants and Profunctors.
class Attenuable a b
attenuation :: Attenuable a b => Attenuation a b
attenuation :: (Attenuable a b, Coercible a b) => Attenuation a b
-- | An operator form of Attenuable.
type (⊆) = Attenuable
-- | Coerce from a representational subtype a to its supertype
-- b.
attenuate :: Attenuable a b => a -> b
-- | Lift an Attenuation to a constraint within a subexpression.
--
-- This is just specialization of withDict; consider using that or
-- (\\).
withAttenuation :: Attenuation a b -> (Attenuable a b => r) -> r
-- | Contravariant functors map attenuation contravariantly.
contravariance :: forall f a b. (Representational f, Contravariant f) => Attenuable a b :- Attenuable (f b) (f a)
-- | Attenuations are transitive.
transitivity :: forall b a c. (Attenuable b c, Attenuable a b) :- Attenuable a c
-- | Unsafe misuses of Attenuations' underlying Coercions.
--
-- This can allow violating the invariants of the source type, since it
-- allows casting in the opposite direction from the intended
-- Attenuation. If the Coercion is lifted to a
-- Coercible instance, this is especially bad, since it can get
-- used invisibly to allow lifted or composed coercions that shouldn't be
-- allowed. The contract defined here is that types may rely absolutely
-- on Attenuations not being used backwards in a way that violates
-- their internal invariants, including for type-safety and memory-safety
-- purposes. As such, it is unsafe to extract the Coercion
-- from an Attenuation, and any nonsense that results from doing
-- so constitutes a bug in the client code that called
-- unsafeToCoercion.
--
-- This means extreme caution must be used with the contents of this
-- module. It's always safe to use this to cast values back to their
-- original type or to any type the original type is attenuable to.
-- Otherwise, the safety of a particular backwards cast depends entirely
-- on the specific types involved.
--
-- Take care not to hold onto / leak inverted Attenuations or
-- illegitimately-obtained Coercions by accident!
module Data.Type.Attenuation.Unsafe
-- | Unsafely access the internal Coercion of an Attenuation.
unsafeToCoercion :: Attenuation a b -> Coercion a b
-- | Unsafely invert an Attenuation.
unsafeSym :: Attenuation a b -> Attenuation b a