Skip to content

Instantly share code, notes, and snippets.

@LSLeary
Last active January 5, 2025 10:15
Show Gist options
  • Save LSLeary/b044a619337007877366f9faca38947d to your computer and use it in GitHub Desktop.
Save LSLeary/b044a619337007877366f9faca38947d to your computer and use it in GitHub Desktop.
Generalised Coercible
-- 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