Monotonic.hs

module SubHask.Category.Trans.Monotonic
     ( Mon
     , unsafeProveMon

     -- * The MonT transformer
     , MonT (..)
     , unsafeProveMonT

     )
    where

import SubHask.Category
import SubHask.Algebra
import SubHask.SubType

data IncreasingT cat (a :: *) (b :: *) where
    IncreasingT :: (Ord_ a, Ord_ b) => cat a b -> IncreasingT cat a b

mkMutable [t| forall cat a b. IncreasingT cat a b |]

instance Category cat => Category (IncreasingT cat) where
    type ValidCategory (IncreasingT cat) a = (ValidCategory cat a, Ord_ a)
    id = IncreasingT id
    (IncreasingT f).(IncreasingT g) = IncreasingT $ f.g

instance Sup a b c => Sup (IncreasingT a) b c
instance Sup b a c => Sup a (IncreasingT b) c
instance (subcat <: cat) => IncreasingT subcat <: cat where
    embedType_ = Embed2 (\ (IncreasingT f) -> embedType2 f)

instance Semigroup (cat a b) => Semigroup (IncreasingT cat a b) where
    (IncreasingT f)+(IncreasingT g) = IncreasingT $ f+g

instance Abelian (cat a b) => Abelian (IncreasingT cat a b) where

instance Provable (IncreasingT Hask) where
    f $$ a = ProofOf $ (f $ unProofOf a)

newtype instance ProofOf (IncreasingT cat) a = ProofOf { unProofOf :: ProofOf_ cat a }

mkMutable [t| forall a cat. ProofOf (IncreasingT cat) a |]

instance Semigroup (ProofOf_ cat a) => Semigroup (ProofOf (IncreasingT cat) a) where
    (ProofOf a1)+(ProofOf a2) = ProofOf (a1+a2)

instance Abelian (ProofOf_ cat a) => Abelian (ProofOf (IncreasingT cat) a)

type Increasing a = Increasing_ a
type family Increasing_ a where
    Increasing_ ( (cat :: * -> * -> *) a b) = IncreasingT cat a b

proveIncreasing ::
    ( Ord_ a
    , Ord_ b
    ) => (ProofOf (IncreasingT Hask) a -> ProofOf (IncreasingT Hask) b) -> Increasing (a -> b)
proveIncreasing f = unsafeProveIncreasing $ \a -> unProofOf $ f $ ProofOf a

instance (Ord_ a, Ord_ b) => Hask (ProofOf (IncreasingT Hask) a) (ProofOf (IncreasingT Hask) b) <: (IncreasingT Hask) a b where
    embedType_ = Embed0 proveIncreasing

unsafeProveIncreasing ::
    ( Ord_ a
    , Ord_ b
    ) => (a -> b) -> Increasing (a -> b)
unsafeProveIncreasing = IncreasingT

-- | A convenient specialization of "MonT" and "Hask"
type Mon = MonT Hask

type ValidMon a = Ord a

data MonT cat (a :: *) (b :: *) where
    MonT :: (ValidMon a, ValidMon b) => cat a b -> MonT cat a b

unsafeProveMonT :: (ValidMon a, ValidMon b) => cat a b -> MonT cat a b
unsafeProveMonT = MonT

unsafeProveMon :: (ValidMon a, ValidMon b) => cat a b -> MonT cat a b
unsafeProveMon = MonT

instance Category cat => Category (MonT cat) where
    type ValidCategory (MonT cat) a = (ValidCategory cat a, ValidMon a)
    id = MonT id
    (MonT f).(MonT g) = MonT $ f.g

instance Sup a b c => Sup (MonT a) b c
instance Sup b a c => Sup a (MonT b) c
instance (subcat <: cat) => MonT subcat <: cat where
    embedType_ = Embed2 (\ (MonT f) -> embedType2 f)