Data.Type.Attenuation.Internal

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.

Documentation

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

Constructors

Attenuation (Coercion a b)

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)

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

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.

refl :: Attenuation a a

Any type is unidirectionally-coercible to itself.

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

Transitivity of Attenuations. See also the Category instance.

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.

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.

rep :: Representational f => Coercion a b -> Coercion (f a) (f b)

Lift a Coercion over a type constructor.

rep0 :: Representational0 f => Coercion a b -> Coercion (f a x) (f b x)

Lift a Coercion over the last-but-one parameter of a type constructor.

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 (\\).