{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Data.Connection.Property (
adjoint,
adjointL,
adjointR,
adjunction,
closed,
closedL,
closedR,
kernel,
kernelL,
kernelR,
invertible,
monotonic,
monotonicR,
monotonicL,
monotone,
idempotent,
idempotentL,
idempotentR,
projective,
) where
import safe Data.Connection.Conn
import safe Data.Order
import safe Data.Order.Property
import safe Prelude hiding (Num (..), Ord (..), ceiling, floor)
adjoint :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> b -> Bool
adjoint t a b =
adjointL t a b
&& adjointR t a b
&& adjointL (connL t) b a
&& adjointR (connR t) b a
adjointL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool
adjointL (ConnL f g) = adjunction (<~) (<~) f g
adjointR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool
adjointR (ConnR f g) = adjunction (>~) (>~) g f
adjunction :: Rel r Bool -> Rel s Bool -> (s -> r) -> (r -> s) -> s -> r -> Bool
adjunction (#) (%) f g a b = f a # b <=> a % g b
closed :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> Bool
closed t a = closedL t a && closedR t a
closedL :: (Preorder a, Preorder b) => ConnL a b -> a -> Bool
closedL (ConnL f g) = invertible (>~) f g
closedR :: (Preorder a, Preorder b) => ConnR a b -> a -> Bool
closedR (ConnR f g) = invertible (<~) g f
kernel :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> b -> Bool
kernel t b = kernelL t b && kernelR t b
kernelL :: (Preorder a, Preorder b) => ConnL a b -> b -> Bool
kernelL (ConnL f g) = invertible (<~) g f
kernelR :: (Preorder a, Preorder b) => ConnR a b -> b -> Bool
kernelR (ConnR f g) = invertible (>~) f g
invertible :: Rel s b -> (s -> r) -> (r -> s) -> s -> b
invertible (#) f g a = g (f a) # a
monotonic :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> a -> b -> b -> Bool
monotonic t a1 a2 b1 b2 = monotonicL t a1 a2 b1 b2 && monotonicR t a1 a2 b1 b2
monotonicR :: (Preorder a, Preorder b) => ConnR a b -> a -> a -> b -> b -> Bool
monotonicR (ConnR f g) a1 a2 b1 b2 = monotone (<~) (<~) g a1 a2 && monotone (<~) (<~) f b1 b2
monotonicL :: (Preorder a, Preorder b) => ConnL a b -> a -> a -> b -> b -> Bool
monotonicL (ConnL f g) a1 a2 b1 b2 = monotone (<~) (<~) f a1 a2 && monotone (<~) (<~) g b1 b2
monotone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool
monotone (#) (%) f a b = a # b ==> f a % f b
idempotent :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> b -> Bool
idempotent t a b = idempotentL t a b && idempotentR t a b
idempotentL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool
idempotentL c@(ConnL f g) a b = projective (~~) g (upper1 c id) b && projective (~~) f (ceiling1 c id) a
idempotentR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool
idempotentR c@(ConnR f g) a b = projective (~~) g (floor1 c id) a && projective (~~) f (lower1 c id) b
projective :: Rel s b -> (r -> s) -> (s -> s) -> r -> b
projective (#) f g r = g (f r) # f r