type-iso-0.1.0.0: Typeclasses for injective relations and isomorphisms between types.

Safe HaskellNone
LanguageHaskell2010

Data.Types.Injective

Description

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.

Synopsis

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!

Methods

to :: a -> b Source

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