Canonical categorical conversions (injections and projections)

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

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 uniqueoutput. 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)