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

Language | Haskell2010 |

Representational subtyping relations and variance roles.

## Synopsis

- data Attenuation a b
- type (:⊆:) = Attenuation
- attenuateWith :: Attenuation a b -> a -> b
- coercible :: Coercible a b => Attenuation a b
- trans :: Attenuation a b -> Attenuation b c -> Attenuation a c
- repr :: (a :~: b) -> Attenuation a b
- coer :: Coercion a b -> Attenuation a b
- iso :: Attenuation a b -> Attenuation b a -> Coercion a b
- inst :: Attenuation f g -> Attenuation (f x) (g x)
- 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
- type Variance s t a b = Attenuation a b -> Attenuation s t
- co :: (Functor f, Representational f) => Variance (f a) (f b) a b
- contra :: (Contravariant f, Representational f) => Variance (f b) (f a) 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
- attVoid :: forall a. Attenuation Void a
- attAny :: forall a. Attenuation a Any
- class Attenuable a b where
- attenuation :: Attenuation a b

- type (⊆) = Attenuable
- attenuate :: Attenuable a b => a -> b
- withAttenuation :: Attenuation a b -> (Attenuable a b => r) -> r
- contravariance :: forall f a b. (Representational f, Contravariant f) => Attenuable a b :- Attenuable (f b) (f a)
- transitivity :: forall b a c. (Attenuable b c, Attenuable a b) :- Attenuable a c

# Attenuation

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

#### Instances

type (:⊆:) = Attenuation Source #

An operator form of `Attenuation`

, by analogy to (`:~:`

).

attenuateWith :: Attenuation a b -> a -> b Source #

Coerce along an `Attenuation`

.

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

coercible :: Coercible a b => Attenuation a b Source #

Any coercible types have an `Attenuation`

.

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

Transitivity of `Attenuation`

s. See also the `Category`

instance.

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

Any type is unidirectionally coercible to itself.

coer :: Coercion a b -> Attenuation a b Source #

Bidirectional coercions can be weakened to unidirectional coercions.

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

If `Attenuation`

s in both directions exist, they're actually a `Coercion`

.

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

`Attenuation`

s across type constructors can be instantiated.

This means `Attenuation`

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

.

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

## Functor and Contravariant

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.

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

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

.

## Initial and Final Objects

attVoid :: forall a. Attenuation Void a Source #

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

s.

attAny :: forall a. Attenuation a Any Source #

`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 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 (⊆) = Attenuable Source #

An operator form of `Attenuable`

.

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

Coerce from a representational subtype `a`

to its supertype `b`

.

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

).

## Entailments

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

`Contravariant`

functors map attenuation contravariantly.

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

`Attenuation`

s are transitive.