lude

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

Adjunction.hs (1261B)

      1 module Lude.Algebra.Category.Adjunction (
      2     Adjoint (..),
      3 ) where
      4 
      5 import Lude.Algebra.Category.Core
      6 import Lude.Algebra.Category.Iso
      7 import Lude.Haskell
      8 
      9 -- TODO: Zappable?
     10 
     11 --------------------------------------------------------------------------------
     12 
     13 type Adjoint :: forall {i} {j}. (i -> j) -> (j -> i) -> Constraint
     14 class (Functorial f, Functorial g, Dom f ~ Cod g, Cod f ~ Dom g) => Adjoint (f :: i -> j) (g :: j -> i) | f -> g, g -> f where
     15     {-# MINIMAL unit, counit | adj #-}
     16 
     17     unit :: forall (a :: i). (Obj (Dom f) a) => Dom f a (g (f a))
     18     unit = to adj identity \\ f `preservesObj` a
     19 
     20     counit :: forall (b :: j). (Obj (Cod f) b) => Cod f (f (g b)) b
     21     counit = fro adj identity \\ g `preservesObj` b
     22 
     23     adj :: forall (a :: i) (b :: j). (Obj (Dom f) a, Obj (Cod f) b) => Iso Function (Cod f (f a) b) (Dom f a (g b))
     24     adj = MkIso (\h -> map h . unit) (\h -> counit . map h)
     25 
     26 --------------------------------------------------------------------------------
     27 -- Haskell
     28 
     29 instance Adjoint Given Evidence where
     30     unit = witnessSelf
     31     counit = coprovisionSelf
     32     adj = MkIso witnessOf coprovisionOf
     33 
     34 instance Adjoint Evidence Given where
     35     unit = provisionSelf
     36     counit = cowitnessSelf
     37     adj = MkIso provisionOf cowitnessOf