{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}

{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}

-- |

-- Module      : OAlg.Data.Identity

-- Description : identical predicate

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- identical predicate.

module OAlg.Data.Identity
  (
    -- * Id

    Id(..)
  , fromId
  , trafoFromId
  , trafoToId
  , toIdG, fromIdG

    -- * Applicative

  , Applicative, amap, ($)
  , Functorial, amapf
  , Functor

    -- * Id2

  , Id2(..)
  )
  where

import Prelude (Show,Read,Eq,Ord,Enum,Bounded,Foldable)

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

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

-- Id -


-- | identical predicate.

newtype Id x = Id x deriving (Int -> Id x -> ShowS
[Id x] -> ShowS
Id x -> String
(Int -> Id x -> ShowS)
-> (Id x -> String) -> ([Id x] -> ShowS) -> Show (Id x)
forall x. Show x => Int -> Id x -> ShowS
forall x. Show x => [Id x] -> ShowS
forall x. Show x => Id x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall x. Show x => Int -> Id x -> ShowS
showsPrec :: Int -> Id x -> ShowS
$cshow :: forall x. Show x => Id x -> String
show :: Id x -> String
$cshowList :: forall x. Show x => [Id x] -> ShowS
showList :: [Id x] -> ShowS
Show,ReadPrec [Id x]
ReadPrec (Id x)
Int -> ReadS (Id x)
ReadS [Id x]
(Int -> ReadS (Id x))
-> ReadS [Id x]
-> ReadPrec (Id x)
-> ReadPrec [Id x]
-> Read (Id x)
forall x. Read x => ReadPrec [Id x]
forall x. Read x => ReadPrec (Id x)
forall x. Read x => Int -> ReadS (Id x)
forall x. Read x => ReadS [Id x]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall x. Read x => Int -> ReadS (Id x)
readsPrec :: Int -> ReadS (Id x)
$creadList :: forall x. Read x => ReadS [Id x]
readList :: ReadS [Id x]
$creadPrec :: forall x. Read x => ReadPrec (Id x)
readPrec :: ReadPrec (Id x)
$creadListPrec :: forall x. Read x => ReadPrec [Id x]
readListPrec :: ReadPrec [Id x]
Read,Id x -> Id x -> Bool
(Id x -> Id x -> Bool) -> (Id x -> Id x -> Bool) -> Eq (Id x)
forall x. Eq x => Id x -> Id x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall x. Eq x => Id x -> Id x -> Bool
== :: Id x -> Id x -> Bool
$c/= :: forall x. Eq x => Id x -> Id x -> Bool
/= :: Id x -> Id x -> Bool
Eq,Eq (Id x)
Eq (Id x) =>
(Id x -> Id x -> Ordering)
-> (Id x -> Id x -> Bool)
-> (Id x -> Id x -> Bool)
-> (Id x -> Id x -> Bool)
-> (Id x -> Id x -> Bool)
-> (Id x -> Id x -> Id x)
-> (Id x -> Id x -> Id x)
-> Ord (Id x)
Id x -> Id x -> Bool
Id x -> Id x -> Ordering
Id x -> Id x -> Id x
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall x. Ord x => Eq (Id x)
forall x. Ord x => Id x -> Id x -> Bool
forall x. Ord x => Id x -> Id x -> Ordering
forall x. Ord x => Id x -> Id x -> Id x
$ccompare :: forall x. Ord x => Id x -> Id x -> Ordering
compare :: Id x -> Id x -> Ordering
$c< :: forall x. Ord x => Id x -> Id x -> Bool
< :: Id x -> Id x -> Bool
$c<= :: forall x. Ord x => Id x -> Id x -> Bool
<= :: Id x -> Id x -> Bool
$c> :: forall x. Ord x => Id x -> Id x -> Bool
> :: Id x -> Id x -> Bool
$c>= :: forall x. Ord x => Id x -> Id x -> Bool
>= :: Id x -> Id x -> Bool
$cmax :: forall x. Ord x => Id x -> Id x -> Id x
max :: Id x -> Id x -> Id x
$cmin :: forall x. Ord x => Id x -> Id x -> Id x
min :: Id x -> Id x -> Id x
Ord,Int -> Id x
Id x -> Int
Id x -> [Id x]
Id x -> Id x
Id x -> Id x -> [Id x]
Id x -> Id x -> Id x -> [Id x]
(Id x -> Id x)
-> (Id x -> Id x)
-> (Int -> Id x)
-> (Id x -> Int)
-> (Id x -> [Id x])
-> (Id x -> Id x -> [Id x])
-> (Id x -> Id x -> [Id x])
-> (Id x -> Id x -> Id x -> [Id x])
-> Enum (Id x)
forall x. Enum x => Int -> Id x
forall x. Enum x => Id x -> Int
forall x. Enum x => Id x -> [Id x]
forall x. Enum x => Id x -> Id x
forall x. Enum x => Id x -> Id x -> [Id x]
forall x. Enum x => Id x -> Id x -> Id x -> [Id x]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: forall x. Enum x => Id x -> Id x
succ :: Id x -> Id x
$cpred :: forall x. Enum x => Id x -> Id x
pred :: Id x -> Id x
$ctoEnum :: forall x. Enum x => Int -> Id x
toEnum :: Int -> Id x
$cfromEnum :: forall x. Enum x => Id x -> Int
fromEnum :: Id x -> Int
$cenumFrom :: forall x. Enum x => Id x -> [Id x]
enumFrom :: Id x -> [Id x]
$cenumFromThen :: forall x. Enum x => Id x -> Id x -> [Id x]
enumFromThen :: Id x -> Id x -> [Id x]
$cenumFromTo :: forall x. Enum x => Id x -> Id x -> [Id x]
enumFromTo :: Id x -> Id x -> [Id x]
$cenumFromThenTo :: forall x. Enum x => Id x -> Id x -> Id x -> [Id x]
enumFromThenTo :: Id x -> Id x -> Id x -> [Id x]
Enum,Id x
Id x -> Id x -> Bounded (Id x)
forall a. a -> a -> Bounded a
forall x. Bounded x => Id x
$cminBound :: forall x. Bounded x => Id x
minBound :: Id x
$cmaxBound :: forall x. Bounded x => Id x
maxBound :: Id x
Bounded,(forall m. Monoid m => Id m -> m)
-> (forall m a. Monoid m => (a -> m) -> Id a -> m)
-> (forall m a. Monoid m => (a -> m) -> Id a -> m)
-> (forall a b. (a -> b -> b) -> b -> Id a -> b)
-> (forall a b. (a -> b -> b) -> b -> Id a -> b)
-> (forall b a. (b -> a -> b) -> b -> Id a -> b)
-> (forall b a. (b -> a -> b) -> b -> Id a -> b)
-> (forall a. (a -> a -> a) -> Id a -> a)
-> (forall a. (a -> a -> a) -> Id a -> a)
-> (forall a. Id a -> [a])
-> (forall a. Id a -> Bool)
-> (forall a. Id a -> Int)
-> (forall a. Eq a => a -> Id a -> Bool)
-> (forall a. Ord a => Id a -> a)
-> (forall a. Ord a => Id a -> a)
-> (forall a. Num a => Id a -> a)
-> (forall a. Num a => Id a -> a)
-> Foldable Id
forall a. Eq a => a -> Id a -> Bool
forall a. Num a => Id a -> a
forall a. Ord a => Id a -> a
forall m. Monoid m => Id m -> m
forall a. Id a -> Bool
forall a. Id a -> Int
forall a. Id a -> [a]
forall a. (a -> a -> a) -> Id a -> a
forall m a. Monoid m => (a -> m) -> Id a -> m
forall b a. (b -> a -> b) -> b -> Id a -> b
forall a b. (a -> b -> b) -> b -> Id a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Id m -> m
fold :: forall m. Monoid m => Id m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Id a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Id a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Id a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Id a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Id a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Id a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Id a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Id a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Id a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Id a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Id a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Id a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Id a -> a
foldr1 :: forall a. (a -> a -> a) -> Id a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Id a -> a
foldl1 :: forall a. (a -> a -> a) -> Id a -> a
$ctoList :: forall a. Id a -> [a]
toList :: forall a. Id a -> [a]
$cnull :: forall a. Id a -> Bool
null :: forall a. Id a -> Bool
$clength :: forall a. Id a -> Int
length :: forall a. Id a -> Int
$celem :: forall a. Eq a => a -> Id a -> Bool
elem :: forall a. Eq a => a -> Id a -> Bool
$cmaximum :: forall a. Ord a => Id a -> a
maximum :: forall a. Ord a => Id a -> a
$cminimum :: forall a. Ord a => Id a -> a
minimum :: forall a. Ord a => Id a -> a
$csum :: forall a. Num a => Id a -> a
sum :: forall a. Num a => Id a -> a
$cproduct :: forall a. Num a => Id a -> a
product :: forall a. Num a => Id a -> a
Foldable)

instance ApplicativeG Id h c => ApplicativeG Id (Inv2 h) c where amapG :: forall x y. Inv2 h x y -> c (Id x) (Id y)
amapG (Inv2 h x y
t h y x
_) = h x y -> c (Id x) (Id y)
forall x y. h x y -> c (Id x) (Id y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
t
instance FunctorialG Id h c => FunctorialG Id (Inv2 h) c

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

-- formId -


-- | deconstructs 'Id'.

fromId :: Id x -> x
fromId :: forall x. Id x -> x
fromId (Id x
x) = x
x

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

-- trafoFromId -


-- | transforming a @f :: x -> 'Id' y@ to a @f' :: x -> i z@.

trafoFromId :: (y -> i z) -> (x -> Id y) -> x -> i z
trafoFromId :: forall y (i :: * -> *) z x. (y -> i z) -> (x -> Id y) -> x -> i z
trafoFromId y -> i z
i x -> Id y
f x
x = y -> i z
i y
y where Id y
y = x -> Id y
f x
x

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

-- trafoToId -


-- | transforming a @f :: x -> y@ to a @f' :: x -> Id y@.

trafoToId :: (x -> y) -> x -> Id y
trafoToId :: forall x y. (x -> y) -> x -> Id y
trafoToId x -> y
f = y -> Id y
forall x. x -> Id x
Id (y -> Id y) -> (x -> y) -> x -> Id y
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
f

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

-- toIdG -


-- | the induced mapping.

toIdG :: (x -> y) -> Id x -> Id y
toIdG :: forall x y. (x -> y) -> Id x -> Id y
toIdG x -> y
f (Id x
x) = y -> Id y
forall x. x -> Id x
Id (x -> y
f x
x)

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

-- fromIdG -


-- | the induced mapping.

fromIdG :: (Id x -> Id y) -> x -> y
fromIdG :: forall x y. (Id x -> Id y) -> x -> y
fromIdG Id x -> Id y
f = Id y -> y
forall x. Id x -> x
fromId (Id y -> y) -> (x -> Id y) -> x -> y
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
. Id x -> Id y
f (Id x -> Id y) -> (x -> Id x) -> x -> Id y
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 -> Id x
forall x. x -> Id x
Id 

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

-- apIdType-


-- | application to @(->)@ based on 'Id',

apIdType :: ApplicativeG Id h (->) => ApplicationG Id h (->)
apIdType :: forall (h :: * -> * -> *).
ApplicativeG Id h (->) =>
ApplicationG Id h (->)
apIdType = ApplicationG Id h (->)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *).
ApplicativeG t a b =>
ApplicationG t a b
ApplicationG

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

-- Applicative -


-- | representable @__h__@s according to 'Id'.

type Applicative h = ApplicativeG Id h (->)

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

-- amap -


-- | representation of @__h__@ in @('->')@. 

amap :: Applicative h => h x y -> x -> y
amap :: forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h x
x = y
y where Id y
y = h x y -> Id x -> Id y
forall x y. h x y -> Id x -> Id y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h (x -> Id x
forall x. x -> Id x
Id x
x)

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

-- ($)

  
infixr 0 $

-- | right associative application on values.

($) :: Applicative h => h x y -> x -> y
$ :: forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
($) = h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap

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

-- Functorial -


instance ApplicativeG Id (->) (->) where amapG :: forall x y. (x -> y) -> Id x -> Id y
amapG = (x -> y) -> Id x -> Id y
forall x y. (x -> y) -> Id x -> Id y
toIdG

-- | functorials form @__c__@ to @('->')@ according to 'Id'.

type Functorial c = FunctorialG Id c (->)

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

-- amapf -

-- | functorial representation of @__h__@ in @('->')@. 

amapf :: Functorial h => h x y -> x -> y
amapf :: forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf = h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap

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

-- Functor -


-- | attest of being 'Functorial' from the 'Category' __c__ to the 'Category' @('->')@.

data Functor c where
  Functor :: Functorial c => Functor c  

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

-- Id2 -


-- | identical predicat.

newtype Id2 h x y = Id2 (h x y)

instance Morphism h => Morphism (Id2 h) where
  type ObjectClass (Id2 h) = ObjectClass h
  homomorphous :: forall x y. Id2 h x y -> Homomorphous (ObjectClass (Id2 h)) x y
homomorphous (Id2 h x y
h) = h x y -> Homomorphous (ObjectClass h) x y
forall x y. h x y -> Homomorphous (ObjectClass h) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h x y
h

instance ApplicativeG Id h c => ApplicativeG Id (Id2 h) c where
  amapG :: forall x y. Id2 h x y -> c (Id x) (Id y)
amapG (Id2 h x y
h) = h x y -> c (Id x) (Id y)
forall x y. h x y -> c (Id x) (Id y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h