# injections: Canonical categorical conversions (injections and projections)

[ bsd3, data, library ] [ Propose Tags ]

Canonical injections and projections. See README.md for more details.

Versions [RSS] [faq] 0.1.0.0 CHANGELOG.md base (>=4.12 && <4.16), containers (>=0.5), text (>=1.2) [details] BSD-3-Clause 2020 Thomas Tuegel Thomas Tuegel Thomas Tuegel Data https://github.com/ttuegel/injections https://github.com/ttuegel/injections/issues head: git clone https://github.com/ttuegel/injections.git by ThomasTuegel at 2021-08-26T02:08:42Z NixOS:0.1.0.0 47 total (0 in the last 30 days) (no votes yet) [estimated by Bayesian average] λ λ λ Docs available Last success reported on 2021-08-26

## Modules

[Index] [Quick Jump]

#### Maintainer's Corner

For package maintainers and hackage trustees

Candidates

• No Candidates

[back to package description]

# injections

Canonical categorical conversions (injections and projections) between Haskell types.

Problem: We want predictable conversions between types that have equivalent semantics in their domains but not equivalent representations (so we can't use coerce).

Alternatively: Rust's From trait with Haskell flavor.

## Injection

The class Injection describes a lossless conversion from one type to another; that is, the sole method of the class,

inject :: from -> into


takes a value input :: from and returns a value output :: into which preserves all the information contained in the input. Specifically, each input is mapped to a unique output. In mathematical terminology, inject is injective:

inject a ≡ inject b → a ≡ b


the outputs of two calls to inject is the same only if the inputs are the same. The name of the class is derived from the mathematical term.

Injection models the "is-a" relationship used in languages with subtypes (such as in object-oriented programming), but an explicit cast with inject is required in Haskell.

### Examples

There are many examples of injections scattered throughout Haskell, but the Injection class collects them in one place. Here we present some examples. Some of these instances have been generalized in the library, but we present the simplified version here for explanatory purposes.

Dynamic is a dynamically-typed wrapper for values of all Typeable types. Wrapping a value with toDyn preserves the value exactly, so we know that it is injective:

instance Typeable a => Injection a Dynamic where
inject = toDyn


The constructor Just :: a -> Maybe a is an injective function:

instance Injection a (Maybe a) where
inject = Just


Constructors with a single argument are always injective functions. We must use Just here; if we had written inject _ = Nothing, that would violate the injective law. Usually, any putative definition of inject with a wildcard match on the left-hand side will fail to be injective. There are exceptions to this guideline; for example, this instance is injective:

-- BAD!
instance Injection () (Maybe ()) where
-- This is injective because the type () has only one value.
inject _ = Nothing


However, we also require instances to be canonical. This instance isn't canonical because it arbitrarily restricts @from ~ ()@. Actually, there is already the definition of a canonical injection into Maybe; we may as well write

instance Injection a (Maybe a) where
inject = pure


One consequence of the injectivity law is that the output type must be at least as large as the input type. We can inject a Maybe a into a [a] because the latter type is strictly larger:

instance Injection (Maybe a) [a] where
inject = maybeToList


Where Maybe a contains either zero or one values of a, [a] contains zero or more values of a.

Some common conversions are notably not injective. For example, Data.Map.fromList returns the same Map for different lists:

Data.Map.fromList [('a', 'A'), ('b', 'B')] == Data.Map.fromList [('b', 'B'), ('a', 'A')]


Therefore, we cannot define an instance [(k, v)] (Map k v).

When there is an equivalence between two types, that equivalence is usually an injection. For example, the class Integral defines

toInteger :: Integra a => a -> Integer


Where this conversion is a total equivalence, it forms a canonical injection into Integer:

instance Injection Natural Integer where
inject = toInteger


Likewise, the class Num defines an equivalence

fromInteger :: Num a => Integer -> a


For types that have total implementations of fromInteger, this is usually an injection:

instance HasResolution a => Injection Integer (Fixed a) where
inject = fromInteger

-- BAD: No reasonable person would accept this!
instance Injection String Text where
inject = Text.pack . reverse


## Retraction

Because Injection is a lossless conversion, we can define a Retraction which undoes it. The method

retract :: into -> Maybe from


is the (left) inverse of inject:

retract (inject x) = Just x


retract is partial (returns Maybe) because the type into may be larger than the type from; that is, there may be values in into which are not inject-ed from from, and in that case retract may return Nothing.

### Examples

instance Typeable a => Retraction a Dynamic where
retract = fromDyn

instance Retraction a (Maybe a) where
retract = id

instance Retraction (Maybe a) [a] where
retract [] = Just Nothing
retract [x] = Just (Just x)
retract _ = Nothing

instance Retraction Natural Integer where
retract x
| x < 0 = Nothing
| otherwise = Just (fromInteger x)