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

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}

-- |

-- Module      : OAlg.Data.Dualisable

-- Description : concept of duality

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- defining the type of the co-object according to the kind of a given object.

-- 

-- Special care has been taken for objects of parameterized types over

-- a structured type (see "OAlg.Entity.Diagram.Definition#Duality" which serves as a boiler

-- plate for all dualities implemented here).

module OAlg.Data.Dualisable
  ( -- * Dual

    Dual, Dual1
  , Dl1(..), fromDl1, mapDl1
  , ShowDual1, EqDual1

    -- * Dualisable

  , Dualisable(..), fromDual'

    -- * Reflexive

  , Reflexive(..), fromBidual'

    -- * Transposable

  , Transposable(..)

    -- * Site

  , Site(..), ToSite

    -- * Side

  , Side(..)

    -- * Direction

  , Direction(..)
  )
  where

import Data.Kind

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

-- Dual -


-- | the kind of the co-object according to the kind of given object.

type family Dual (x :: k) :: k

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

-- Dual1 -


-- | the parameterized kind of the co-object according to the parameterized kind of a given object.

type family Dual1 (c :: k -> Type) :: k -> Type

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

-- Dl1 -


-- | wrapper for @'Dual1' __d x__@.

newtype Dl1 d x = Dl1 (Dual1 d x)

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

-- ShowDual1 -


-- | helper class to avoid undecidable instances.

class Show (Dual1 d x) => ShowDual1 d x

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

-- EqDual1 -


-- | helper class to avoid undecidable instances.

class Eq (Dual1 d x) => EqDual1 d x

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

-- fromDl1 -


-- | deconstructing 'Dl1'

fromDl1 :: Dl1 d x -> Dual1 d x
fromDl1 :: forall {k} (d :: k -> *) (x :: k). Dl1 d x -> Dual1 d x
fromDl1 (Dl1 Dual1 d x
d) = Dual1 d x
d

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

-- mapDl1 -


-- | mapping 'Dl1'.

mapDl1 :: (Dual1 d x -> Dual1 d y) -> Dl1 d x -> Dl1 d y
mapDl1 :: forall {k} (d :: k -> *) (x :: k) (y :: k).
(Dual1 d x -> Dual1 d y) -> Dl1 d x -> Dl1 d y
mapDl1 Dual1 d x -> Dual1 d y
f (Dl1 Dual1 d x
x) = Dual1 d y -> Dl1 d y
forall {k} (d :: k -> *) (x :: k). Dual1 d x -> Dl1 d x
Dl1 (Dual1 d x -> Dual1 d y
f Dual1 d x
x)

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

-- Dualisable -


-- | admitting a duality.

--

--   __Property__ Let __@x@__ be 'Dualisable', than holds: 'toDual' is a bijection

--   with its inverse 'fromDual'.

class Dualisable x where
  toDual   :: x -> Dual x
  fromDual :: Dual x -> x

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

-- fromDual' -


-- | 'fromDual' enriched with a parameterized type __@p@__ which serves as a proxy -

--   e.g. 'Data.Proxy.Proxy' or 'OAlg.Data.Identity.Id' will serve - and will not be evaluated.

--   It serves for the type checker to pick the right 'fromDual'.

fromDual' :: Dualisable x => p x -> Dual x -> x
fromDual' :: forall x (p :: * -> *). Dualisable x => p x -> Dual x -> x
fromDual' p x
_ = Dual x -> x
forall x. Dualisable x => Dual x -> x
fromDual

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

-- Reflexive -


-- | admitting reflection.

--

--   __Property__ Let __@x@__ be 'Reflexive', than holds:

--

--   (1) 'toBidual' is a bijection with its inverse 'fromBidual'.

class Reflexive x where
  toBidual   :: x -> Dual (Dual x)
  fromBidual :: Dual (Dual x) -> x

-- | 'fromBidual' enriched with a parameterized type __@p@__ which serves as a proxy -

--   e.g. 'Proxy' or 'OAlg.Data.Identity.Id' will serve - and will not be evaluated.

--   It serves for the type checker to pick the right 'fromBidual'.

fromBidual' :: Reflexive x => p x -> Dual (Dual x) -> x
fromBidual' :: forall x (p :: * -> *). Reflexive x => p x -> Dual (Dual x) -> x
fromBidual' p x
_ = Dual (Dual x) -> x
forall x. Reflexive x => Dual (Dual x) -> x
fromBidual

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

-- Transposable -


-- | transposable types.

--

--   __Property__ Let __@x@__ be a 'Transposable', then holds:

--  For all @x@ in __@x@__ holds: @'transpose' ('transpose' x) '==' x@.

class Transposable x where 
  transpose :: x -> x

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

-- Site -


-- | concept of the sites 'From' and 'To'.

data Site = From | To deriving (Int -> Site -> ShowS
[Site] -> ShowS
Site -> String
(Int -> Site -> ShowS)
-> (Site -> String) -> ([Site] -> ShowS) -> Show Site
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Site -> ShowS
showsPrec :: Int -> Site -> ShowS
$cshow :: Site -> String
show :: Site -> String
$cshowList :: [Site] -> ShowS
showList :: [Site] -> ShowS
Show,Site -> Site -> Bool
(Site -> Site -> Bool) -> (Site -> Site -> Bool) -> Eq Site
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Site -> Site -> Bool
== :: Site -> Site -> Bool
$c/= :: Site -> Site -> Bool
/= :: Site -> Site -> Bool
Eq,Eq Site
Eq Site =>
(Site -> Site -> Ordering)
-> (Site -> Site -> Bool)
-> (Site -> Site -> Bool)
-> (Site -> Site -> Bool)
-> (Site -> Site -> Bool)
-> (Site -> Site -> Site)
-> (Site -> Site -> Site)
-> Ord Site
Site -> Site -> Bool
Site -> Site -> Ordering
Site -> Site -> Site
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
$ccompare :: Site -> Site -> Ordering
compare :: Site -> Site -> Ordering
$c< :: Site -> Site -> Bool
< :: Site -> Site -> Bool
$c<= :: Site -> Site -> Bool
<= :: Site -> Site -> Bool
$c> :: Site -> Site -> Bool
> :: Site -> Site -> Bool
$c>= :: Site -> Site -> Bool
>= :: Site -> Site -> Bool
$cmax :: Site -> Site -> Site
max :: Site -> Site -> Site
$cmin :: Site -> Site -> Site
min :: Site -> Site -> Site
Ord,Int -> Site
Site -> Int
Site -> [Site]
Site -> Site
Site -> Site -> [Site]
Site -> Site -> Site -> [Site]
(Site -> Site)
-> (Site -> Site)
-> (Int -> Site)
-> (Site -> Int)
-> (Site -> [Site])
-> (Site -> Site -> [Site])
-> (Site -> Site -> [Site])
-> (Site -> Site -> Site -> [Site])
-> Enum Site
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 :: Site -> Site
succ :: Site -> Site
$cpred :: Site -> Site
pred :: Site -> Site
$ctoEnum :: Int -> Site
toEnum :: Int -> Site
$cfromEnum :: Site -> Int
fromEnum :: Site -> Int
$cenumFrom :: Site -> [Site]
enumFrom :: Site -> [Site]
$cenumFromThen :: Site -> Site -> [Site]
enumFromThen :: Site -> Site -> [Site]
$cenumFromTo :: Site -> Site -> [Site]
enumFromTo :: Site -> Site -> [Site]
$cenumFromThenTo :: Site -> Site -> Site -> [Site]
enumFromThenTo :: Site -> Site -> Site -> [Site]
Enum,Site
Site -> Site -> Bounded Site
forall a. a -> a -> Bounded a
$cminBound :: Site
minBound :: Site
$cmaxBound :: Site
maxBound :: Site
Bounded)

type instance Dual From = To
type instance Dual To = From

instance Transposable Site where
  transpose :: Site -> Site
transpose Site
From = Site
To
  transpose Site
To = Site
From

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

-- ToSite -


-- | mapping to 'Site'.

type family ToSite (s :: k) :: Site

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

-- Side -


-- | concept of sides 'LeftSide' and 'RightSide'

data Side = LeftSide | RightSide deriving (Int -> Side -> ShowS
[Side] -> ShowS
Side -> String
(Int -> Side -> ShowS)
-> (Side -> String) -> ([Side] -> ShowS) -> Show Side
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Side -> ShowS
showsPrec :: Int -> Side -> ShowS
$cshow :: Side -> String
show :: Side -> String
$cshowList :: [Side] -> ShowS
showList :: [Side] -> ShowS
Show,Side -> Side -> Bool
(Side -> Side -> Bool) -> (Side -> Side -> Bool) -> Eq Side
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Side -> Side -> Bool
== :: Side -> Side -> Bool
$c/= :: Side -> Side -> Bool
/= :: Side -> Side -> Bool
Eq,Eq Side
Eq Side =>
(Side -> Side -> Ordering)
-> (Side -> Side -> Bool)
-> (Side -> Side -> Bool)
-> (Side -> Side -> Bool)
-> (Side -> Side -> Bool)
-> (Side -> Side -> Side)
-> (Side -> Side -> Side)
-> Ord Side
Side -> Side -> Bool
Side -> Side -> Ordering
Side -> Side -> Side
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
$ccompare :: Side -> Side -> Ordering
compare :: Side -> Side -> Ordering
$c< :: Side -> Side -> Bool
< :: Side -> Side -> Bool
$c<= :: Side -> Side -> Bool
<= :: Side -> Side -> Bool
$c> :: Side -> Side -> Bool
> :: Side -> Side -> Bool
$c>= :: Side -> Side -> Bool
>= :: Side -> Side -> Bool
$cmax :: Side -> Side -> Side
max :: Side -> Side -> Side
$cmin :: Side -> Side -> Side
min :: Side -> Side -> Side
Ord,Int -> Side
Side -> Int
Side -> [Side]
Side -> Side
Side -> Side -> [Side]
Side -> Side -> Side -> [Side]
(Side -> Side)
-> (Side -> Side)
-> (Int -> Side)
-> (Side -> Int)
-> (Side -> [Side])
-> (Side -> Side -> [Side])
-> (Side -> Side -> [Side])
-> (Side -> Side -> Side -> [Side])
-> Enum Side
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 :: Side -> Side
succ :: Side -> Side
$cpred :: Side -> Side
pred :: Side -> Side
$ctoEnum :: Int -> Side
toEnum :: Int -> Side
$cfromEnum :: Side -> Int
fromEnum :: Side -> Int
$cenumFrom :: Side -> [Side]
enumFrom :: Side -> [Side]
$cenumFromThen :: Side -> Side -> [Side]
enumFromThen :: Side -> Side -> [Side]
$cenumFromTo :: Side -> Side -> [Side]
enumFromTo :: Side -> Side -> [Side]
$cenumFromThenTo :: Side -> Side -> Side -> [Side]
enumFromThenTo :: Side -> Side -> Side -> [Side]
Enum,Side
Side -> Side -> Bounded Side
forall a. a -> a -> Bounded a
$cminBound :: Side
minBound :: Side
$cmaxBound :: Side
maxBound :: Side
Bounded)

type instance Dual LeftSide = RightSide
type instance Dual RightSide = LeftSide

instance Transposable Side where
  transpose :: Side -> Side
transpose Side
LeftSide = Side
RightSide
  transpose Side
RightSide = Side
LeftSide

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

-- Direction -


-- | concept of the directions 'LeftToRight' and 'RightToLeft'.

data Direction = LeftToRight | RightToLeft deriving (Int -> Direction -> ShowS
[Direction] -> ShowS
Direction -> String
(Int -> Direction -> ShowS)
-> (Direction -> String)
-> ([Direction] -> ShowS)
-> Show Direction
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Direction -> ShowS
showsPrec :: Int -> Direction -> ShowS
$cshow :: Direction -> String
show :: Direction -> String
$cshowList :: [Direction] -> ShowS
showList :: [Direction] -> ShowS
Show,Direction -> Direction -> Bool
(Direction -> Direction -> Bool)
-> (Direction -> Direction -> Bool) -> Eq Direction
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Direction -> Direction -> Bool
== :: Direction -> Direction -> Bool
$c/= :: Direction -> Direction -> Bool
/= :: Direction -> Direction -> Bool
Eq,Eq Direction
Eq Direction =>
(Direction -> Direction -> Ordering)
-> (Direction -> Direction -> Bool)
-> (Direction -> Direction -> Bool)
-> (Direction -> Direction -> Bool)
-> (Direction -> Direction -> Bool)
-> (Direction -> Direction -> Direction)
-> (Direction -> Direction -> Direction)
-> Ord Direction
Direction -> Direction -> Bool
Direction -> Direction -> Ordering
Direction -> Direction -> Direction
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
$ccompare :: Direction -> Direction -> Ordering
compare :: Direction -> Direction -> Ordering
$c< :: Direction -> Direction -> Bool
< :: Direction -> Direction -> Bool
$c<= :: Direction -> Direction -> Bool
<= :: Direction -> Direction -> Bool
$c> :: Direction -> Direction -> Bool
> :: Direction -> Direction -> Bool
$c>= :: Direction -> Direction -> Bool
>= :: Direction -> Direction -> Bool
$cmax :: Direction -> Direction -> Direction
max :: Direction -> Direction -> Direction
$cmin :: Direction -> Direction -> Direction
min :: Direction -> Direction -> Direction
Ord,Int -> Direction
Direction -> Int
Direction -> [Direction]
Direction -> Direction
Direction -> Direction -> [Direction]
Direction -> Direction -> Direction -> [Direction]
(Direction -> Direction)
-> (Direction -> Direction)
-> (Int -> Direction)
-> (Direction -> Int)
-> (Direction -> [Direction])
-> (Direction -> Direction -> [Direction])
-> (Direction -> Direction -> [Direction])
-> (Direction -> Direction -> Direction -> [Direction])
-> Enum Direction
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 :: Direction -> Direction
succ :: Direction -> Direction
$cpred :: Direction -> Direction
pred :: Direction -> Direction
$ctoEnum :: Int -> Direction
toEnum :: Int -> Direction
$cfromEnum :: Direction -> Int
fromEnum :: Direction -> Int
$cenumFrom :: Direction -> [Direction]
enumFrom :: Direction -> [Direction]
$cenumFromThen :: Direction -> Direction -> [Direction]
enumFromThen :: Direction -> Direction -> [Direction]
$cenumFromTo :: Direction -> Direction -> [Direction]
enumFromTo :: Direction -> Direction -> [Direction]
$cenumFromThenTo :: Direction -> Direction -> Direction -> [Direction]
enumFromThenTo :: Direction -> Direction -> Direction -> [Direction]
Enum,Direction
Direction -> Direction -> Bounded Direction
forall a. a -> a -> Bounded a
$cminBound :: Direction
minBound :: Direction
$cmaxBound :: Direction
maxBound :: Direction
Bounded)

type instance Dual LeftToRight = RightToLeft
type instance Dual RightToLeft = LeftToRight

instance Transposable Direction where
  transpose :: Direction -> Direction
transpose Direction
LeftToRight = Direction
RightToLeft
  transpose Direction
RightToLeft = Direction
LeftToRight