Boring.hs

{-# LANGUAGE CPP              #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs            #-}
{-# LANGUAGE TypeOperators    #-}
-- | '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 (..),
    -- * More integeresting stuff
    vacuous,
    boringRep,
    untainted,
    ) where

import Control.Applicative   (Const (..))
import Data.Functor.Identity (Identity (..))
import Data.Functor.Rep      (Representable (..))
import Data.List.NonEmpty    (NonEmpty (..))
import Data.Proxy            (Proxy (..))
import Data.Tagged           (Tagged (..))

import qualified Data.Void as V

#if MIN_VERSION_base(4,7,0)
import qualified Data.Type.Equality as Eq
#endif

-------------------------------------------------------------------------------
-- 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

instance Boring () where
    boring = ()

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

instance Boring (Proxy a) where
    boring = Proxy

instance Boring a => Boring (Const a b) where
    boring = Const boring

instance  Boring b => Boring (Tagged a b) where
    boring = Tagged boring

instance Boring a => Boring (Identity a) where
    boring = Identity boring

instance (Boring a, Boring b) => Boring (a, b) where
    boring = (boring, boring)

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

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

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

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

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

#if MIN_VERSION_base(4,7,0)
-- | Type equality is 'Boring' too.
instance a ~ b => Boring (a Eq.:~: b) where
    boring = Eq.Refl
#endif

-------------------------------------------------------------------------------
-- 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

instance Absurd V.Void where
    absurd = V.absurd

instance (Absurd a, Absurd b) => Absurd (Either a b) where
    absurd (Left a) = absurd a
    absurd (Right b) = absurd b

instance Absurd a => Absurd (NonEmpty a) where
    absurd (x :| _) = absurd x

instance Absurd a => Absurd (Identity a) where
    absurd = absurd . runIdentity

-------------------------------------------------------------------------------
-- 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 = fmap absurd

-- | If an index of 'Representable' @f@ is 'Absurd', @f a@ is 'Boring'.
boringRep :: (Representable f, Absurd (Rep f)) => f a
boringRep = tabulate absurd

-- | If an index of 'Representable' @f@ is 'Boring', @f@ is isomorphic to 'Identity'.
--
-- See also @Settable@ class in @lens@.
untainted :: (Representable f, Boring (Rep f)) => f a -> a
untainted = flip index boring