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.

Instances

Category (Attenuation :: k -> k -> Type)

Defined in Data.Type.Attenuation.Internal

Methods

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

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

Eq (Attenuation a b)

Defined in Data.Type.Attenuation.Internal

Methods

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

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

Ord (Attenuation a b)

Defined in Data.Type.Attenuation.Internal

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.Internal

Methods

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

show :: Attenuation a b -> String

showList :: [Attenuation a b] -> ShowS

HasDict (Attenuable a b) (Attenuation a b)

Defined in Data.Type.Attenuation.Internal

Methods

evidence :: Attenuation a b -> Dict (Attenuable a b)

type (:⊆:) = Attenuation

An operator form of Attenuation, by analogy to (:~:).

attenuateWith :: 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.

iso :: Attenuation a b -> Attenuation b a -> Coercion a b

If Attenuations in both directions exist, they're actually a Coercion.

inst :: Attenuation f g -> Attenuation (f x) (g x)

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.

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.

(->)

domain :: Variance (b -> x) (a -> x) a b

Lift an Attenuation contravariantly over the argument of a functiwon.

codomain :: Variance (x -> a) (x -> b) a b

Lift an Attenuation covariantly over the result of a function.

This is just a specialization of co.

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.

Attenuable

class Attenuable a b where

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.

Minimal complete definition

Nothing

Methods

attenuation :: Attenuation a b

default attenuation :: Coercible a b => Attenuation a b

Instances

Attenuable (a :: Type) (a :: Type)

Defined in Data.Type.Attenuation.Internal

Methods

attenuation :: Attenuation a a

Coercible a b => Attenuable (a :: k) (b :: k)

Defined in Data.Type.Attenuation.Internal

Methods

attenuation :: Attenuation a b

(Functor f, Representational f, Attenuable x y) => Attenuable (f x :: Type) (f y :: Type)

Defined in Data.Type.Attenuation.Internal

Methods

attenuation :: Attenuation (f x) (f y)

(Attenuable c a, Attenuable b d) => Attenuable (a -> b :: Type) (c -> d :: Type)

Defined in Data.Type.Attenuation.Internal

Methods

attenuation :: Attenuation (a -> b) (c -> d)

(Attenuable a a', Attenuable b b') => Attenuable ((a, b) :: Type) ((a', b') :: Type)

Defined in Data.Type.Attenuation.Internal

Methods

attenuation :: Attenuation (a, b) (a', b')

(Bifunctor f, Representational0 f, Representational1 f, Attenuable a c, Attenuable b d) => Attenuable (f a b :: Type) (f c d :: Type)

Defined in Data.Type.Attenuation.Internal

Methods

attenuation :: Attenuation (f a b) (f c d)

(Attenuable a a', Attenuable b b', Attenuable c c') => Attenuable ((a, b, c) :: Type) ((a', b', c') :: Type)

Defined in Data.Type.Attenuation.Internal

Methods

attenuation :: Attenuation (a, b, c) (a', b', c')

HasDict (Attenuable a b) (Attenuation a b)

Defined in Data.Type.Attenuation.Internal

Methods

evidence :: Attenuation a b -> Dict (Attenuable a b)

type (⊆) = Attenuable

An operator form of Attenuable.

attenuate :: Attenuable a b => a -> b

Coerce from a representational subtype a to its supertype b.

withAttenuation :: Attenuation a b -> (Attenuable a b => r) -> r

Lift an Attenuation to a constraint within a subexpression.

This is just specialization of withDict; consider using that or (\\).

Entailments

contravariance :: forall f a b. (Representational f, Contravariant f) => Attenuable a b :- Attenuable (f b) (f a)

Contravariant functors map attenuation contravariantly.

transitivity :: forall b a c. (Attenuable b c, Attenuable a b) :- Attenuable a c

Attenuations are transitive.