boring-0.1.3: Boring and Absurd types

Safe HaskellNone
LanguageHaskell2010

Data.Boring

Contents

Description

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)

Synopsis

Classes

class Boring a where Source #

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.

Methods

boring :: a Source #

Instances
Boring () Source # 
Instance details

Defined in Data.Boring

Methods

boring :: () Source #

Absurd a => Boring [a] Source #

Recall regular expressions, kleene star of empty regexp is epsilon!

Instance details

Defined in Data.Boring

Methods

boring :: [a] Source #

Absurd a => Boring (Maybe a) Source #

Maybe a = a + 1, 0 + 1 = 1.

Instance details

Defined in Data.Boring

Methods

boring :: Maybe a Source #

Boring p => Boring (Par1 p) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: Par1 p Source #

Boring a => Boring (Identity a) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: Identity a Source #

b ~ BP BE => Boring (Pos b) Source #

Since: 0.1.3

Instance details

Defined in Data.Boring

Methods

boring :: Pos b Source #

b ~ BE => Boring (PosP b) Source #

Since: 0.1.3

Instance details

Defined in Data.Boring

Methods

boring :: PosP b Source #

SBinI b => Boring (SBin b) Source #

Since: 0.1.3

Instance details

Defined in Data.Boring

Methods

boring :: SBin b Source #

SBinPI b => Boring (SBinP b) Source #

Since: 0.1.3

Instance details

Defined in Data.Boring

Methods

boring :: SBinP b Source #

c => Boring (Dict c) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: Dict c Source #

Decidable a => Boring (Dec a) Source #

This relies on the fact that a is proposition in h-Prop sense.

Since: 0.1.3

Instance details

Defined in Data.Boring

Methods

boring :: Dec a Source #

n ~ S Z => Boring (Fin n) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: Fin n Source #

SNatI n => Boring (SNat n) Source #

Since: 0.1.2

Instance details

Defined in Data.Boring

Methods

boring :: SNat n Source #

Boring a => Boring (I a) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: I a Source #

SBoolI b => Boring (SBool b) Source #

Since: 0.1.2

Instance details

Defined in Data.Boring

Methods

boring :: SBool b Source #

Boring a => Boring (Stream a) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: Stream a Source #

Boring b => Boring (a -> b) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: a -> b Source #

Boring (U1 p) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: U1 p Source #

(Boring a, Boring b) => Boring (a, b) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: (a, b) Source #

Boring (Proxy a) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: Proxy a Source #

(LE n m, SNatI m) => Boring (LEProof n m) Source #

Since: 0.1.2

Instance details

Defined in Data.Boring

Methods

boring :: LEProof n m Source #

LE n m => Boring (LEProof n m) Source #

Since: 0.1.2

Instance details

Defined in Data.Boring

Methods

boring :: LEProof n m Source #

b ~ BZ => Boring (RAVec b a) Source #

Since: 0.1.3

Instance details

Defined in Data.Boring

Methods

boring :: RAVec b a Source #

n ~ Z => Boring (Vec n a) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: Vec n a Source #

n ~ Z => Boring (Vec n a) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: Vec n a Source #

Boring (f p) => Boring (Rec1 f p) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: Rec1 f p Source #

(Boring a, Boring b, Boring c) => Boring (a, b, c) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: (a, b, c) Source #

Boring a => Boring (Const a b) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: Const a b Source #

Coercible a b => Boring (Coercion a b) Source #

Coercibility is Boring too.

Instance details

Defined in Data.Boring

Methods

boring :: Coercion a b Source #

a ~ b => Boring (a :~: b) Source #

Homogeneous type equality is Boring too.

Instance details

Defined in Data.Boring

Methods

boring :: a :~: b Source #

Boring b => Boring (K b a) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: K b a Source #

Boring b => Boring (Tagged a b) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: Tagged a b Source #

Boring c => Boring (K1 i c p) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: K1 i c p Source #

(Boring (f p), Boring (g p)) => Boring ((f :*: g) p) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: (f :*: g) p Source #

(Boring a, Boring b, Boring c, Boring d) => Boring (a, b, c, d) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: (a, b, c, d) Source #

(Boring (f a), Boring (g a)) => Boring (Product f g a) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: Product f g a Source #

a ~~ b => Boring (a :~~: b) Source #

Heterogeneous type equality is Boring too.

Instance details

Defined in Data.Boring

Methods

boring :: a :~~: b Source #

Boring (f p) => Boring (M1 i c f p) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: M1 i c f p Source #

Boring (f (g p)) => Boring ((f :.: g) p) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: (f :.: g) p Source #

(Boring a, Boring b, Boring c, Boring d, Boring e) => Boring (a, b, c, d, e) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: (a, b, c, d, e) Source #

Boring (f (g a)) => Boring (Compose f g a) Source # 
Instance details

Defined in Data.Boring

Methods

boring :: Compose f g a Source #

class Absurd a where Source #

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.

Methods

absurd :: a -> b Source #

Instances
Absurd Void Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: Void -> b Source #

Absurd p => Absurd (Par1 p) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: Par1 p -> b Source #

Absurd a => Absurd (Identity a) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: Identity a -> b Source #

Absurd a => Absurd (NonEmpty a) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: NonEmpty a -> b Source #

b ~ BZ => Absurd (Pos b) Source #

Since: 0.1.3

Instance details

Defined in Data.Boring

Methods

absurd :: Pos b -> b0 Source #

n ~ Z => Absurd (Fin n) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: Fin n -> b Source #

Absurd a => Absurd (I a) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: I a -> b Source #

Absurd a => Absurd (NERAList a) Source #

Since: 0.1.3

Instance details

Defined in Data.Boring

Methods

absurd :: NERAList a -> b Source #

Absurd a => Absurd (Stream a) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: Stream a -> b Source #

(Absurd a, Absurd b) => Absurd (Either a b) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: Either a b -> b0 Source #

Absurd (V1 p) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: V1 p -> b Source #

(LE m n, n' ~ S n, SNatI n) => Absurd (LEProof n' m) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: LEProof n' m -> b Source #

(LE m n, n' ~ S n) => Absurd (LEProof n' m) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: LEProof n' m -> b Source #

Absurd (f p) => Absurd (Rec1 f p) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: Rec1 f p -> b Source #

Absurd b => Absurd (Const b a) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: Const b a -> b0 Source #

Absurd b => Absurd (K b a) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: K b a -> b0 Source #

Absurd a => Absurd (Tagged b a) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: Tagged b a -> b0 Source #

Absurd c => Absurd (K1 i c p) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: K1 i c p -> b Source #

(Absurd (f p), Absurd (g p)) => Absurd ((f :+: g) p) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: (f :+: g) p -> b Source #

(Absurd (f a), Absurd (g a)) => Absurd (Sum f g a) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: Sum f g a -> b Source #

Absurd (f p) => Absurd (M1 i c f p) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: M1 i c f p -> b Source #

Absurd (f (g p)) => Absurd ((f :.: g) p) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: (f :.: g) p -> b Source #

Absurd (f (g a)) => Absurd (Compose f g a) Source # 
Instance details

Defined in Data.Boring

Methods

absurd :: Compose f g a -> b Source #

More interesting stuff

vacuous :: (Functor f, Absurd a) => f a -> f b Source #

If Absurd is uninhabited then any Functor that holds only values of type Absurd is holding no values.

boringRep :: (Representable f, Absurd (Rep f)) => f a Source #

If an index of Representable f is Absurd, f a is Boring.

untainted :: (Representable f, Boring (Rep f)) => f a -> a Source #

If an index of Representable f is Boring, f is isomorphic to Identity.

See also Settable class in lens.

devoid :: Absurd s => p a (f b) -> s -> f s Source #

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

united :: (Boring a, Functor f) => (a -> f a) -> s -> f s Source #

We can always retrieve a Boring value from any type.

united :: Boring a => Lens' s a

Dec

Dec a can be Boring in two ways: When a is Boring or Absurd.

boringYes :: Boring a => Dec a Source #

Yes, it's boring.

Since: 0.1.3

absurdNo :: Absurd a => Dec a Source #

No, it's absurd.

Since: 0.1.3