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
From trait with Haskell flavor.
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.
input is mapped to a unique
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.
There are many examples of injections scattered throughout Haskell,
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
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
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:
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
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
Maybe a contains either zero or one values of
[a] contains zero or more values of
Some common conversions are notably not injective.
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
toInteger :: Integra a => a -> Integer
Where this conversion is a total equivalence, it forms a canonical injection into
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
Injection is a lossless conversion, we can define a
Retraction which undoes it.
retract :: into -> Maybe from
is the (left) inverse of
retract (inject x) = Just x
retract is partial (returns
Maybe) because the type
into may be larger than the type
that is, there may be values in
into which are not
and in that case
retract may return
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
| x < 0 = Nothing
| otherwise = Just (fromInteger x)