Safe Haskell  None 

Language  Haskell2010 
Boring
and Absurd
classes. One approach.
Different approach would be to have
 noneonetons 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.
, orAbsurd
a =>Boring
(a > b)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
 class Boring a where
 boring :: a
 class Absurd a where
 absurd :: a > b
 vacuous :: (Functor f, Absurd a) => f a > f b
 boringRep :: (Representable f, Absurd (Rep f)) => f a
 untainted :: (Representable f, Boring (Rep f)) => f a > a
 devoid :: Absurd s => p a (f b) > s > f s
 united :: (Boring a, Functor f) => (a > f a) > s > f s
 boringYes :: Boring a => Dec a
 absurdNo :: Absurd a => Dec a
Classes
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
(
and
Boring
a, Absurd
b) => Either a b(
would be valid instances.Absurd
a, Boring
b) => Either a b
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.
Instances
Boring () Source #  
Defined in Data.Boring  
Absurd a => Boring [a] Source #  Recall regular expressions, kleene star of empty regexp is epsilon! 
Defined in Data.Boring  
Absurd a => Boring (Maybe a) Source # 

Defined in Data.Boring  
Boring p => Boring (Par1 p) Source #  
Defined in Data.Boring  
Boring a => Boring (Identity a) Source #  
Defined in Data.Boring  
c => Boring (Dict c) Source #  
Defined in Data.Boring  
Decidable a => Boring (Dec a) Source #  This relies on the fact that Since: 0.1.3 
Defined in Data.Boring  
n ~ S Z => Boring (Fin n) Source #  
Defined in Data.Boring  
SNatI n => Boring (SNat n) Source #  Since: 0.1.3 
Defined in Data.Boring  
Boring a => Boring (I a) Source #  
Defined in Data.Boring  
SBoolI b => Boring (SBool b) Source #  Since: 0.1.3 
Defined in Data.Boring  
Boring a => Boring (Stream a) Source #  
Defined in Data.Boring  
Boring b => Boring (a > b) Source #  
Defined in Data.Boring  
Boring (U1 p) Source #  
Defined in Data.Boring  
(Boring a, Boring b) => Boring (a, b) Source #  
Defined in Data.Boring  
Boring (Proxy a) Source #  
Defined in Data.Boring  
(LE n m, SNatI m) => Boring (LEProof n m) Source #  Since: 0.1.3 
Defined in Data.Boring  
LE n m => Boring (LEProof n m) Source #  Since: 0.1.3 
Defined in Data.Boring  
n ~ Z => Boring (Vec n a) Source #  
Defined in Data.Boring  
n ~ Z => Boring (Vec n a) Source #  
Defined in Data.Boring  
Boring (f p) => Boring (Rec1 f p) Source #  
Defined in Data.Boring  
(Boring a, Boring b, Boring c) => Boring (a, b, c) Source #  
Defined in Data.Boring  
Boring a => Boring (Const a b) Source #  
Defined in Data.Boring  
Coercible a b => Boring (Coercion a b) Source #  Coercibility is 
Defined in Data.Boring  
a ~ b => Boring (a :~: b) Source #  Homogeneous type equality is 
Defined in Data.Boring  
Boring b => Boring (K b a) Source #  
Defined in Data.Boring  
Boring b => Boring (Tagged a b) Source #  
Defined in Data.Boring  
Boring c => Boring (K1 i c p) Source #  
Defined in Data.Boring  
(Boring (f p), Boring (g p)) => Boring ((f :*: g) p) Source #  
Defined in Data.Boring  
(Boring a, Boring b, Boring c, Boring d) => Boring (a, b, c, d) Source #  
Defined in Data.Boring  
(Boring (f a), Boring (g a)) => Boring (Product f g a) Source #  
Defined in Data.Boring  
a ~~ b => Boring (a :~~: b) Source #  Heterogeneous type equality is 
Defined in Data.Boring  
Boring (f p) => Boring (M1 i c f p) Source #  
Defined in Data.Boring  
Boring (f (g p)) => Boring ((f :.: g) p) Source #  
Defined in Data.Boring  
(Boring a, Boring b, Boring c, Boring d, Boring e) => Boring (a, b, c, d, e) Source #  
Defined in Data.Boring  
Boring (f (g a)) => Boring (Compose f g a) Source #  
Defined in Data.Boring 
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.
Instances
More interesting stuff
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
.