Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Injective types. This module contains the Injective
typeclass and instances
for the following equivalence classes:
{Strict Text, Lazy Text, String}
.ByteString
s are not part of this, since there exists more than one way to turn unicode text into a ByteString (see Data.Text.Encoding and Data.Text.Lazy.Encoding).{Whole, Integer}
. Be advices, though, that Peano numbers may contain unobservable infinities (i.e.infinity = S infinity
) and thus, the conversion to Integer may not terminate.{Nat, Natural}
. For finite values, they're extensionally equivalent, butNat
has lazy infinity.
Additional injections:
- class Injective a b where
Documentation
class Injective a b where Source #
The class relation between types a
and b
s.t. a
can be injected
into b
.
The following laws must be fulfilled:
Injectivity
x /= y ==> (to x) /= (to y)
Totality
to
should be a total function. No cheating by it undefined for parts of the set!
to :: forall b1 a1. (b1 ~ b, a1 ~ a) => a -> b Source #
Converts a value of type a
"losslessly" to one of type b
.