Data.Types.Injective

Injective types. This module contains the Injective typeclass and instances for the following equivalence classes:

• {Strict Text, Lazy Text, String}. ByteStrings 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, but Nat has lazy infinity.

Additional injections:

• Maybe to Either (the reverse is not true, since different Left values would all be converted to Nothing).
• Integers to Rational.
• Natural numbers to Integer and Rational.

Documentation

class Injective a b where

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!

Methods

to :: a -> b

Converts a value of type a "losslessly" to one of type b.

Instances

Injective Integer Rational

Injective Integer Whole

Injective String Text

Injective String Text

Injective a a

Injective Natural Integer

Injective Natural Rational

Injective Natural Nat

Injective Natural Whole

Injective Nat Integer

Injective Nat Rational

Injective Nat Natural

Injective Nat Whole

Injective Whole Integer

Injective Whole Rational

Injective Text String

Injective Text Text

Injective Text String

Injective Text Text

Default a => Injective (Maybe b) (Either a b)