Safe Haskell | None |
---|---|
Language | Haskell2010 |
Representational subtyping relations and variance roles.
Synopsis
- data Attenuation a b
- attenuate :: 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
- 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
- lcontra :: (Profunctor p, Representational0 p) => Variance (p b x) (p a x) a b
- rco :: (Profunctor p, Representational1 p) => Variance (p x a) (p x b) a b
- attVoid :: forall a. Attenuation Void a
- attAny :: forall a. Attenuation a Any
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. 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
attenuate :: 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.
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.
Profunctor
lcontra :: (Profunctor p, Representational0 p) => Variance (p b x) (p a x) a b Source #
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 Source #
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 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
.