{-# 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.Dioid.Interval
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)

import qualified Control.Category as C


type family Rep a :: *


-- | 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 also:
--
-- * <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 :: Rep a -> a -> Bool

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

    upper :: Rep a -> a -> Bool

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

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