Safe Haskell | None |
---|---|

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, but`Nat`

has lazy infinity.

Additional injections:

# 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!