{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE Rank2Types #-}

module Data.Connection.Yoneda where

import Data.Int
import Data.Word
import Data.Prd
import Data.Prd.Nan
import Data.Prd.Lattice
import Data.Bifunctor
import Data.Function
import Data.Functor.Identity
import Data.Functor.Product
import Data.Functor.Sum
import Data.Connection
import Data.Connection.Int
import Data.Connection.Word
import Data.Connection.Float
import Data.Foldable
import Data.List (unfoldr)
import GHC.Num (subtract)
import Numeric.Natural
import Data.Bool
import Prelude hiding (Enum(..), Ord(..), until, filter)

import qualified Control.Category as C


type family Rep a :: *

type instance Rep (Down a) = Down (Rep a)
type instance Rep Bool = Bool

-- | Yoneda representation for lattice ideals & filters.
--
-- A subset /I/ of a lattice is an ideal if and only if it is a lower set 
-- that is closed under finite joins, i.e., it is nonempty and for all 
-- /x/, /y/ in /I/, the element /x \vee y/ is also in /I/.
--
-- /upper/ and /lower/ commute with /Down/:
--
-- * @lower x y == upper (Down x) (Down y)@
--
-- * @lower (Down x) (Down y) == upper x y@
--
-- /Rep a/ is upward-closed:
--
-- * @'upper' x s && x '<~' y ==> 'upper' y s@
--
-- * @'upper' x s && 'upper' y s ==> 'connl' 'filter' x '/\' 'connl' 'filter' y '>~' s@
--
-- /Rep a/ is downward-closed:
--
-- * @'lower' x s && x '>~' y ==> 'lower' y s@
--
-- * @'lower' x s && 'lower' y s ==> 'connl' 'ideal' x '\/' 'connl' 'ideal' y '~<' s@
--
-- Finally /filter >>> ideal/ and /ideal >>> filter/ are both connections
-- on /a/ and /Rep a/ respectively.
--
-- See:
--
-- * <https://en.wikipedia.org/wiki/Filter_(mathematics)>
-- * <https://en.wikipedia.org/wiki/Ideal_(order_theory)>
--
class (Prd a, Lattice (Rep a)) => Yoneda a where

  -- | Principal ideal generated by an element of /a/.
  ideal :: Conn (Rep a) a

  -- | Lower set in /a/ generated by an element in /Rep a/.
  lower :: Rep a -> a -> Bool

  -- | Principal filter generated by an element of /a/.
  filter :: Conn a (Rep a)

  -- | Upper set in /a/ generated by an element in /Rep a/.
  upper :: Rep a -> a -> Bool


instance Yoneda a => Yoneda (Down a) where
  ideal = dual filter
  lower (Down r) (Down a) = upper @a r a
  filter = dual ideal
  upper (Down r) (Down a) = lower @a r a

instance Yoneda Bool where
  ideal = C.id
  lower = (>~)
  filter = C.id
  upper = (<~)