{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_HADDOCK show-extensions #-}

-- | Module    :  IsomorphismClass.Extra
-- Copyright   :  (C) 2023 Alexey Tochin
-- License     :  BSD3 (see the file LICENSE)
-- Maintainer  :  Alexey Tochin <Alexey.Tochin@gmail.com>
--
-- Extra instances for 'IsomorphicTo' typeclass from 'isomorphism-class' package.
module IsomorphismClass.Extra () where

import Control.Category (id)
import Data.Void (Void, absurd)
import IsomorphismClass (IsomorphicTo, to)
import Prelude (Either (Left, Right), fst, snd)

instance {-# INCOHERENT #-} IsomorphicTo a a where
  to :: a -> a
to = forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

-- Type products

instance {-# INCOHERENT #-} IsomorphicTo a (a, ()) where
  to :: (a, ()) -> a
to = forall a b. (a, b) -> a
fst

instance {-# INCOHERENT #-} IsomorphicTo (a, ()) a where
  to :: a -> (a, ())
to = (,())

instance {-# INCOHERENT #-} IsomorphicTo a ((), a) where
  to :: ((), a) -> a
to = forall a b. (a, b) -> b
snd

instance {-# INCOHERENT #-} IsomorphicTo ((), a) a where
  to :: a -> ((), a)
to = ((),)

-- | Type product commutativity
--
-- ==== __Examples of usage__
--
-- >>> import IsomorphismClass.Isomorphism (iso)
-- >>> (iso :: (->) (a, b) (b, a)) (1, "x")
-- ("x",1)
instance {-# INCOHERENT #-} IsomorphicTo (a, b) (b, a) where
  to :: (b, a) -> (a, b)
to (b
b, a
a) = (a
a, b
b)

instance {-# INCOHERENT #-} IsomorphicTo (a, (b, c)) ((a, b), c) where
  to :: ((a, b), c) -> (a, (b, c))
to ((a
a, b
b), c
c) = (a
a, (b
b, c
c))

instance {-# INCOHERENT #-} IsomorphicTo ((a, b), c) (a, (b, c)) where
  to :: (a, (b, c)) -> ((a, b), c)
to (a
a, (b
b, c
c)) = ((a
a, b
b), c
c)

instance {-# INCOHERENT #-} IsomorphicTo ((a, b), (c, d)) ((a, c), (b, d)) where
  to :: ((a, c), (b, d)) -> ((a, b), (c, d))
to ((a
a, c
c), (b
b, d
d)) = ((a
a, b
b), (c
c, d
d))

-- instance {-# INCOHERENT #-} IsomorphicTo (a, (b, (c, d))) (a, ((c, d), b)) where
--  to (a, ((c, d), b)) = (a, (b, (c, d)))
--
-- instance {-# INCOHERENT #-} IsomorphicTo (a, ((c, d), b)) (a, (b, (c, d))) where
--  to (a, (b, (c, d))) = (a, ((c, d), b))

-- Type sums

instance {-# INCOHERENT #-} IsomorphicTo a (Either a Void) where
  to :: Either a Void -> a
to (Left a
a) = a
a
  to (Right Void
a) = forall a. Void -> a
absurd Void
a

instance {-# INCOHERENT #-} IsomorphicTo (Either a Void) a where
  to :: a -> Either a Void
to = forall a b. a -> Either a b
Left

-- | Type sum commutativity.
--
-- ==== __Examples of usage__
--
-- >>> import IsomorphismClass.Isomorphism (iso)
-- >>> (iso :: (->) (Either a b) (Either b a)) (Left 1)
-- Right 1
-- >>> (iso :: (->) (Either a b) (Either b a)) (Right "x")
-- Left "x"
instance {-# INCOHERENT #-} IsomorphicTo a (Either Void a) where
  to :: Either Void a -> a
to (Right a
a) = a
a
  to (Left Void
a) = forall a. Void -> a
absurd Void
a

instance {-# INCOHERENT #-} IsomorphicTo (Either Void a) a where
  to :: a -> Either Void a
to = forall a b. b -> Either a b
Right

instance {-# INCOHERENT #-} IsomorphicTo (Either a b) (Either b a) where
  to :: Either b a -> Either a b
to (Left b
b) = forall a b. b -> Either a b
Right b
b
  to (Right a
b) = forall a b. a -> Either a b
Left a
b

instance {-# INCOHERENT #-} IsomorphicTo (Either a (Either b c)) (Either (Either a b) c) where
  to :: Either (Either a b) c -> Either a (Either b c)
to (Left (Left a
a)) = forall a b. a -> Either a b
Left a
a
  to (Left (Right b
b)) = forall a b. b -> Either a b
Right (forall a b. a -> Either a b
Left b
b)
  to (Right c
c) = forall a b. b -> Either a b
Right (forall a b. b -> Either a b
Right c
c)

instance {-# INCOHERENT #-} IsomorphicTo (Either (Either a b) c) (Either a (Either b c)) where
  to :: Either a (Either b c) -> Either (Either a b) c
to (Left a
a) = forall a b. a -> Either a b
Left (forall a b. a -> Either a b
Left a
a)
  to (Right (Left b
b)) = forall a b. a -> Either a b
Left (forall a b. b -> Either a b
Right b
b)
  to (Right (Right c
c)) = forall a b. b -> Either a b
Right c
c

instance {-# INCOHERENT #-} IsomorphicTo (Either (Either a b) (Either c d)) (Either (Either a c) (Either b d)) where
  to :: Either (Either a c) (Either b d)
-> Either (Either a b) (Either c d)
to (Left (Left a
a)) = forall a b. a -> Either a b
Left (forall a b. a -> Either a b
Left a
a)
  to (Left (Right c
c)) = forall a b. b -> Either a b
Right (forall a b. a -> Either a b
Left c
c)
  to (Right (Left b
b)) = forall a b. a -> Either a b
Left (forall a b. b -> Either a b
Right b
b)
  to (Right (Right d
d)) = forall a b. b -> Either a b
Right (forall a b. b -> Either a b
Right d
d)

-- instance {-# INCOHERENT #-} IsomorphicTo (Either a (Either b (Either c d))) (Either a (Either (Either c d) b)) where
--  to (Left a) = Left a
--  to (Right (Left b)) = Right (Right b)
--  to (Right (Right (Left c))) =   Right
--
--
--  to (a, ((c, d), b)) = (a, (b, (c, d)))
--
-- instance {-# INCOHERENT #-} IsomorphicTo (Either a (Either (Either c d) b)) (Either a (Either b (Either c d))) where
--  to (a, (b, (c, d))) = (a, ((c, d), b))