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