Data.Type.Attenuation

Representational subtyping relations and variance roles.

Attenuation

data Attenuation a b

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.

Instances

Category Attenuation

Defined in Data.Type.Attenuation

Methods

id :: forall (a :: k). Attenuation a a

(.) :: forall (b :: k) (c :: k) (a :: k). Attenuation b c -> Attenuation a b -> Attenuation a c

Eq (Attenuation a b)

Defined in Data.Type.Attenuation

Methods

(==) :: Attenuation a b -> Attenuation a b -> Bool

(/=) :: Attenuation a b -> Attenuation a b -> Bool

Ord (Attenuation a b)

Defined in Data.Type.Attenuation

Methods

compare :: Attenuation a b -> Attenuation a b -> Ordering

(<) :: Attenuation a b -> Attenuation a b -> Bool

(<=) :: Attenuation a b -> Attenuation a b -> Bool

(>) :: Attenuation a b -> Attenuation a b -> Bool

(>=) :: Attenuation a b -> Attenuation a b -> Bool

max :: Attenuation a b -> Attenuation a b -> Attenuation a b

min :: Attenuation a b -> Attenuation a b -> Attenuation a b

Show (Attenuation a b)

Defined in Data.Type.Attenuation

Methods

showsPrec :: Int -> Attenuation a b -> ShowS

show :: Attenuation a b -> String

showList :: [Attenuation a b] -> ShowS

attenuate :: Attenuation a b -> a -> b

Coerce along an Attenuation.

This is really, truly a coercion when it reaches Core.

coercible :: Coercible a b => Attenuation a b

Any coercible types have an Attenuation.

trans :: Attenuation a b -> Attenuation b c -> Attenuation a c

Transitivity of Attenuations. See also the Category instance.

repr :: (a :~: b) -> Attenuation a b

Any type is unidirectionally coercible to itself.

coer :: Coercion a b -> Attenuation a b

Bidirectional coercions can be weakened to unidirectional coercions.

Representationality

type Representational f = forall a b. Coercible a b => Coercible (f a) (f b) :: Constraint

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 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 constraint that behaves like type role f _ representational.

See also Representational.

type Variance s t a b = Attenuation a b -> Attenuation s t

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.

Functor and Contravariant

co :: (Functor f, Representational f) => Variance (f a) (f b) a b

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.

contra :: (Contravariant f, Representational f) => Variance (f b) (f a) a b

Lift an Attenuation contravariantly over a type constructor f.

Regarding the Contravariant constraint, see co, and interchange mentions of covariance and contravariance.

Bifunctor

fstco :: (Bifunctor f, Representational0 f) => Variance (f a x) (f b x) 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.

sndco :: (Bifunctor f, Representational1 f) => Variance (f x a) (f x b) 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.

Profunctor

lcontra :: (Profunctor p, Representational0 p) => Variance (p b x) (p a x) 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.

rco :: (Profunctor p, Representational1 p) => Variance (p x a) (p x b) 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.

Initial and Final Objects

attVoid :: forall a. Attenuation Void a

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.

attAny :: forall a. Attenuation a Any

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.