Last active
January 5, 2025 10:15
-
-
Save LSLeary/b044a619337007877366f9faca38947d to your computer and use it in GitHub Desktop.
Generalised Coercible
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- These coercions could probably be generated automatically with a | |
-- type class and this plugin: | |
-- https://github.com/noughtmare/transitive-constraint-plugin | |
{-# LANGUAGE UnboxedTuples, UnliftedNewtypes, ExplicitNamespaces #-} | |
{-# LANGUAGE RoleAnnotations, DataKinds, QuantifiedConstraints #-} | |
module Coercible ( | |
Coercible(..), | |
type (~~>), | |
refl, (~), symm, | |
Repr, | |
Positive, pos, | |
Negative, neg, | |
-- Extension | |
Coercion(..), | |
useCo, | |
-- User-space Utils / Examples | |
sub, contrasub, | |
Repr2, bisub, | |
) where | |
-- base | |
import GHC.Exts (TYPE, ZeroBitType, LiftedRep, UnliftedRep) | |
import Unsafe.Coerce (unsafeCoerce, unsafeCoerceUnlifted) | |
import Data.Kind (Type, Constraint) | |
import Data.Coerce qualified as Symm | |
import Data.Functor.Contravariant (Contravariant(..)) | |
import Data.Bifunctor (Bifunctor(..)) | |
class Coercible rr where | |
coerce :: forall (a :: TYPE rr) (b :: TYPE rr). a ~~> b -> a -> b | |
-- Further instances to be written at need. | |
instance Coercible LiftedRep where coerce !_ = unsafeCoerce | |
instance Coercible UnliftedRep where coerce !_ = unsafeCoerceUnlifted | |
type role (~~>) nominal nominal | |
type (~~>) :: k -> k -> ZeroBitType | |
newtype a ~~> b = UnsafeCoercion (# #) | |
refl :: forall {k} (a :: k). (# #) -> a ~~> a | |
refl = UnsafeCoercion | |
(~) :: forall {k} (a :: k) (b :: k) (c :: k). a ~~> b -> b ~~> c -> a ~~> c | |
!_ ~ !_ = UnsafeCoercion (# #) | |
symm :: forall {k} (a :: k) (b :: k). Symm.Coercible a b => a ~~> b | |
symm = UnsafeCoercion (# #) | |
type Repr :: (k1 -> k2) -> Constraint | |
type Repr f = forall a b. Symm.Coercible a b => Symm.Coercible (f a) (f b) | |
type HO k = forall rr1 rr2. (TYPE rr1 -> TYPE rr2) -> k | |
type Positive :: HO Type | |
type Positive f = forall a b. (a -> b) -> f a -> f b | |
-- `Positive f` means that the symmetric coercion `Repr f` depends upon is | |
-- only used /forwards/, so we can safely substitute a forward coercion. | |
pos | |
:: forall {rr1} {rr2} a b (f :: TYPE rr1 -> TYPE rr2) | |
. Repr f => Positive f -> a ~~> b -> f a ~~> f b | |
pos !_ !_ = UnsafeCoercion (# #) | |
type Negative :: HO Type | |
type Negative f = forall a b. (b -> a) -> f a -> f b | |
-- `Negative f` means that the symmetric coercion `Repr f` depends upon is | |
-- only used /backwards/, so we can safely substitute a backward coercion. | |
neg | |
:: forall {rr1} {rr2} a b (f :: TYPE rr1 -> TYPE rr2) | |
. Repr f => Negative f -> b ~~> a -> f a ~~> f b | |
neg !_ !_ = UnsafeCoercion (# #) | |
{-# WARNING in "x-not-for-direct-use" co "Use via `coerce` and `useCo`." #-} | |
-- | A type class for user declared coercions. | |
-- Law: @a@ and @b@ have the same runtime representation. | |
type Coercion :: TYPE rr -> TYPE rr -> Constraint | |
class Coercion a b where | |
co :: a -> b | |
useCo :: forall {rr} (a :: TYPE rr) (b :: TYPE rr). Coercion a b => a ~~> b | |
useCo = UnsafeCoercion (# #) | |
-- `pos` and `neg` may look limited, but they really go a long way. | |
-- Here we implement `sub`, `contrasub` and `bisub` safely in user-space. | |
-- The `Profunctor` equivalent would be the same as `bisub`, but using `neg` | |
-- and `lmap` in place of `pos` and `first`. | |
sub :: (Repr f, Functor f) => a ~~> b -> f a ~~> f b | |
sub = pos fmap | |
contrasub :: (Repr f, Contravariant f) => b ~~> a -> f a ~~> f b | |
contrasub = neg contramap | |
type Repr2 :: (k1 -> k2 -> k3) -> Constraint | |
type Repr2 p | |
= forall a b c d | |
. (Symm.Coercible a c, Symm.Coercible b d) | |
=> Symm.Coercible (p a b) (p c d) | |
newtype Flip p a b = Flip{ unFlip :: p b a } | |
bisub | |
:: forall p a b c d | |
. (Repr2 p, Bifunctor p) | |
=> a ~~> c -> b ~~> d -> p a b ~~> p c d | |
bisub ac bd | |
= symm @(p a b) @(Flip p b a) | |
~ pos (\f -> Flip . first f . unFlip) ac | |
~ symm @(Flip p b c) @(p c b) | |
~ sub bd |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment