{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_HADDOCK show-extensions #-}
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 = a -> a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
instance {-# INCOHERENT #-} IsomorphicTo a (a, ()) where
to :: (a, ()) -> a
to = (a, ()) -> a
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 = ((), a) -> a
forall a b. (a, b) -> b
snd
instance {-# INCOHERENT #-} IsomorphicTo ((), a) a where
to :: a -> ((), a)
to = ((),)
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 (Either a Void) where
to :: Either a Void -> a
to (Left a
a) = a
a
to (Right Void
a) = Void -> a
forall a. Void -> a
absurd Void
a
instance {-# INCOHERENT #-} IsomorphicTo (Either a Void) a where
to :: a -> Either a Void
to = a -> Either a Void
forall a b. a -> Either a b
Left
instance {-# INCOHERENT #-} IsomorphicTo a (Either Void a) where
to :: Either Void a -> a
to (Right a
a) = a
a
to (Left Void
a) = Void -> a
forall a. Void -> a
absurd Void
a
instance {-# INCOHERENT #-} IsomorphicTo (Either Void a) a where
to :: a -> Either Void a
to = a -> Either Void a
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) = b -> Either a b
forall a b. b -> Either a b
Right b
b
to (Right a
b) = a -> Either 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)) = a -> Either a (Either b c)
forall a b. a -> Either a b
Left a
a
to (Left (Right b
b)) = Either b c -> Either a (Either b c)
forall a b. b -> Either a b
Right (b -> Either b c
forall a b. a -> Either a b
Left b
b)
to (Right c
c) = Either b c -> Either a (Either b c)
forall a b. b -> Either a b
Right (c -> Either b c
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) = Either a b -> Either (Either a b) c
forall a b. a -> Either a b
Left (a -> Either a b
forall a b. a -> Either a b
Left a
a)
to (Right (Left b
b)) = Either a b -> Either (Either a b) c
forall a b. a -> Either a b
Left (b -> Either a b
forall a b. b -> Either a b
Right b
b)
to (Right (Right c
c)) = c -> Either (Either a b) 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)) = Either a b -> Either (Either a b) (Either c d)
forall a b. a -> Either a b
Left (a -> Either a b
forall a b. a -> Either a b
Left a
a)
to (Left (Right c
c)) = Either c d -> Either (Either a b) (Either c d)
forall a b. b -> Either a b
Right (c -> Either c d
forall a b. a -> Either a b
Left c
c)
to (Right (Left b
b)) = Either a b -> Either (Either a b) (Either c d)
forall a b. a -> Either a b
Left (b -> Either a b
forall a b. b -> Either a b
Right b
b)
to (Right (Right d
d)) = Either c d -> Either (Either a b) (Either c d)
forall a b. b -> Either a b
Right (d -> Either c d
forall a b. b -> Either a b
Right d
d)