Safe Haskell | None |
---|---|

Language | Haskell2010 |

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`

.

## Synopsis

- newtype Attenuation a b = Attenuation (Coercion a b)
- class Attenuable a b where
- attenuation :: Attenuation a b

- type Variance s t a b = Attenuation a b -> Attenuation s t
- type Representational f = forall a b. Coercible a b => Coercible (f a) (f b) :: Constraint
- type Representational0 f = forall a b x. Coercible a b => Coercible (f a x) (f b x) :: Constraint
- type Representational1 f = forall a b x. Coercible a b => Coercible (f x a) (f x b) :: Constraint
- refl :: Attenuation a a
- trans :: Attenuation a b -> Attenuation b c -> Attenuation a c
- co :: (Functor f, Representational f) => Variance (f a) (f b) a b
- fstco :: (Bifunctor f, Representational0 f) => Variance (f a x) (f b x) a b
- sndco :: (Bifunctor f, Representational1 f) => Variance (f x a) (f x b) a b
- domain :: Variance (b -> x) (a -> x) a b
- codomain :: Variance (x -> a) (x -> b) a b
- rep :: Representational f => Coercion a b -> Coercion (f a) (f b)
- rep0 :: Representational0 f => Coercion a b -> Coercion (f a x) (f b x)
- withAttenuation :: Attenuation a b -> (Attenuable a b => r) -> r

# Documentation

newtype Attenuation a b Source #

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

`Fin`

s to `Int`

s, and `Fin`

s to other `Fin`

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

Attenuation (Coercion a b) |

#### Instances

class Attenuable a b where Source #

`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 `Functor`

s and `Bifunctor`

s.

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
`Contravariant`

s and `Profunctor`

s.

Nothing

attenuation :: Attenuation a b Source #

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

#### Instances

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

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
`Attenuation`

s through several `Functor`

s by

.`co`

.co.co $ x

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

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 Source #

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 Source #

A constraint that behaves like `type role f _ representational`

.

See also `Representational`

.

refl :: Attenuation a a Source #

Any type is unidirectionally-coercible to itself.

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

Transitivity of `Attenuation`

s. See also the `Category`

instance.

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

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 Source #

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 Source #

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 Source #

Lift an `Attenuation`

contravariantly over the argument of a functiwon.

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

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) Source #

Lift a `Coercion`

over a type constructor.

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

Lift a `Coercion`

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

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

Lift an `Attenuation`

to a constraint within a subexpression.

This is just specialization of `withDict`

; consider using
that or (`\\`

).