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

Safe HaskellSafe
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!

Minimal complete definition

to

Methods

to :: forall b1 a1. (b1 ~ b, a1 ~ a) => a -> b Source #

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

Instances

Injective Integer Rational Source # 

Methods

to :: ((* ~ b1) Rational, (* ~ a1) Integer) => Integer -> Rational Source #

Injective Integer Whole Source # 

Methods

to :: ((* ~ b1) Whole, (* ~ a1) Integer) => Integer -> Whole Source #

Injective Natural Integer Source # 

Methods

to :: ((* ~ b1) Integer, (* ~ a1) Natural) => Natural -> Integer Source #

Injective Natural Rational Source # 

Methods

to :: ((* ~ b1) Rational, (* ~ a1) Natural) => Natural -> Rational Source #

Injective Natural Nat Source # 

Methods

to :: ((* ~ b1) Nat, (* ~ a1) Natural) => Natural -> Nat Source #

Injective Natural Whole Source # 

Methods

to :: ((* ~ b1) Whole, (* ~ a1) Natural) => Natural -> Whole Source #

Injective a a Source # 

Methods

to :: ((* ~ b1) a, (* ~ a1) a) => a -> a Source #

Injective String Text Source # 

Methods

to :: ((* ~ b1) Text, (* ~ a1) String) => String -> Text Source #

Injective String Text Source # 

Methods

to :: ((* ~ b1) Text, (* ~ a1) String) => String -> Text Source #

Injective Nat Integer Source # 

Methods

to :: ((* ~ b1) Integer, (* ~ a1) Nat) => Nat -> Integer Source #

Injective Nat Natural Source # 

Methods

to :: ((* ~ b1) Natural, (* ~ a1) Nat) => Nat -> Natural Source #

Injective Nat Rational Source # 

Methods

to :: ((* ~ b1) Rational, (* ~ a1) Nat) => Nat -> Rational Source #

Injective Nat Whole Source # 

Methods

to :: ((* ~ b1) Whole, (* ~ a1) Nat) => Nat -> Whole Source #

Injective Whole Integer Source # 

Methods

to :: ((* ~ b1) Integer, (* ~ a1) Whole) => Whole -> Integer Source #

Injective Whole Rational Source # 

Methods

to :: ((* ~ b1) Rational, (* ~ a1) Whole) => Whole -> Rational Source #

Injective Text String Source # 

Methods

to :: ((* ~ b1) String, (* ~ a1) Text) => Text -> String Source #

Injective Text Text Source # 

Methods

to :: ((* ~ b1) Text, (* ~ a1) Text) => Text -> Text Source #

Injective Text String Source # 

Methods

to :: ((* ~ b1) String, (* ~ a1) Text) => Text -> String Source #

Injective Text Text Source # 

Methods

to :: ((* ~ b1) Text, (* ~ a1) Text) => Text -> Text Source #

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

Methods

to :: ((* ~ b1) (Either a b), (* ~ a1) (Maybe b)) => Maybe b -> Either a b Source #