{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}

-- |

-- Module      : OAlg.Category.Map

-- Description : categories of mappings.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- categoris of mappings.

module OAlg.Category.Map
  ( Map(..)
  )
  where

import OAlg.Category.Applicative
import OAlg.Category.Definition
import OAlg.Structure.Definition

--------------------------------------------------------------------------------

-- Map -


-- | mapping between @__s__@-structures.

data Map s x y where
  Map :: (Structure s x, Structure s y) => (x -> y) -> Map s x y
  
instance Morphism (Map s) where
  type ObjectClass (Map s) = s
  homomorphous :: forall x y. Map s x y -> Homomorphous (ObjectClass (Map s)) x y
homomorphous (Map x -> y
_) = Struct s x
forall s x. Structure s x => Struct s x
Struct Struct s x -> Struct s y -> Homomorphous s x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct s y
forall s x. Structure s x => Struct s x
Struct

instance Category (Map s) where
  cOne :: forall x. Struct (ObjectClass (Map s)) x -> Map s x x
cOne Struct (ObjectClass (Map s)) x
Struct = (x -> x) -> Map s x x
forall s x y.
(Structure s x, Structure s y) =>
(x -> y) -> Map s x y
Map x -> x
forall x. x -> x
id
  Map y -> z
f . :: forall y z x. Map s y z -> Map s x y -> Map s x z
. Map x -> y
g = (x -> z) -> Map s x z
forall s x y.
(Structure s x, Structure s y) =>
(x -> y) -> Map s x y
Map (y -> z
f (y -> z) -> (x -> y) -> x -> z
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. x -> y
g)

instance ApplicativeG [] (Map s) (->) where
  amapG :: forall x y. Map s x y -> [x] -> [y]
amapG (Map x -> y
f) [x]
xs = (x -> y) -> [x] -> [y]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> y
f [x]
xs

instance FunctorialG [] (Map s) (->)