lol.hs

import Data.Coerce
import Data.Functor.Compose
import Data.Functor.Identity
import Data.Kind

--------------------------------------------------------------------------------

data Iso p a b = Iso {fwd :: p a b, bwd :: p b a}

type FCoercible :: (k -> Type) -> Constraint
type FCoercible f = forall a b. Coercible a b => Coercible (f a) (f b)

type BCoercible :: HKD k -> Constraint
type BCoercible k = forall f g. (FCoercible f, FCoercible g) => Coercible (k f) (k g)

coercible :: Coercible a b => Iso (->) a b
coercible = Iso {fwd = coerce, bwd = coerce}

--------------------------------------------------------------------------------

type HKD k = (k -> *) -> *

type BPure :: k -> HKD k
newtype BPure a cb = BPure {unBPure :: cb a}

type BJoin :: HKD (HKD k) -> HKD k
newtype BJoin kka cb = BJoin {unBJoin :: kka (BPure cb)}

type BFMap :: (a -> b) -> HKD a -> HKD b
newtype BFMap ab ka cb = BFMap {unBFMap :: ka (Compose cb ab)}

type BFFMap :: HKD a -> (a -> b) -> HKD b
newtype BFFMap ka ab cb = BFFMap {unBFFMap :: BFMap ab ka cb}

type BBind :: (a -> HKD b) -> HKD a -> HKD b
type BBind f k = BJoin (BFMap f k)

type BLift2 :: (a -> b -> c) -> HKD a -> HKD b -> HKD c
newtype BLift2 f kba kbb cb = BLift2 {unBLift2 :: BBind (BFFMap kbb) (BFMap f kba) cb}

type BProd :: HKD Type -> HKD Type -> HKD Type
type BProd = BLift2 (,)

type BSum :: HKD Type -> HKD Type -> HKD Type
type BSum = BLift2 Either

--------------------------------------------------------------------------------

-- Left unit law
type LUnit1 :: HKD a -> HKD a
newtype LUnit1 k cb = LUnit1 {unLUnit1 :: BJoin (BPure k) cb}

type LUnit2 :: HKD a -> HKD a
newtype LUnit2 k cb = LUnit2 {unLUnit2 :: k cb}

lunit :: Iso (->) (LUnit1 k cb) (LUnit2 k cb)
lunit = coercible

--------------------------------------------------------------------------------

-- Right unit law
type RUnit1 :: HKD Type -> HKD Type
newtype RUnit1 k cb = RUnit1 {unRUnit1 :: BJoin (BFMap BPure k) cb}

type RUnit2 :: HKD Type -> HKD Type
newtype RUnit2 k cb = RUnit2 {unRUnit2 :: k cb}

runit :: (FCoercible cb, BCoercible k) => Iso (->) (RUnit1 k cb) (RUnit2 k cb)
runit = coercible

--------------------------------------------------------------------------------

-- Associativity law
type Assoc1 :: HKD (HKD (HKD a)) -> HKD a
newtype Assoc1 k cb = Assoc1 {unAssoc1 :: BJoin (BJoin k) cb}

type Assoc2 :: HKD (HKD (HKD a)) -> HKD a
newtype Assoc2 k cb = Assoc2 {unAssoc2 :: BJoin (BFMap BJoin k) cb}

assoc :: (FCoercible cb, BCoercible k) => Iso (->) (Assoc1 k cb) (Assoc2 k cb)
assoc = coercible

--------------------------------------------------------------------------------

test :: (BPure Int `BProd` BPure String `BProd` BPure Bool) Identity
test
  = BLift2
  $ BJoin
  $ BFMap
  $ BFMap
  $ BLift2
  $ BJoin
  $ BFMap
  $ BFMap
  $ BPure
  $ Compose
  $ Compose
  $ BPure
  $ BFFMap
  $ BFMap
  $ BPure
  $ Compose
  $ Compose
  $ Compose
  $ BPure
  $ BFFMap
  $ BFMap
  $ BPure
  $ Compose
  $ Identity
  $ ((42, "foo"), False)

What is your Iso for? All your isos are defined as coercible, so I think it'd be nicer to say

import Data.Type.Coercion (Coercion (..))
lunit :: Coercion (LUnit1 k cb) (LUnit2 k cb)
lunit = Coercion
runit :: (FCoercible cb, BCoercible k) => Coercion (RUnit1 k cb) (RUnit2 k cb)
runit = Coercion
assoc :: (FCoercible cb, BCoercible k) => Coercion (Assoc1 k cb) (Assoc2 k cb)
assoc = Coercion

Users could write coerceWith assoc or coerceWith (sym assoc), for example, to "extract" the two sides of the isomorphism, but they can also gcoerceWith or pattern match on it to get more.

What is your Iso for?

Iso is for representing isomorphisms (in this case bijections), which are the notion of sameness up to which we expect the monad laws to hold in this context.

All your isos are defined as coercible

It's true that all of these isos are defined using coercible. It's not true in general that all isos of this form arise from a coercion.

so I think it'd be nicer to say ...

You are of course welcome to your opinion, but I don't share it.