{-# LANGUAGE CPP               #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE Trustworthy       #-}
{-# LANGUAGE TypeOperators     #-}
{-# LANGUAGE EmptyCase         #-}
-- | '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

import qualified Data.Coerce        as Co
import qualified Data.Type.Coercion as Co

import qualified Data.Type.Equality as Eq

import qualified Type.Reflection as Typeable

#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 = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to Rep a Any
forall a. Rep a a
forall (f :: * -> *) a. GBoring f => f a
gboring

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

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

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

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

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

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

instance Boring (f (g a)) => Boring (Compose f g a) where
    boring :: Compose f g a
boring = f (g a) -> Compose f g a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose f (g a)
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 = f a -> g a -> Product f g a
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair f a
forall a. Boring a => a
boring g a
forall a. Boring a => a
boring

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

instance (Boring a, Boring b, Boring c) => Boring (a, b, c) where
    boring :: (a, b, c)
boring = (a
forall a. Boring a => a
boring, b
forall a. Boring a => a
boring, c
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 = (a
forall a. Boring a => a
boring, b
forall a. Boring a => a
boring, c
forall a. Boring a => a
boring, d
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 = (a
forall a. Boring a => a
boring, b
forall a. Boring a => a
boring, c
forall a. Boring a => a
boring, d
forall a. Boring a => a
boring, e
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 = Maybe a
forall a. Maybe a
Nothing

-- | Coercibility is 'Boring' too.
instance Co.Coercible a b => Boring (Co.Coercion a b) where
    boring :: Coercion a b
boring = Coercion a b
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Co.Coercion

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

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

instance Typeable.Typeable a => Boring (Typeable.TypeRep a) where
    boring :: TypeRep a
boring = TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
Typeable.typeRep

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

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

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

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

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

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

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

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

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

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

instance Boring (f (g p)) => Boring ((f :.: g) p) where
    boring :: (:.:) f g p
boring = f (g p) -> (:.:) f g p
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 f (g p)
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 = Rep a Any -> b
forall a b. Rep a a -> b
forall (f :: * -> *) a b. GAbsurd f => f a -> b
gabsurd (Rep a Any -> b) -> (a -> Rep a Any) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from

instance Absurd V.Void where
    absurd :: forall b. Void -> b
absurd = Void -> b
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) = a -> b
forall b. a -> b
forall a b. Absurd a => a -> b
absurd a
a
    absurd (Right b
b) = b -> b
forall b. 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]
_) = a -> b
forall b. a -> b
forall a b. Absurd a => a -> b
absurd a
x

instance Absurd a => Absurd (Identity a) where
    absurd :: forall b. Identity a -> b
absurd = a -> b
forall b. a -> b
forall a b. Absurd a => a -> b
absurd (a -> b) -> (Identity a -> a) -> Identity a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> a
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 = f (g a) -> b
forall b. f (g a) -> b
forall a b. Absurd a => a -> b
absurd (f (g a) -> b) -> (Compose f g a -> f (g a)) -> Compose f g a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f g a -> f (g a)
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) = f a -> b
forall b. f a -> b
forall a b. Absurd a => a -> b
absurd f a
fa
    absurd (InR g a
ga) = g a -> b
forall b. g a -> b
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 = b -> b
forall b. b -> b
forall a b. Absurd a => a -> b
absurd (b -> b) -> (Const b a -> b) -> Const b a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const b a -> b
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 = a -> b
forall b. a -> b
forall a b. Absurd a => a -> b
absurd (a -> b) -> (Tagged b a -> a) -> Tagged b a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tagged b a -> a
forall {k} (s :: k) b. Tagged s b -> b
unTagged
#endif

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

instance Absurd (V1 p) where
    absurd :: forall b. V1 p -> b
absurd V1 p
v = case V1 p
v of {}

instance Absurd c => Absurd (K1 i c p) where
    absurd :: forall b. K1 i c p -> b
absurd = c -> b
forall b. c -> b
forall a b. Absurd a => a -> b
absurd (c -> b) -> (K1 i c p -> c) -> K1 i c p -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c p -> 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 = f p -> b
forall b. f p -> b
forall a b. Absurd a => a -> b
absurd (f p -> b) -> (M1 i c f p -> f p) -> M1 i c f p -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f p -> f p
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) = f p -> b
forall b. f p -> b
forall a b. Absurd a => a -> b
absurd f p
a
    absurd (R1 g p
b) = g p -> b
forall b. 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 = p -> b
forall b. p -> b
forall a b. Absurd a => a -> b
absurd (p -> b) -> (Par1 p -> p) -> Par1 p -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Par1 p -> p
forall p. Par1 p -> p
unPar1

instance Absurd (f p) => Absurd (Rec1 f p) where
    absurd :: forall b. Rec1 f p -> b
absurd = f p -> b
forall b. f p -> b
forall a b. Absurd a => a -> b
absurd (f p -> b) -> (Rec1 f p -> f p) -> Rec1 f p -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec1 f p -> f p
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 = f (g p) -> b
forall b. f (g p) -> b
forall a b. Absurd a => a -> b
absurd (f (g p) -> b) -> ((:.:) f g p -> f (g p)) -> (:.:) f g p -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:.:) f g p -> f (g p)
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 = (a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
forall b. a -> b
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)
_ = s -> f s
forall b. s -> 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 s -> f a -> f s
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ a -> f a
f a
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 = U1 a
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 = f a -> M1 i c f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 f a
forall a. f a
forall (f :: * -> *) a. GBoring f => f a
gboring

instance (GBoring f, GBoring g) => GBoring (f :*: g) where
    gboring :: forall a. (:*:) f g a
gboring = f a
forall a. f a
forall (f :: * -> *) a. GBoring f => f a
gboring f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
forall a. g a
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 = c -> K1 i c a
forall k i c (p :: k). c -> K1 i c p
K1 c
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
    gabsurd :: forall p b. V1 p -> b
gabsurd V1 a
x = case V1 a
x of {}

instance GAbsurd f => GAbsurd (M1 i c f) where
    gabsurd :: forall a b. M1 i c f a -> b
gabsurd (M1 f a
x) = f a -> b
forall a b. f a -> b
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) = c -> b
forall b. c -> b
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) = f a -> b
forall a b. f a -> b
forall (f :: * -> *) a b. GAbsurd f => f a -> b
gabsurd f a
x
    gabsurd (R1 g a
y) = g a -> b
forall a b. g a -> b
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