{-# LANGUAGE CPP               #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE Trustworthy       #-}
{-# LANGUAGE TypeOperators     #-}
#if __GLASGOW_HASKELL >= 708
{-# LANGUAGE EmptyCase         #-}
#endif
-- | 'Boring' and 'Absurd' classes. One approach.
--
-- Different approach would be to have
--
-- @
-- -- none-one-tons semiring
-- data NOT = None | One | Tons
--
-- type family Cardinality (a :: *) :: NOT
--
-- class Cardinality a ~ None => Absurd a where ...
-- class Cardinality a ~ One  => Boring a where ...
-- @
--
-- This would make possible to define more instances, e.g.
--
-- @
-- instance (Mult (Cardinality a) (Cardinality b) ~ None) => Absurd (a, b) where ...
-- @
--
-- === Functions
--
-- Function is an exponential:
--
-- @
-- Cardinality (a -> b) ~ Exponent (Cardinality b) (Cardinality a)
-- @
--
-- or shortly @|a -> b| = |b| ^ |a|@. This gives us possible instances:
--
-- * @|a| = 0 => |a -> b| = m ^ 0 = 1@, i.e. @'Absurd' a => 'Boring' (a -> b)@, or
--
-- * @|b| = 1 => |a -> b| = 1 ^ n = 1@, i.e. @'Boring' b => 'Boring' (a -> b)@.
--
-- Both instances are 'Boring', but we chose to define the latter.
--
-- === Note about adding instances
--
-- At this moment this module misses a lot of instances,
-- please make a patch to add more. Especially, if the package is already
-- in the transitive dependency closure.
--
-- E.g. any possibly empty container @f@ has @'Absurd' a => 'Boring' (f a)@
--
module Data.Boring (
    -- * Classes
    Boring (..),
    Absurd (..),
    -- ** Generic implementation
    GBoring,
    GAbsurd,
    -- * More interesting stuff
    vacuous,
    devoid,
    united,
) where

import Prelude (Either (..), Functor (..), Maybe (..), const, (.))

import Control.Applicative   (Const (..), (<$))
import Data.Functor.Compose  (Compose (..))
import Data.Functor.Identity (Identity (..))
import Data.Functor.Product  (Product (..))
import Data.Functor.Sum      (Sum (..))
import Data.List.NonEmpty    (NonEmpty (..))
import Data.Proxy            (Proxy (..))
import GHC.Generics
       (Generic (..), K1 (..), M1 (..), Par1 (..), Rec1 (..), U1 (..), V1,
       (:*:) (..), (:+:) (..), (:.:) (..))

import qualified Data.Void as V

#if __GLASGOW_HASKELL >= 708
import qualified Data.Coerce        as Co
import qualified Data.Type.Coercion as Co
#else
import Prelude (seq, error)
#endif

import qualified Data.Type.Equality as Eq

#if MIN_VERSION_base(4,10,0)
import qualified Type.Reflection as Typeable
#endif

#if MIN_VERSION_base(4,18,0)
import qualified GHC.TypeLits as TypeLits
import qualified GHC.TypeNats as TypeNats
#endif

#ifdef MIN_VERSION_tagged
import Data.Tagged (Tagged (..))
#endif

-- $setup
-- >>> :set -XDeriveGeneric
-- >>> import GHC.Generics (Generic)

-------------------------------------------------------------------------------
-- Boring
-------------------------------------------------------------------------------

-- | 'Boring' types which contains one thing, also
-- 'boring'. There is nothing interesting to be gained by
-- comparing one element of the boring type with another,
-- because there is nothing to learn about an element of the
-- boring type by giving it any of your attention.
--
-- /Boring Law:/
--
-- @
-- 'boring' == x
-- @
--
-- /Note:/ This is different class from @Default@.
-- @Default@ gives you /some/ value,
-- @Boring@ gives you an unique value.
--
-- Also note, that we cannot have instances for e.g.
-- 'Either', as both
-- @('Boring' a, 'Absurd' b) => Either a b@ and
-- @('Absurd' a, 'Boring' b) => Either a b@ would be valid instances.
--
-- Another useful trick, is that you can rewrite computations with
-- 'Boring' results, for example @foo :: Int -> ()@, __if__ you are sure
-- that @foo@ is __total__.
--
-- > {-# RULES "less expensive" foo = boring #-}
--
-- That's particularly useful with equality ':~:' proofs.
--
class Boring a where
    boring :: a
    default boring :: (Generic a, GBoring (Rep a)) => a
    boring = forall a x. Generic a => Rep a x -> a
to forall (f :: * -> *) a. GBoring f => f a
gboring

instance Boring () where
    boring :: ()
boring = ()

instance Boring b => Boring (a -> b) where
    boring :: a -> b
boring = forall a b. a -> b -> a
const forall a. Boring a => a
boring

instance Boring (Proxy a) where
    boring :: Proxy a
boring = forall {k} (t :: k). Proxy t
Proxy

instance Boring a => Boring (Const a b) where
    boring :: Const a b
boring = forall {k} a (b :: k). a -> Const a b
Const forall a. Boring a => a
boring

#ifdef MIN_VERSION_tagged
instance Boring b => Boring (Tagged a b) where
    boring :: Tagged a b
boring = forall {k} (s :: k) b. b -> Tagged s b
Tagged forall a. Boring a => a
boring
#endif

instance Boring a => Boring (Identity a) where
    boring :: Identity a
boring = forall a. a -> Identity a
Identity forall a. Boring a => a
boring

instance Boring (f (g a)) => Boring (Compose f g a) where
    boring :: Compose f g a
boring = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall a. Boring a => a
boring

instance (Boring (f a), Boring (g a)) => Boring (Product f g a) where
    boring :: Product f g a
boring = forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall a. Boring a => a
boring forall a. Boring a => a
boring

instance (Boring a, Boring b) => Boring (a, b) where
    boring :: (a, b)
boring = (forall a. Boring a => a
boring, forall a. Boring a => a
boring)

instance (Boring a, Boring b, Boring c) => Boring (a, b, c) where
    boring :: (a, b, c)
boring = (forall a. Boring a => a
boring, forall a. Boring a => a
boring, forall a. Boring a => a
boring)

instance (Boring a, Boring b, Boring c, Boring d) => Boring (a, b, c, d) where
    boring :: (a, b, c, d)
boring = (forall a. Boring a => a
boring, forall a. Boring a => a
boring, forall a. Boring a => a
boring, forall a. Boring a => a
boring)

instance (Boring a, Boring b, Boring c, Boring d, Boring e) => Boring (a, b, c, d, e) where
    boring :: (a, b, c, d, e)
boring = (forall a. Boring a => a
boring, forall a. Boring a => a
boring, forall a. Boring a => a
boring, forall a. Boring a => a
boring, forall a. Boring a => a
boring)

-- | Recall regular expressions, kleene star of empty regexp is epsilon!
instance Absurd a => Boring [a] where
    boring :: [a]
boring = []

-- | @'Maybe' a = a + 1@, @0 + 1 = 1@.
instance Absurd a => Boring (Maybe a) where
    boring :: Maybe a
boring = forall a. Maybe a
Nothing

#if __GLASGOW_HASKELL >= 708
-- | Coercibility is 'Boring' too.
instance Co.Coercible a b => Boring (Co.Coercion a b) where
    boring = Co.Coercion
#endif

-- | Homogeneous type equality is 'Boring' too.
instance a ~ b => Boring (a Eq.:~: b) where
    boring :: a :~: b
boring = forall {k} (a :: k). a :~: a
Eq.Refl

# if MIN_VERSION_base(4,10,0)
-- | Heterogeneous type equality is 'Boring' too.
instance a Eq.~~ b => Boring (a Eq.:~~: b) where
    boring :: a :~~: b
boring = forall {k1} (a :: k1). a :~~: a
Eq.HRefl
# endif

#if MIN_VERSION_base(4,10,0)
instance Typeable.Typeable a => Boring (Typeable.TypeRep a) where
    boring :: TypeRep a
boring = forall {k} (a :: k). Typeable a => TypeRep a
Typeable.typeRep
#endif

#if MIN_VERSION_base(4,18,0)
instance TypeLits.KnownChar n => Boring (TypeLits.SChar n) where
    boring = TypeLits.charSing

instance TypeLits.KnownSymbol n => Boring (TypeLits.SSymbol n) where
    boring = TypeLits.symbolSing

instance TypeNats.KnownNat n => Boring (TypeNats.SNat n) where
    boring = TypeNats.natSing
#endif

-------------------------------------------------------------------------------
-- Generics
-------------------------------------------------------------------------------

instance Boring (U1 p) where
    boring :: U1 p
boring = forall k (p :: k). U1 p
U1

instance Boring c => Boring (K1 i c p) where
    boring :: K1 i c p
boring = forall k i c (p :: k). c -> K1 i c p
K1 forall a. Boring a => a
boring

instance Boring (f p) => Boring (M1 i c f p) where
    boring :: M1 i c f p
boring = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall a. Boring a => a
boring

instance (Boring (f p), Boring (g p)) => Boring ((f :*: g) p) where
    boring :: (:*:) f g p
boring = forall a. Boring a => a
boring forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall a. Boring a => a
boring

instance Boring p => Boring (Par1 p) where
    boring :: Par1 p
boring = forall p. p -> Par1 p
Par1 forall a. Boring a => a
boring

instance Boring (f p) => Boring (Rec1 f p) where
    boring :: Rec1 f p
boring = forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 forall a. Boring a => a
boring

instance Boring (f (g p)) => Boring ((f :.: g) p) where
    boring :: (:.:) f g p
boring = forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 forall a. Boring a => a
boring


-------------------------------------------------------------------------------
-- Absurd
-------------------------------------------------------------------------------

-- | The 'Absurd' type is very exciting, because if somebody ever gives you a
-- value belonging to it, you know that you are already dead and in Heaven and
-- that anything you want is yours.
--
-- Similarly as there are many 'Boring' sums, there are many 'Absurd' products,
-- so we don't have 'Absurd' instances for tuples.
class Absurd a where
    absurd :: a -> b
    default absurd :: (Generic a, GAbsurd (Rep a)) => a -> b
    absurd = forall (f :: * -> *) a b. GAbsurd f => f a -> b
gabsurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. Generic a => a -> Rep a x
from

instance Absurd V.Void where
    absurd :: forall b. Void -> b
absurd = forall b. Void -> b
V.absurd

instance (Absurd a, Absurd b) => Absurd (Either a b) where
    absurd :: forall b. Either a b -> b
absurd (Left a
a) = forall a b. Absurd a => a -> b
absurd a
a
    absurd (Right b
b) = forall a b. Absurd a => a -> b
absurd b
b

instance Absurd a => Absurd (NonEmpty a) where
    absurd :: forall b. NonEmpty a -> b
absurd (a
x :| [a]
_) = forall a b. Absurd a => a -> b
absurd a
x

instance Absurd a => Absurd (Identity a) where
    absurd :: forall b. Identity a -> b
absurd = forall a b. Absurd a => a -> b
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Identity a -> a
runIdentity

instance Absurd (f (g a)) => Absurd (Compose f g a) where
    absurd :: forall b. Compose f g a -> b
absurd = forall a b. Absurd a => a -> b
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose

instance (Absurd (f a), Absurd (g a)) => Absurd (Sum f g a) where
    absurd :: forall b. Sum f g a -> b
absurd (InL f a
fa) = forall a b. Absurd a => a -> b
absurd f a
fa
    absurd (InR g a
ga) = forall a b. Absurd a => a -> b
absurd g a
ga

instance Absurd b => Absurd (Const b a) where
    absurd :: forall b. Const b a -> b
absurd = forall a b. Absurd a => a -> b
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} a (b :: k). Const a b -> a
getConst

#ifdef MIN_VERSION_tagged
instance Absurd a => Absurd (Tagged b a) where
    absurd :: forall b. Tagged b a -> b
absurd = forall a b. Absurd a => a -> b
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (s :: k) b. Tagged s b -> b
unTagged
#endif

-------------------------------------------------------------------------------
-- Generics
-------------------------------------------------------------------------------

instance Absurd (V1 p) where
#if __GLASGOW_HASKELL >= 708
    absurd v = case v of {}
#else
    absurd :: forall b. V1 p -> b
absurd V1 p
v = V1 p
v seq :: forall a b. a -> b -> b
`seq` forall a. HasCallStack => [Char] -> a
error [Char]
"absurd @(V1 p)"
#endif

instance Absurd c => Absurd (K1 i c p) where
    absurd :: forall b. K1 i c p -> b
absurd = forall a b. Absurd a => a -> b
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i c (p :: k). K1 i c p -> c
unK1

instance Absurd (f p) => Absurd (M1 i c f p) where
    absurd :: forall b. M1 i c f p -> b
absurd = forall a b. Absurd a => a -> b
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1

instance (Absurd (f p), Absurd (g p)) => Absurd ((f :+: g) p) where
    absurd :: forall b. (:+:) f g p -> b
absurd (L1 f p
a) = forall a b. Absurd a => a -> b
absurd f p
a
    absurd (R1 g p
b) = forall a b. Absurd a => a -> b
absurd g p
b

instance Absurd p => Absurd (Par1 p) where
    absurd :: forall b. Par1 p -> b
absurd = forall a b. Absurd a => a -> b
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. Par1 p -> p
unPar1

instance Absurd (f p) => Absurd (Rec1 f p) where
    absurd :: forall b. Rec1 f p -> b
absurd = forall a b. Absurd a => a -> b
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (p :: k). Rec1 f p -> f p
unRec1

instance Absurd (f (g p)) => Absurd ((f :.: g) p) where
    absurd :: forall b. (:.:) f g p -> b
absurd = forall a b. Absurd a => a -> b
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
unComp1

-------------------------------------------------------------------------------
-- More interesting stuff
-------------------------------------------------------------------------------

-- | If 'Absurd' is uninhabited then any 'Functor' that holds only
-- values of type 'Absurd' is holding no values.
vacuous :: (Functor f, Absurd a) => f a -> f b
vacuous :: forall (f :: * -> *) a b. (Functor f, Absurd a) => f a -> f b
vacuous = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. Absurd a => a -> b
absurd

-- | There is a field for every type in the 'Absurd'. Very zen.
--
-- @
-- 'devoid' :: 'Absurd' s => Over p f s s a b
-- @
-- type Over p f s t a b = p a (f b) -> s -> f t
devoid :: Absurd s => p a (f b) -> s -> f s
devoid :: forall s (p :: * -> * -> *) a (f :: * -> *) b.
Absurd s =>
p a (f b) -> s -> f s
devoid p a (f b)
_ = forall a b. Absurd a => a -> b
absurd

-- | We can always retrieve a 'Boring' value from any type.
--
-- @
-- 'united' :: 'Boring' a => Lens' s a
-- @
united :: (Boring a, Functor f) => (a -> f a) -> s -> f s
united :: forall a (f :: * -> *) s.
(Boring a, Functor f) =>
(a -> f a) -> s -> f s
united a -> f a
f s
v = s
v forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ a -> f a
f forall a. Boring a => a
boring

-------------------------------------------------------------------------------
-- default implementatiosn
-------------------------------------------------------------------------------

-- | A helper class to implement 'Generic' derivation of 'Boring'.
--
-- Technically we could do (avoiding @QuantifiedConstraints@):
--
-- @
-- type GBoring f = (Boring (f V.Void), Functor f)
--
-- gboring :: forall f x. GBoring f => f x
-- gboring = vacuous (boring :: f V.Void)
-- @
--
-- but separate class is cleaner.
--
-- >>> data B2 = B2 () () deriving (Show, Generic)
-- >>> instance Boring B2
-- >>> boring :: B2
-- B2 () ()
--
class GBoring f where
    gboring :: f a

instance GBoring U1 where
    gboring :: forall p. U1 p
gboring = forall k (p :: k). U1 p
U1

instance GBoring f => GBoring (M1 i c f) where
    gboring :: forall a. M1 i c f a
gboring = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall (f :: * -> *) a. GBoring f => f a
gboring

instance (GBoring f, GBoring g) => GBoring (f :*: g) where
    gboring :: forall a. (:*:) f g a
gboring = forall (f :: * -> *) a. GBoring f => f a
gboring forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (f :: * -> *) a. GBoring f => f a
gboring

-- There are two valid instances for GBoring (f :+: g), so we don't define
-- either of them.

instance Boring c => GBoring (K1 i c) where
    gboring :: forall a. K1 i c a
gboring = forall k i c (p :: k). c -> K1 i c p
K1 forall a. Boring a => a
boring

-- | A helper class to implement of 'Generic' derivation of 'Absurd'.
--
-- @
-- type GAbsurd f = (Absurd (f ()), Functor f)
--
-- gabsurd :: forall f x y. GAbsurd f => f x -> y
-- gabsurd = absurd . void
-- @
--
class GAbsurd f where
    gabsurd :: f a -> b

instance GAbsurd V1 where
#if __GLASGOW_HASKELL >= 708
    gabsurd x = case x of {}
#else
    gabsurd :: forall p b. V1 p -> b
gabsurd V1 a
x = V1 a
x seq :: forall a b. a -> b -> b
`seq` forall a. HasCallStack => [Char] -> a
error [Char]
"gabsurd @V1"
#endif

instance GAbsurd f => GAbsurd (M1 i c f) where
    gabsurd :: forall a b. M1 i c f a -> b
gabsurd (M1 f a
x) = forall (f :: * -> *) a b. GAbsurd f => f a -> b
gabsurd f a
x

instance Absurd c => GAbsurd (K1 i c) where
    gabsurd :: forall a b. K1 i c a -> b
gabsurd (K1 c
x) = forall a b. Absurd a => a -> b
absurd c
x

instance (GAbsurd f, GAbsurd g) => GAbsurd (f :+: g) where
    gabsurd :: forall a b. (:+:) f g a -> b
gabsurd (L1 f a
x) = forall (f :: * -> *) a b. GAbsurd f => f a -> b
gabsurd f a
x
    gabsurd (R1 g a
y) = forall (f :: * -> *) a b. GAbsurd f => f a -> b
gabsurd g a
y

-- There are two reasonable instances for GAbsurd (f :*: g), so we define neither