type-iso-0.1.0.0: Data/Types/Isomorphic.hs
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
-- |Contains the class definition of 'Iso', indicating isomorphism between two
-- types.
module Data.Types.Isomorphic (
Iso(..),
module Data.Types.Injective,
from,
) where
import qualified Numeric.Natural as N
import qualified Numeric.Peano as PN
import qualified Data.Text as TS
import qualified Data.Text.Lazy as TL
import Data.Types.Injective
-- |The class of isomorphic types, i.e. those which can be cast to each
-- other withouth loss of information. Type isomorphism is an equivalence
-- relation (reflexive, symmetric, transitive), but due to the limitations
-- of the type system, only reflexivity is implemented for all types.
-- Since there are no type inequality constraints, writing symmetry and
-- transitivity instances over all types would result in overlapping instances
-- with due to reflexivity.
--
-- The following must be ensured:
--
-- [@Isomorphism@]
-- @
-- isoFrom . isoTo = id
-- @
--
-- Reflexivity, symmetry and transitivity are then "free":
--
-- @
-- instance Iso a a where
-- isoTo = id
-- isoFrom = id
-- @
--
-- @
-- instance Iso a b => Iso b a where
-- isoTo = isoFrom
-- isoFrom = isoTo
-- @
--
-- @
-- instance (Iso a b, Iso b c) => Iso a c where
-- isoTo = isoTo . isoTo
-- isFrom = isoFrom . isoFrom
-- @
--
-- Out of these, only the first one (reflexivity) is actually implemented,
-- since the other two would result in overlapping instances. We would be able
-- to avoid this with type inequality constrains (e.g. @a \/~ b@, @a \/~ c@,
-- @b \/~ c)@.
class (Injective a b, Injective b a) => Iso a b where
-- |Synonym for 'to'.
from :: (Iso a b) => b -> a
from = to
instance Iso a a where
-- equivalence class of string types.
instance Iso TS.Text String
instance Iso String TS.Text
instance Iso TL.Text String
instance Iso String TL.Text
instance Iso TS.Text TL.Text
instance Iso TL.Text TS.Text
-- Peano wholes and integers.
instance Iso PN.Whole Integer
instance Iso Integer PN.Whole