| Safe Haskell | Trustworthy |
|---|---|
| Language | Haskell2010 |
Data.Boring
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.Absurda =>Boring(a -> b) -
|b| = 1 => |a -> b| = 1 ^ n = 1, i.e.Boringb =>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)
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.
Minimal complete definition
Nothing
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 |
|
| Boring b => Boring (a -> b) Source # | |
|
Defined in Data.Boring |
|
| Boring ( U1 p) Source # | |
|
Defined in Data.Boring |
|
| Typeable a => Boring ( TypeRep a) 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 |
|
| 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 |
|
| a ~ b => Boring (a :~: b) Source # |
Homogeneous type equality is
|
|
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.
Minimal complete definition
Nothing
Methods
Instances
Generic implementation
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 :: B2B2 () ()
Minimal complete definition
gboring
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
Minimal complete definition
gabsurd