lude

Haskell prelude alternative
git clone git://git.rr3.xyz/lude | git clone gits://git.rr3.xyz/lude
Log | Files | Refs | README | LICENSE

Iso.hs (1342B)

      1 module Lude.Algebra.Category.Iso (
      2     Iso (..),
      3 ) where
      4 
      5 import Lude.Algebra.Category.Core
      6 import Lude.Haskell
      7 
      8 -- TODO: Iso is a groupoid.
      9 
     10 --------------------------------------------------------------------------------
     11 
     12 -- | An isomorphism (in some category)
     13 --
     14 -- In other words, @Iso p@ is the *core* of @p@.
     15 --
     16 -- Laws:
     17 --   - @to . fro = identity@
     18 --   - @fro . to = identity@
     19 type Iso :: forall {i}. Cat i -> Cat i
     20 data Iso p a b = MkIso {to :: a `p` b, fro :: b `p` a}
     21 
     22 instance (Categorical p) => Iso p a b `Witnesses` Mor (Iso p) a b where
     23     witness (MkIso f _) = MkEvidence \\ witnessMor f
     24 
     25 instance (Categorical p) => Categorical (Iso p) where
     26     type Obj (Iso p) = Obj p
     27     identity = MkIso identity identity
     28     compose (MkIso f0 f1) (MkIso g0 g1) = MkIso (f0 . g0) (g1 . f1)
     29     witnessMor = witness
     30 
     31 instance (Categorical p) => Functorial (Iso p a) where
     32     type Dom (Iso p a) = Iso p
     33     type Cod (Iso p a) = Function
     34     map = compose
     35 
     36 instance (Categorical p) => Functorial (Iso p) where
     37     type Dom (Iso p) = Dual (Iso p)
     38     type Cod (Iso p) = Iso p ==> Function
     39     map (MkDual f) = Naturally (. f)
     40 
     41 --------------------------------------------------------------------------------
     42 
     43 -- TODO: ?
     44 -- isoCoerce :: forall (a :: Type) (b :: Type). (Coercible a b) => Iso Function a b
     45 -- isoCoerce = MkIso coerce coerce