{-# LANGUAGE GADTs, TypeFamilies, PatternSynonyms, ScopedTypeVariables, RankNTypes, TypeOperators #-}
module Data.Category.Preorder where

import Prelude hiding ((.), id, Functor)

import Data.Category
import Data.Category.Limit
import Data.Category.CartesianClosed
import Data.Category.Functor
import Data.Category.Adjunction
import Data.Category.Enriched
import Data.Category.Enriched.Functor
import Data.Category.Enriched.Limit hiding (HasEnds(..))

data Preorder a x y where
  (:<=:) :: a -> a -> Preorder a x y

pattern Obj :: a -> Preorder a x y
pattern $bObj :: forall a x y. a -> Preorder a x y
$mObj :: forall {r} {a} {x} {y}.
Preorder a x y -> (a -> r) -> ((# #) -> r) -> r
Obj a <- a :<=: _ where
  Obj a
a = a
a forall a x y. a -> a -> Preorder a x y
:<=: a
a
{-# COMPLETE Obj #-} -- Note: only complete for identity arrows `Obj Preorder a`

unObj :: Obj (Preorder a) x -> a
unObj :: forall a x. Obj (Preorder a) x -> a
unObj (Obj a
a) = a
a

instance Eq a => Category (Preorder a) where
  src :: forall a b. Preorder a a b -> Obj (Preorder a) a
src (a
s :<=: a
_) = forall a x y. a -> Preorder a x y
Obj a
s
  tgt :: forall a b. Preorder a a b -> Obj (Preorder a) b
tgt (a
_ :<=: a
t) = forall a x y. a -> Preorder a x y
Obj a
t
  (a
b :<=: a
c) . :: forall b c a. Preorder a b c -> Preorder a a b -> Preorder a a c
. (a
a :<=: a
b') = if a
b forall a. Eq a => a -> a -> Bool
== a
b' then a
a forall a x y. a -> a -> Preorder a x y
:<=: a
c else forall a. HasCallStack => [Char] -> a
error [Char]
"Invalid composition"

instance (Eq a, Bounded a) => HasInitialObject (Preorder a) where
  type InitialObject (Preorder a) = ()
  initialObject :: Obj (Preorder a) (InitialObject (Preorder a))
initialObject = forall a x y. a -> Preorder a x y
Obj forall a. Bounded a => a
minBound
  initialize :: forall a.
Obj (Preorder a) a -> Preorder a (InitialObject (Preorder a)) a
initialize (Obj a
a) = forall a. Bounded a => a
minBound forall a x y. a -> a -> Preorder a x y
:<=: a
a

instance (Eq a, Bounded a) => HasTerminalObject (Preorder a) where
  type TerminalObject (Preorder a) = ()
  terminalObject :: Obj (Preorder a) (TerminalObject (Preorder a))
terminalObject = forall a x y. a -> Preorder a x y
Obj forall a. Bounded a => a
maxBound
  terminate :: forall a.
Obj (Preorder a) a -> Preorder a a (TerminalObject (Preorder a))
terminate (Obj a
a) = a
a forall a x y. a -> a -> Preorder a x y
:<=: forall a. Bounded a => a
maxBound

instance Ord a => HasBinaryProducts (Preorder a) where
  type BinaryProduct (Preorder a) x y = ()
  proj1 :: forall x y.
Obj (Preorder a) x
-> Obj (Preorder a) y
-> Preorder a (BinaryProduct (Preorder a) x y) x
proj1 (Obj a
a) (Obj a
b) = forall a. Ord a => a -> a -> a
min a
a a
b forall a x y. a -> a -> Preorder a x y
:<=: a
a
  proj2 :: forall x y.
Obj (Preorder a) x
-> Obj (Preorder a) y
-> Preorder a (BinaryProduct (Preorder a) x y) y
proj2 (Obj a
a) (Obj a
b) = forall a. Ord a => a -> a -> a
min a
a a
b forall a x y. a -> a -> Preorder a x y
:<=: a
b
  (a
a :<=: a
x) &&& :: forall a x y.
Preorder a a x
-> Preorder a a y -> Preorder a a (BinaryProduct (Preorder a) x y)
&&& (a
_a :<=: a
y) = a
a forall a x y. a -> a -> Preorder a x y
:<=: forall a. Ord a => a -> a -> a
min a
x a
y

instance Ord a => HasBinaryCoproducts (Preorder a) where
  type BinaryCoproduct (Preorder a) x y = ()
  inj1 :: forall x y.
Obj (Preorder a) x
-> Obj (Preorder a) y
-> Preorder a x (BinaryCoproduct (Preorder a) x y)
inj1 (Obj a
a) (Obj a
b) = a
a forall a x y. a -> a -> Preorder a x y
:<=: forall a. Ord a => a -> a -> a
max a
a a
b
  inj2 :: forall x y.
Obj (Preorder a) x
-> Obj (Preorder a) y
-> Preorder a y (BinaryCoproduct (Preorder a) x y)
inj2 (Obj a
a) (Obj a
b) = a
b forall a x y. a -> a -> Preorder a x y
:<=: forall a. Ord a => a -> a -> a
max a
a a
b
  (a
x :<=: a
a) ||| :: forall x a y.
Preorder a x a
-> Preorder a y a
-> Preorder a (BinaryCoproduct (Preorder a) x y) a
||| (a
y :<=: a
_a) = forall a. Ord a => a -> a -> a
max a
x a
y forall a x y. a -> a -> Preorder a x y
:<=: a
a

-- | `ordExp a b` is the largest x such that min x a <= b
ordExp :: (Ord a, Bounded a) => a -> a -> a
ordExp :: forall a. (Ord a, Bounded a) => a -> a -> a
ordExp a
a a
b = if a
a forall a. Ord a => a -> a -> Bool
<= a
b then forall a. Bounded a => a
maxBound else a
b

instance (Ord a, Bounded a) => CartesianClosed (Preorder a) where
  type Exponential (Preorder a) x y = ()
  apply :: forall y z.
Obj (Preorder a) y
-> Obj (Preorder a) z
-> Preorder
     a (BinaryProduct (Preorder a) (Exponential (Preorder a) y z) y) z
apply (Obj a
a) (Obj a
b) = forall a. Ord a => a -> a -> a
min (forall a. (Ord a, Bounded a) => a -> a -> a
ordExp a
a a
b) a
a forall a x y. a -> a -> Preorder a x y
:<=: a
b
  tuple :: forall y z.
Obj (Preorder a) y
-> Obj (Preorder a) z
-> Preorder
     a z (Exponential (Preorder a) y (BinaryProduct (Preorder a) z y))
tuple (Obj a
a) (Obj a
b) = a
b forall a x y. a -> a -> Preorder a x y
:<=: forall a. (Ord a, Bounded a) => a -> a -> a
ordExp a
a (forall a. Ord a => a -> a -> a
min a
a a
b)
  (a
z1 :<=: a
z2) ^^^ :: forall z1 z2 y2 y1.
Preorder a z1 z2
-> Preorder a y2 y1
-> Preorder
     a (Exponential (Preorder a) y1 z1) (Exponential (Preorder a) y2 z2)
^^^ (a
y2 :<=: a
y1) = forall a. (Ord a, Bounded a) => a -> a -> a
ordExp a
y1 a
z1 forall a x y. a -> a -> Preorder a x y
:<=: forall a. (Ord a, Bounded a) => a -> a -> a
ordExp a
y2 a
z2


class Category k => EnumObjs k where
  enumObjs :: (forall a. Obj k a -> r) -> [r]

glb :: (Ord a, Bounded a) => [a] -> a
glb :: forall a. (Ord a, Bounded a) => [a] -> a
glb [] = forall a. Bounded a => a
maxBound
glb [a]
xs = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [a]
xs


type End' t = ()
end
  :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a)
  => t -> Obj (Preorder a) (End' t)
end :: forall (k :: * -> * -> *) t a.
(VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a,
 Bounded a) =>
t -> Obj (Preorder a) ()
end t
t = forall a x y. a -> Preorder a x y
Obj forall a b. (a -> b) -> a -> b
$ forall a. (Ord a, Bounded a) => [a] -> a
glb (forall (k :: * -> * -> *) r.
EnumObjs k =>
(forall a. Obj k a -> r) -> [r]
enumObjs (\Obj k a
a -> forall a x. Obj (Preorder a) x -> a
unObj (forall (v :: * -> * -> *) a b. Self v a b -> v a b
getSelf (t
t forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% (forall (k :: * -> * -> *) a b. k b a -> EOp k a b
EOp Obj k a
a forall (k1 :: * -> * -> *) (k2 :: * -> * -> *) a1 a2.
(V k1 ~ V k2) =>
Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)
:<>: Obj k a
a)))))

endCounit
  :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a)
  => t -> Obj k b -> Preorder a (End' t) (t :%% (b, b))
endCounit :: forall (k :: * -> * -> *) t a b.
(VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a,
 Bounded a) =>
t -> Obj k b -> Preorder a () (t :%% (b, b))
endCounit t
t Obj k b
a = forall a x. Obj (Preorder a) x -> a
unObj (forall (k :: * -> * -> *) t a.
(VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a,
 Bounded a) =>
t -> Obj (Preorder a) ()
end t
t) forall a x y. a -> a -> Preorder a x y
:<=: forall a x. Obj (Preorder a) x -> a
unObj (forall (v :: * -> * -> *) a b. Self v a b -> v a b
getSelf (t
t forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% (forall (k :: * -> * -> *) a b. k b a -> EOp k a b
EOp Obj k b
a forall (k1 :: * -> * -> *) (k2 :: * -> * -> *) a1 a2.
(V k1 ~ V k2) =>
Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)
:<>: Obj k b
a)))

endFactorizer
  :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a)
  => t -> Obj (Preorder a) x -> (forall b. Obj k b -> Preorder a x (t :%% (b, b))) -> Preorder a x (End' t)
endFactorizer :: forall (k :: * -> * -> *) t a x.
(VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a,
 Bounded a) =>
t
-> Obj (Preorder a) x
-> (forall b. Obj k b -> Preorder a x (t :%% (b, b)))
-> Preorder a x ()
endFactorizer t
_ (Obj a
x) forall b. Obj k b -> Preorder a x (t :%% (b, b))
f = a
x forall a x y. a -> a -> Preorder a x y
:<=: forall a. (Ord a, Bounded a) => [a] -> a
glb (forall (k :: * -> * -> *) r.
EnumObjs k =>
(forall a. Obj k a -> r) -> [r]
enumObjs (\Obj k a
b -> case forall b. Obj k b -> Preorder a x (t :%% (b, b))
f Obj k a
b of a
_ :<=: a
tbb -> a
tbb))


data Floor = Floor
instance Functor Floor where
  type Dom Floor = Preorder Double
  type Cod Floor = Preorder Integer
  type Floor :% a = ()
  Floor
Floor % :: forall a b.
Floor -> Dom Floor a b -> Cod Floor (Floor :% a) (Floor :% b)
% (Double
a :<=: Double
b) = forall a b. (RealFrac a, Integral b) => a -> b
floor Double
a forall a x y. a -> a -> Preorder a x y
:<=: forall a b. (RealFrac a, Integral b) => a -> b
floor Double
b

data FromInteger = FromInteger
instance Functor FromInteger where
  type Dom FromInteger = Preorder Integer
  type Cod FromInteger = Preorder Double
  type FromInteger :% a = ()
  FromInteger
FromInteger % :: forall a b.
FromInteger
-> Dom FromInteger a b
-> Cod FromInteger (FromInteger :% a) (FromInteger :% b)
% (Integer
a :<=: Integer
b) = forall a. Num a => Integer -> a
fromInteger Integer
a forall a x y. a -> a -> Preorder a x y
:<=: forall a. Num a => Integer -> a
fromInteger Integer
b

floorGaloisConnection :: Adjunction (Preorder Double) (Preorder Integer) FromInteger Floor
floorGaloisConnection :: Adjunction (Preorder Double) (Preorder Integer) FromInteger Floor
floorGaloisConnection = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunction FromInteger
FromInteger Floor
Floor
  (\(Obj Integer
a) (Double
_fromIntegerA :<=: Double
b) -> Integer
a forall a x y. a -> a -> Preorder a x y
:<=: forall a b. (RealFrac a, Integral b) => a -> b
floor Double
b)
  (\(Obj Double
b) (Integer
a :<=: Integer
_floorB) -> forall a. Num a => Integer -> a
fromInteger Integer
a forall a x y. a -> a -> Preorder a x y
:<=: Double
b)