-- 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.1.0.0 -- | 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. Note, however, that we can't have a useful -- typeclass of this subtyping relation because all of its instances -- would have to be specified individually: whereas Coercible is -- willing to invert or compose coercions implicitly because of GHC -- magic, a subtyping class would not have that affordance. data Attenuation a b -- | Coerce along an Attenuation. -- -- This is really, truly a coercion when it reaches Core. attenuate :: 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 -- | 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 covariantly over the left of a -- Profunctor. -- -- Similarly to the use of Functor in co, we use -- Profunctor to guarantee contravariance in the appropriate -- parameter. lcontra :: (Profunctor p, Representational0 p) => Variance (p b x) (p a x) a b -- | Lift an Attenuation covariantly over the right of a -- Profunctor. -- -- Similarly to the use of Functor in co, we use -- Profunctor to guarantee contravariance in the appropriate -- parameter. -- -- As with sndco, this functions the same as co, but the -- needed Functor instance might not be available in polymorphic -- contexts. rco :: (Profunctor p, Representational1 p) => Variance (p x a) (p 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 instance GHC.Show.Show (Data.Type.Attenuation.Attenuation a b) instance GHC.Classes.Ord (Data.Type.Attenuation.Attenuation a b) instance GHC.Classes.Eq (Data.Type.Attenuation.Attenuation a b) instance Control.Category.Category Data.Type.Attenuation.Attenuation