{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeOperators, GADTs, KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances, MultiParamTypeClasses #-} -- for Functor instance
{-# OPTIONS_GHC -Wall #-}

{-# OPTIONS_GHC -fno-warn-unused-imports #-} -- TEMP
-- {-# OPTIONS_GHC -fno-warn-unused-binds   #-} -- TEMP

----------------------------------------------------------------------
-- |
-- Module      :  ConCat.Demand
-- 
-- Maintainer  :  conal@conal.net
-- Stability   :  experimental
-- 
-- Demand algebra
----------------------------------------------------------------------

-- TODO: Use Dual?

module ConCat.Demand {- (Demand(..),demand,(:-?)(..)) -} where

import Prelude hiding (id,(.),curry,uncurry,const)
import qualified Prelude as P

import Control.Applicative (liftA2)

import Control.Newtype.Generics (Newtype(..))

import ConCat.Misc ((:*),(:+),Unop,inNew,inNew2)
import ConCat.Category

-- | Demand pattern
data Demand :: * -> * where
  NoneD  :: Demand a
  (:***) :: Demand a -> Demand b -> Demand (a :* b)
  (:+++) :: Demand a -> Demand b -> Demand (a :+ b)
  (:~>)  :: Demand a -> Demand b -> Demand (a -> b)
  AllD   :: Demand a

deriving instance Show (Demand a)

{--------------------------------------------------------------------
    Semantics
--------------------------------------------------------------------}

-- | Semantic function. Extract just the demanded information.
demand :: Demand a -> Unop a
demand :: forall a. Demand a -> Unop a
demand Demand a
NoneD        = Unop a
forall a. Unop a
nothing
demand (Demand a
ra :*** Demand b
rb) = Demand a -> a -> a
forall a. Demand a -> Unop a
demand Demand a
ra (a -> a) -> (b -> b) -> (a, b) -> (a, b)
forall a b c d.
Ok4 (->) a b c d =>
(a -> c) -> (b -> d) -> Prod (->) a b -> Prod (->) c d
forall (k :: * -> * -> *) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (Prod (->) a b) (Prod (->) c d)
*** Demand b -> b -> b
forall a. Demand a -> Unop a
demand Demand b
rb
demand (Demand a
ra :+++ Demand b
rb) = Demand a -> a -> a
forall a. Demand a -> Unop a
demand Demand a
ra (a -> a) -> (b -> b) -> Either a b -> Either a b
forall a b c d.
Ok4 (->) a b c d =>
(c -> a) -> (d -> b) -> Coprod (->) c d -> Coprod (->) a b
forall (k :: * -> * -> *) a b c d.
(MonoidalSCat k, Ok4 k a b c d) =>
k c a -> k d b -> k (Coprod (->) c d) (Coprod (->) a b)
+++ Demand b -> b -> b
forall a. Demand a -> Unop a
demand Demand b
rb
demand (Demand a
ra :~>  Demand b
rb) = Demand a -> a -> a
forall a. Demand a -> Unop a
demand Demand a
ra (a -> a) -> (b -> b) -> (a -> b) -> a -> b
forall (k :: * -> * -> *) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k a' a -> k b b' -> k a b -> k a' b'
~>  Demand b -> b -> b
forall a. Demand a -> Unop a
demand Demand b
rb
demand Demand a
AllD         = Unop a
forall a. Ok (->) a => a -> a
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id

nothing :: Unop a
nothing :: forall a. Unop a
nothing = a -> a -> a
forall a b. a -> b -> a
P.const (String -> a
forall a. HasCallStack => String -> a
error String
"empty demand pulled")

-- I'm uneasy about handling of functions. Does demand ra need to be inverted?

-- | Alternative Semantic function. Splits into needed info and complement.
split :: Demand a -> (Unop a,Unop a)
split :: forall a. Demand a -> (Unop a, Unop a)
split Demand a
NoneD        = (Unop a
forall a. Unop a
nothing,Unop a
forall a. Ok (->) a => a -> a
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id)
split (Demand a
ra :*** Demand b
rb) = (Unop a -> Unop b -> Unop a)
-> Demand a -> Demand b -> (Unop a, Unop a)
forall a b c.
(Unop a -> Unop b -> c) -> Demand a -> Demand b -> (c, c)
lift2Split Unop a -> Unop b -> Unop a
Unop a -> Unop b -> (a, b) -> (a, b)
forall a b c d.
Ok4 (->) a b c d =>
(a -> c) -> (b -> d) -> Prod (->) a b -> Prod (->) c d
forall (k :: * -> * -> *) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (Prod (->) a b) (Prod (->) c d)
(***) Demand a
ra Demand b
rb
split (Demand a
ra :+++ Demand b
rb) = (Unop a -> Unop b -> Unop a)
-> Demand a -> Demand b -> (Unop a, Unop a)
forall a b c.
(Unop a -> Unop b -> c) -> Demand a -> Demand b -> (c, c)
lift2Split Unop a -> Unop b -> Unop a
Unop a -> Unop b -> Either a b -> Either a b
forall a b c d.
Ok4 (->) a b c d =>
(c -> a) -> (d -> b) -> Coprod (->) c d -> Coprod (->) a b
forall (k :: * -> * -> *) a b c d.
(MonoidalSCat k, Ok4 k a b c d) =>
k c a -> k d b -> k (Coprod (->) c d) (Coprod (->) a b)
(+++) Demand a
ra Demand b
rb
split (Demand a
ra :~>  Demand b
rb) = (Unop a -> Unop b -> Unop a)
-> Demand a -> Demand b -> (Unop a, Unop a)
forall a b c.
(Unop a -> Unop b -> c) -> Demand a -> Demand b -> (c, c)
lift2Split Unop a -> Unop b -> Unop a
Unop a -> Unop b -> (a -> b) -> a -> b
forall (k :: * -> * -> *) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k a' a -> k b b' -> k a b -> k a' b'
(~>)  Demand a
ra Demand b
rb
split Demand a
AllD         = (Unop a
forall a. Ok (->) a => a -> a
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id,Unop a
forall a. Unop a
nothing)

-- Alternative definition
_split :: Demand a -> (Unop a,Unop a)
_split :: forall a. Demand a -> (Unop a, Unop a)
_split = Demand a -> Unop a
forall a. Demand a -> Unop a
demand (Demand a -> Unop a)
-> (Demand a -> Unop a) -> Demand a -> (Unop a, Unop a)
forall (k :: * -> * -> *) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& Demand a -> Unop a
forall a. Demand a -> Unop a
demand (Demand a -> Unop a)
-> (Demand a -> Demand a) -> Demand a -> Unop a
forall b c a. Ok3 (->) a b c => (b -> c) -> (a -> b) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Demand a -> Demand a
forall a. Unop (Demand a)
complementD

lift2Split :: (Unop a -> Unop b -> c) -> Demand a -> Demand b -> (c, c)
lift2Split :: forall a b c.
(Unop a -> Unop b -> c) -> Demand a -> Demand b -> (c, c)
lift2Split Unop a -> Unop b -> c
(@@) Demand a
ra Demand b
rb = (Unop a
pa Unop a -> Unop b -> c
@@ Unop b
pb, Unop a
qa Unop a -> Unop b -> c
@@ Unop b
qb)
  where
    (Unop a
pa,Unop a
qa) = Demand a -> (Unop a, Unop a)
forall a. Demand a -> (Unop a, Unop a)
split Demand a
ra
    (Unop b
pb,Unop b
qb) = Demand b -> (Unop b, Unop b)
forall a. Demand a -> (Unop a, Unop a)
split Demand b
rb

-- | Complement of Demand
complementD :: Unop (Demand a)
complementD :: forall a. Unop (Demand a)
complementD Demand a
NoneD        = Demand a
forall a. Demand a
AllD
complementD (Demand a
ra :*** Demand b
rb) = Unop (Demand a)
forall a. Unop (Demand a)
complementD Demand a
ra Demand a -> Demand b -> Demand (a, b)
forall a b. Demand a -> Demand b -> Demand (a :* b)
*: Unop (Demand b)
forall a. Unop (Demand a)
complementD Demand b
rb
complementD (Demand a
ra :+++ Demand b
rb) = Unop (Demand a)
forall a. Unop (Demand a)
complementD Demand a
ra Demand a -> Demand b -> Demand (Either a b)
forall a b. Demand a -> Demand b -> Demand (a :+ b)
+: Unop (Demand b)
forall a. Unop (Demand a)
complementD Demand b
rb
complementD (Demand a
ra :~> Demand b
rb)  = Unop (Demand a)
forall a. Unop (Demand a)
complementD Demand a
ra Demand a -> Demand b -> Demand (a -> b)
forall a b. Demand a -> Demand b -> Demand (a -> b)
>: Unop (Demand b)
forall a. Unop (Demand a)
complementD Demand b
rb
complementD Demand a
AllD         = Demand a
forall a. Demand a
NoneD

{--------------------------------------------------------------------
    Smart constructors
--------------------------------------------------------------------}

-- | Product demand
(*:) :: Demand a -> Demand b -> Demand (a :* b)
*: :: forall a b. Demand a -> Demand b -> Demand (a :* b)
(*:) = Unop (Demand a -> Demand b -> Demand (a, b))
forall a b (op :: * -> * -> *).
Unop (Demand a -> Demand b -> Demand (op a b))
combineD Demand a -> Demand b -> Demand (a, b)
forall a b. Demand a -> Demand b -> Demand (a :* b)
(:***)

-- | Sum demand
(+:) :: Demand a -> Demand b -> Demand (a :+ b)
+: :: forall a b. Demand a -> Demand b -> Demand (a :+ b)
(+:) = Unop (Demand a -> Demand b -> Demand (Either a b))
forall a b (op :: * -> * -> *).
Unop (Demand a -> Demand b -> Demand (op a b))
combineD Demand a -> Demand b -> Demand (Either a b)
forall a b. Demand a -> Demand b -> Demand (a :+ b)
(:+++)

-- | Function demand
(>:) :: Demand a -> Demand b -> Demand (a -> b)
>: :: forall a b. Demand a -> Demand b -> Demand (a -> b)
(>:) = Unop (Demand a -> Demand b -> Demand (a -> b))
forall a b (op :: * -> * -> *).
Unop (Demand a -> Demand b -> Demand (op a b))
combineD Demand a -> Demand b -> Demand (a -> b)
forall a b. Demand a -> Demand b -> Demand (a -> b)
(:~>)

-- | Building block for smart constructor, assuming that @NoneD `op` NoneD ==
-- NoneD@ and @AllD `op` AllD == AllD@.
combineD :: Unop (Demand a -> Demand b -> Demand (a `op` b))
combineD :: forall a b (op :: * -> * -> *).
Unop (Demand a -> Demand b -> Demand (op a b))
combineD  Demand a -> Demand b -> Demand (op a b)
_   Demand a
NoneD Demand b
NoneD = Demand (op a b)
forall a. Demand a
NoneD
combineD  Demand a -> Demand b -> Demand (op a b)
_   Demand a
AllD  Demand b
AllD  = Demand (op a b)
forall a. Demand a
AllD
combineD Demand a -> Demand b -> Demand (op a b)
(@@) Demand a
ra    Demand b
rb    = Demand a
ra Demand a -> Demand b -> Demand (op a b)
@@ Demand b
rb

{--------------------------------------------------------------------
    Construction & destruction
--------------------------------------------------------------------}

pairD :: (Demand a :* Demand b) -> Demand (a :* b)
pairD :: forall a b. (Demand a :* Demand b) -> Demand (a :* b)
pairD = (Demand a -> Exp (->) (Demand b) (Demand (a :* b)))
-> (Demand a, Demand b) -> Demand (a :* b)
forall a b c.
Ok3 (->) a b c =>
(a -> Exp (->) b c) -> Prod (->) a b -> c
forall (k :: * -> * -> *) a b c.
(ClosedCat k, Ok3 k a b c) =>
k a (Exp (->) b c) -> k (Prod (->) a b) c
uncurry Demand a -> Exp (->) (Demand b) (Demand (a :* b))
forall a b. Demand a -> Demand b -> Demand (a :* b)
(*:)

unpairD :: Demand (a :* b) -> (Demand a :* Demand b)
unpairD :: forall a b. Demand (a :* b) -> Demand a :* Demand b
unpairD Demand (a :* b)
NoneD        = (Demand a
forall a. Demand a
NoneD,Demand b
forall a. Demand a
NoneD)
unpairD (Demand a
ra :*** Demand b
rb) = (Demand a
Demand a
ra   ,Demand b
Demand b
rb   )
unpairD Demand (a :* b)
AllD         = (Demand a
forall a. Demand a
AllD ,Demand b
forall a. Demand a
AllD )

inUnpairD :: (Demand a' :* Demand b' -> Demand a :* Demand b)
          -> Demand (a' :* b') -> Demand (a :* b)
inUnpairD :: forall a' b' a b.
((Demand a' :* Demand b') -> Demand a :* Demand b)
-> Demand (a' :* b') -> Demand (a :* b)
inUnpairD = Demand (a' :* b') -> Demand a' :* Demand b'
forall a b. Demand (a :* b) -> Demand a :* Demand b
unpairD (Demand (a' :* b') -> Demand a' :* Demand b')
-> ((Demand a :* Demand b) -> Demand (a :* b))
-> ((Demand a' :* Demand b') -> Demand a :* Demand b)
-> Demand (a' :* b')
-> Demand (a :* b)
forall (k :: * -> * -> *) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k a' a -> k b b' -> k a b -> k a' b'
~> (Demand a :* Demand b) -> Demand (a :* b)
forall a b. (Demand a :* Demand b) -> Demand (a :* b)
pairD


plusD :: (Demand a, Demand b) -> Demand (a :+ b)
plusD :: forall a b. (Demand a, Demand b) -> Demand (a :+ b)
plusD = (Demand a -> Exp (->) (Demand b) (Demand (a :+ b)))
-> (Demand a, Demand b) -> Demand (a :+ b)
forall a b c.
Ok3 (->) a b c =>
(a -> Exp (->) b c) -> Prod (->) a b -> c
forall (k :: * -> * -> *) a b c.
(ClosedCat k, Ok3 k a b c) =>
k a (Exp (->) b c) -> k (Prod (->) a b) c
uncurry Demand a -> Exp (->) (Demand b) (Demand (a :+ b))
forall a b. Demand a -> Demand b -> Demand (a :+ b)
(+:)

unplusD :: Demand (a :+ b) -> (Demand a , Demand b)
unplusD :: forall a b. Demand (a :+ b) -> (Demand a, Demand b)
unplusD Demand (a :+ b)
NoneD        = (Demand a
forall a. Demand a
NoneD, Demand b
forall a. Demand a
NoneD)
unplusD (Demand a
ra :+++ Demand b
rb) = (Demand a
Demand a
ra   , Demand b
Demand b
rb   )
unplusD Demand (a :+ b)
AllD         = (Demand a
forall a. Demand a
AllD , Demand b
forall a. Demand a
AllD )

inUnplusD :: (Demand a' :* Demand b' -> Demand a :* Demand b)
          -> Demand (a' :+ b') -> Demand (a :+ b)
inUnplusD :: forall a' b' a b.
((Demand a' :* Demand b') -> Demand a :* Demand b)
-> Demand (a' :+ b') -> Demand (a :+ b)
inUnplusD = Demand (a' :+ b') -> Demand a' :* Demand b'
forall a b. Demand (a :+ b) -> (Demand a, Demand b)
unplusD (Demand (a' :+ b') -> Demand a' :* Demand b')
-> ((Demand a :* Demand b) -> Demand (a :+ b))
-> ((Demand a' :* Demand b') -> Demand a :* Demand b)
-> Demand (a' :+ b')
-> Demand (a :+ b)
forall (k :: * -> * -> *) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k a' a -> k b b' -> k a b -> k a' b'
~> (Demand a :* Demand b) -> Demand (a :+ b)
forall a b. (Demand a, Demand b) -> Demand (a :+ b)
plusD

funD :: (Demand a, Demand b) -> Demand (a -> b)
funD :: forall a b. (Demand a, Demand b) -> Demand (a -> b)
funD = (Demand a -> Exp (->) (Demand b) (Demand (a -> b)))
-> (Demand a, Demand b) -> Demand (a -> b)
forall a b c.
Ok3 (->) a b c =>
(a -> Exp (->) b c) -> Prod (->) a b -> c
forall (k :: * -> * -> *) a b c.
(ClosedCat k, Ok3 k a b c) =>
k a (Exp (->) b c) -> k (Prod (->) a b) c
uncurry Demand a -> Exp (->) (Demand b) (Demand (a -> b))
forall a b. Demand a -> Demand b -> Demand (a -> b)
(>:)

unfunD :: Demand (a -> b) -> (Demand a, Demand b)
unfunD :: forall a b. Demand (a -> b) -> (Demand a, Demand b)
unfunD Demand (a -> b)
NoneD       = (Demand a
forall a. Demand a
NoneD,Demand b
forall a. Demand a
NoneD)
unfunD (Demand a
ra :~> Demand b
rb) = (Demand a
Demand a
ra, Demand b
Demand b
rb)
unfunD Demand (a -> b)
AllD        = (Demand a
forall a. Demand a
AllD,Demand b
forall a. Demand a
AllD)

inUnfunD :: ((Demand a, Demand b) -> (Demand a', Demand b'))
         -> (Demand (a -> b) -> Demand (a' -> b'))
inUnfunD :: forall a b a' b'.
((Demand a, Demand b) -> (Demand a', Demand b'))
-> Demand (a -> b) -> Demand (a' -> b')
inUnfunD = Demand (a -> b) -> (Demand a, Demand b)
forall a b. Demand (a -> b) -> (Demand a, Demand b)
unfunD (Demand (a -> b) -> (Demand a, Demand b))
-> ((Demand a', Demand b') -> Demand (a' -> b'))
-> ((Demand a, Demand b) -> (Demand a', Demand b'))
-> Demand (a -> b)
-> Demand (a' -> b')
forall (k :: * -> * -> *) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k a' a -> k b b' -> k a b -> k a' b'
~> (Demand a', Demand b') -> Demand (a' -> b')
forall a b. (Demand a, Demand b) -> Demand (a -> b)
funD

mergeD :: Demand (a :* a) -> Demand a
mergeD :: forall a. Demand (a :* a) -> Demand a
mergeD = (Demand a -> Exp (->) (Demand a) (Demand a))
-> Prod (->) (Demand a) (Demand a) -> Demand a
forall a b c.
Ok3 (->) a b c =>
(a -> Exp (->) b c) -> Prod (->) a b -> c
forall (k :: * -> * -> *) a b c.
(ClosedCat k, Ok3 k a b c) =>
k a (Exp (->) b c) -> k (Prod (->) a b) c
uncurry Demand a -> Exp (->) (Demand a) (Demand a)
forall a. Demand a -> Demand a -> Demand a
lubD (Prod (->) (Demand a) (Demand a) -> Demand a)
-> (Demand (a :* a) -> Prod (->) (Demand a) (Demand a))
-> Demand (a :* a)
-> Demand a
forall b c a. Ok3 (->) a b c => (b -> c) -> (a -> b) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Demand (a :* a) -> Prod (->) (Demand a) (Demand a)
forall a b. Demand (a :* b) -> Demand a :* Demand b
unpairD

-- mergeD NoneD        = NoneD
-- mergeD (ra :*** rb) = ra `lubD` rb
-- mergeD AllD         = AllD

{--------------------------------------------------------------------
    Lattice
--------------------------------------------------------------------}

-- Demands form a lattice with bottom = NoneD, top = AllD, and lub & glb as
-- follows. The semantic function preserves lattice structure (is a lattice
-- morphism).

-- | Least upper bound on demands. Specification: 
-- @demand (ra `lubD` rb) == demand ra `lub` demand rb@.
lubD :: Demand a -> Demand a -> Demand a
Demand a
NoneD      lubD :: forall a. Demand a -> Demand a -> Demand a
`lubD` Demand a
a            = Demand a
a
Demand a
a          `lubD` Demand a
NoneD        = Demand a
a
Demand a
AllD       `lubD` Demand a
_            = Demand a
forall a. Demand a
AllD
Demand a
_          `lubD` Demand a
AllD         = Demand a
forall a. Demand a
AllD
(Demand a
a :*** Demand b
b) `lubD` (Demand a
a' :*** Demand b
b') = (Demand a
a Demand a -> Demand a -> Demand a
forall a. Demand a -> Demand a -> Demand a
`lubD` Demand a
Demand a
a') Demand a -> Demand b -> Demand (a, b)
forall a b. Demand a -> Demand b -> Demand (a :* b)
*: (Demand b
b Demand b -> Demand b -> Demand b
forall a. Demand a -> Demand a -> Demand a
`lubD` Demand b
Demand b
b')
(Demand a
a :+++ Demand b
b) `lubD` (Demand a
a' :+++ Demand b
b') = (Demand a
a Demand a -> Demand a -> Demand a
forall a. Demand a -> Demand a -> Demand a
`lubD` Demand a
Demand a
a') Demand a -> Demand b -> Demand (Either a b)
forall a b. Demand a -> Demand b -> Demand (a :+ b)
+: (Demand b
b Demand b -> Demand b -> Demand b
forall a. Demand a -> Demand a -> Demand a
`lubD` Demand b
Demand b
b')
(Demand a
a :~>  Demand b
b) `lubD` (Demand a
a' :~>  Demand b
b') = (Demand a
a Demand a -> Demand a -> Demand a
forall a. Demand a -> Demand a -> Demand a
`lubD` Demand a
Demand a
a') Demand a -> Demand b -> Demand (a -> b)
forall a b. Demand a -> Demand b -> Demand (a -> b)
>: (Demand b
b Demand b -> Demand b -> Demand b
forall a. Demand a -> Demand a -> Demand a
`lubD` Demand b
Demand b
b')

-- | Greatest lower bound on demands. Specification: 
-- @demand (ra `glbD` rb) == demand ra `glb` demand rb@.
glbD :: Demand a -> Demand a -> Demand a
Demand a
NoneD      glbD :: forall a. Demand a -> Demand a -> Demand a
`glbD` Demand a
_            = Demand a
forall a. Demand a
NoneD
Demand a
_          `glbD` Demand a
NoneD        = Demand a
forall a. Demand a
NoneD
Demand a
AllD       `glbD` Demand a
b            = Demand a
b
Demand a
a          `glbD` Demand a
AllD         = Demand a
a
(Demand a
a :*** Demand b
b) `glbD` (Demand a
a' :*** Demand b
b') = (Demand a
a Demand a -> Demand a -> Demand a
forall a. Demand a -> Demand a -> Demand a
`glbD` Demand a
Demand a
a') Demand a -> Demand b -> Demand (a, b)
forall a b. Demand a -> Demand b -> Demand (a :* b)
*: (Demand b
b Demand b -> Demand b -> Demand b
forall a. Demand a -> Demand a -> Demand a
`glbD` Demand b
Demand b
b')
(Demand a
a :+++ Demand b
b) `glbD` (Demand a
a' :+++ Demand b
b') = (Demand a
a Demand a -> Demand a -> Demand a
forall a. Demand a -> Demand a -> Demand a
`glbD` Demand a
Demand a
a') Demand a -> Demand b -> Demand (Either a b)
forall a b. Demand a -> Demand b -> Demand (a :+ b)
+: (Demand b
b Demand b -> Demand b -> Demand b
forall a. Demand a -> Demand a -> Demand a
`glbD` Demand b
Demand b
b')
(Demand a
a :~>  Demand b
b) `glbD` (Demand a
a' :~>  Demand b
b') = (Demand a
a Demand a -> Demand a -> Demand a
forall a. Demand a -> Demand a -> Demand a
`glbD` Demand a
Demand a
a') Demand a -> Demand b -> Demand (a -> b)
forall a b. Demand a -> Demand b -> Demand (a -> b)
>: (Demand b
b Demand b -> Demand b -> Demand b
forall a. Demand a -> Demand a -> Demand a
`glbD` Demand b
Demand b
b')

-- The catch-all cases in lubD and glbD are sum/product.
-- Impossible, but GHC doesn't realize. :(

{--------------------------------------------------------------------
    Demand flow arrow
--------------------------------------------------------------------}

infixr 1 :-?

-- | Demand flow category, running counter to value flow
newtype a :-? b = RX (Demand b -> Demand a)

instance Newtype (a :-? b) where
  type O (a :-? b) = Demand b -> Demand a
  pack :: O (a :-? b) -> a :-? b
pack = O (a :-? b) -> a :-? b
(Demand b -> Demand a) -> a :-? b
forall a b. (Demand b -> Demand a) -> a :-? b
RX
  unpack :: (a :-? b) -> O (a :-? b)
unpack (RX Demand b -> Demand a
f) = O (a :-? b)
Demand b -> Demand a
f

instance Category (:-?) where
  id :: forall a. Ok (:-?) a => a :-? a
id  = O (a :-? a) -> a :-? a
forall n. Newtype n => O n -> n
pack O (a :-? a)
Demand a -> Demand a
forall a. Ok (->) a => a -> a
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id
  . :: forall b c a. Ok3 (:-?) a b c => (b :-? c) -> (a :-? b) -> a :-? c
(.) = (O (b :-? c) -> O (a :-? b) -> O (a :-? c))
-> (b :-? c) -> (a :-? b) -> a :-? c
forall p q r.
(Newtype p, Newtype q, Newtype r) =>
(O p -> O q -> O r) -> p -> q -> r
inNew2 (((Demand b -> Demand a)
 -> (Demand c -> Demand b) -> Demand c -> Demand a)
-> (Demand c -> Demand b)
-> (Demand b -> Demand a)
-> Demand c
-> Demand a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Demand b -> Demand a)
-> (Demand c -> Demand b) -> Demand c -> Demand a
forall b c a. Ok3 (->) a b c => (b -> c) -> (a -> b) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
(.))                -- note flow reversal

instance MonoidalPCat (:-?) where
  *** :: forall a b c d.
Ok4 (:-?) a b c d =>
(a :-? c) -> (b :-? d) -> Prod (->) a b :-? Prod (->) c d
(***) = (O (a :-? c) -> O (b :-? d) -> O ((a :* b) :-? (c :* d)))
-> (a :-? c) -> (b :-? d) -> (a :* b) :-? (c :* d)
forall p q r.
(Newtype p, Newtype q, Newtype r) =>
(O p -> O q -> O r) -> p -> q -> r
inNew2 ((O (a :-? c) -> O (b :-? d) -> O ((a :* b) :-? (c :* d)))
 -> (a :-? c) -> (b :-? d) -> (a :* b) :-? (c :* d))
-> (O (a :-? c) -> O (b :-? d) -> O ((a :* b) :-? (c :* d)))
-> (a :-? c)
-> (b :-? d)
-> (a :* b) :-? (c :* d)
forall a b. (a -> b) -> a -> b
$ \ O (a :-? c)
f O (b :-? d)
g -> ((Demand c :* Demand d) -> Demand a :* Demand b)
-> Demand (c :* d) -> Demand (a :* b)
forall a' b' a b.
((Demand a' :* Demand b') -> Demand a :* Demand b)
-> Demand (a' :* b') -> Demand (a :* b)
inUnpairD (O (a :-? c)
Demand c -> Demand a
f (Demand c -> Demand a)
-> (Demand d -> Demand b)
-> (Demand c :* Demand d)
-> Demand a :* Demand b
forall a b c d.
Ok4 (->) a b c d =>
(a -> c) -> (b -> d) -> Prod (->) a b -> Prod (->) c d
forall (k :: * -> * -> *) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (Prod (->) a b) (Prod (->) c d)
*** O (b :-? d)
Demand d -> Demand b
g)
  {-# INLINE (***) #-}

instance BraidedPCat (:-?) where

instance ProductCat (:-?) where
  exl :: forall a b. Ok2 (:-?) a b => Prod (:-?) a b :-? a
exl = O ((a :* b) :-? a) -> (a :* b) :-? a
forall n. Newtype n => O n -> n
pack (Demand a -> Demand b -> Demand (a :* b)
forall a b. Demand a -> Demand b -> Demand (a :* b)
*: Demand b
forall a. Demand a
NoneD)
  exr :: forall a b. Ok2 (:-?) a b => Prod (:-?) a b :-? b
exr = O ((a :* b) :-? b) -> (a :* b) :-? b
forall n. Newtype n => O n -> n
pack (Demand a
forall a. Demand a
NoneD Demand a -> Demand b -> Demand (a :* b)
forall a b. Demand a -> Demand b -> Demand (a :* b)
*:)
  dup :: forall a. Ok (:-?) a => a :-? Prod (:-?) a a
dup = O (a :-? (a :* a)) -> a :-? (a :* a)
forall n. Newtype n => O n -> n
pack O (a :-? (a :* a))
Demand (a :* a) -> Demand a
forall a. Demand (a :* a) -> Demand a
mergeD
  {-# INLINE exl #-}
  {-# INLINE exr #-}
  {-# INLINE dup #-}

instance UnitCat (:-?) where

instance TerminalCat (:-?)

-- need :: Demand () `k` Demand a

instance MonoidalSCat (:-?) where
  +++ :: forall a b c d.
Ok4 (:-?) a b c d =>
(c :-? a) -> (d :-? b) -> Coprod (->) c d :-? Coprod (->) a b
(+++) = (O (c :-? a) -> O (d :-? b) -> O ((c :+ d) :-? (a :+ b)))
-> (c :-? a) -> (d :-? b) -> (c :+ d) :-? (a :+ b)
forall p q r.
(Newtype p, Newtype q, Newtype r) =>
(O p -> O q -> O r) -> p -> q -> r
inNew2 ((O (c :-? a) -> O (d :-? b) -> O ((c :+ d) :-? (a :+ b)))
 -> (c :-? a) -> (d :-? b) -> (c :+ d) :-? (a :+ b))
-> (O (c :-? a) -> O (d :-? b) -> O ((c :+ d) :-? (a :+ b)))
-> (c :-? a)
-> (d :-? b)
-> (c :+ d) :-? (a :+ b)
forall a b. (a -> b) -> a -> b
$ \ O (c :-? a)
f O (d :-? b)
g -> ((Demand a :* Demand b) -> Demand c :* Demand d)
-> Demand (a :+ b) -> Demand (c :+ d)
forall a' b' a b.
((Demand a' :* Demand b') -> Demand a :* Demand b)
-> Demand (a' :+ b') -> Demand (a :+ b)
inUnplusD (O (c :-? a)
Demand a -> Demand c
f (Demand a -> Demand c)
-> (Demand b -> Demand d)
-> (Demand a :* Demand b)
-> Demand c :* Demand d
forall a b c d.
Ok4 (->) a b c d =>
(a -> c) -> (b -> d) -> Prod (->) a b -> Prod (->) c d
forall (k :: * -> * -> *) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (Prod (->) a b) (Prod (->) c d)
*** O (d :-? b)
Demand b -> Demand d
g)
  {-# INLINE (+++) #-}

instance BraidedSCat  (:-?)

instance CoproductCat (:-?) where
  inl :: forall a b. Ok2 (:-?) a b => a :-? Coprod (:-?) a b
inl = O (a :-? (a :+ b)) -> a :-? (a :+ b)
forall n. Newtype n => O n -> n
pack (Prod (->) (Demand a) (Demand b) -> Demand a
forall a b. Ok2 (->) a b => Prod (:-?) a b -> a
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod (:-?) a b) a
exl (Prod (->) (Demand a) (Demand b) -> Demand a)
-> (Demand (a :+ b) -> Prod (->) (Demand a) (Demand b))
-> Demand (a :+ b)
-> Demand a
forall b c a. Ok3 (->) a b c => (b -> c) -> (a -> b) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Demand (a :+ b) -> Prod (->) (Demand a) (Demand b)
forall a b. Demand (a :+ b) -> (Demand a, Demand b)
unplusD)
  inr :: forall a b. Ok2 (:-?) a b => b :-? Coprod (:-?) a b
inr = O (b :-? (a :+ b)) -> b :-? (a :+ b)
forall n. Newtype n => O n -> n
pack (Prod (->) (Demand a) (Demand b) -> Demand b
forall a b. Ok2 (->) a b => Prod (:-?) a b -> b
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod (:-?) a b) b
exr (Prod (->) (Demand a) (Demand b) -> Demand b)
-> (Demand (a :+ b) -> Prod (->) (Demand a) (Demand b))
-> Demand (a :+ b)
-> Demand b
forall b c a. Ok3 (->) a b c => (b -> c) -> (a -> b) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Demand (a :+ b) -> Prod (->) (Demand a) (Demand b)
forall a b. Demand (a :+ b) -> (Demand a, Demand b)
unplusD)
  jam :: forall a. Ok (:-?) a => Coprod (:-?) a a :-? a
jam = O ((a :+ a) :-? a) -> (a :+ a) :-? a
forall n. Newtype n => O n -> n
pack (Prod (->) (Demand a) (Demand a) -> Demand (a :+ a)
forall a b. (Demand a, Demand b) -> Demand (a :+ b)
plusD (Prod (->) (Demand a) (Demand a) -> Demand (a :+ a))
-> (Demand a -> Prod (->) (Demand a) (Demand a))
-> Demand a
-> Demand (a :+ a)
forall b c a. Ok3 (->) a b c => (b -> c) -> (a -> b) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Demand a -> Prod (->) (Demand a) (Demand a)
forall a. Ok (->) a => a -> Prod (:-?) a a
forall (k :: * -> * -> *) a.
(ProductCat k, Ok k a) =>
k a (Prod (:-?) a a)
dup)
  -- (|||) = (inNew2.liftA2) (+:)

instance ConstCat (:-?) a where
  const :: forall a. Ok (:-?) a => ConstObj (:-?) a -> a :-? ConstObj (:-?) a
const ConstObj (:-?) a
_ = O (a :-? ConstObj (:-?) a) -> a :-? ConstObj (:-?) a
forall n. Newtype n => O n -> n
pack (Demand a -> Demand (ConstObj (:-?) a) -> Demand a
forall a. Ok (->) a => Demand a -> a -> Demand a
forall (k :: * -> * -> *) b a.
(ConstCat k (ConstObj k b), Ok k a) =>
ConstObj k b -> k a (ConstObj k b)
const Demand a
forall a. Demand a
NoneD)

instance BottomCat (:-?) a b where
  bottomC :: a :-? b
bottomC = O (a :-? b) -> a :-? b
forall n. Newtype n => O n -> n
pack (Demand a -> Demand b -> Demand a
forall a. Ok (->) a => Demand a -> a -> Demand a
forall (k :: * -> * -> *) b a.
(ConstCat k (ConstObj k b), Ok k a) =>
ConstObj k b -> k a (ConstObj k b)
const Demand a
forall a. Demand a
NoneD)

hyperStrict :: a :-? b
hyperStrict :: forall a b. a :-? b
hyperStrict = O (a :-? b) -> a :-? b
forall n. Newtype n => O n -> n
pack O (a :-? b)
Demand b -> Demand a
forall {a} {a}. Demand a -> Demand a
f
 where
   f :: Demand a -> Demand a
f Demand a
NoneD = Demand a
forall a. Demand a
NoneD
   f Demand a
_     = Demand a
forall a. Demand a
AllD

instance BoolCat (:-?) where
  notC :: BoolOf (:-?) :-? BoolOf (:-?)
notC = O (BoolOf (:-?) :-? BoolOf (:-?)) -> BoolOf (:-?) :-? BoolOf (:-?)
forall n. Newtype n => O n -> n
pack O (BoolOf (:-?) :-? BoolOf (:-?))
Demand (BoolOf (:-?)) -> Demand (BoolOf (:-?))
forall a. Ok (->) a => a -> a
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id
  andC :: Prod (:-?) (BoolOf (:-?)) (BoolOf (:-?)) :-? BoolOf (:-?)
andC = Prod (:-?) (BoolOf (:-?)) (BoolOf (:-?)) :-? BoolOf (:-?)
forall a b. a :-? b
hyperStrict
  orC :: Prod (:-?) (BoolOf (:-?)) (BoolOf (:-?)) :-? BoolOf (:-?)
orC  = Prod (:-?) (BoolOf (:-?)) (BoolOf (:-?)) :-? BoolOf (:-?)
forall a b. a :-? b
hyperStrict
  xorC :: Prod (:-?) (BoolOf (:-?)) (BoolOf (:-?)) :-? BoolOf (:-?)
xorC = Prod (:-?) (BoolOf (:-?)) (BoolOf (:-?)) :-? BoolOf (:-?)
forall a b. a :-? b
hyperStrict

instance EqCat (->) a => EqCat (:-?) a where
  equal :: Prod (:-?) a a :-? BoolOf (:-?)
equal    = Prod (:-?) a a :-? BoolOf (:-?)
forall a b. a :-? b
hyperStrict
  notEqual :: Prod (:-?) a a :-? BoolOf (:-?)
notEqual = Prod (:-?) a a :-? BoolOf (:-?)
forall a b. a :-? b
hyperStrict

instance Ord a => OrdCat (:-?) a where
  lessThan :: Prod (:-?) a a :-? BoolOf (:-?)
lessThan           = Prod (:-?) a a :-? BoolOf (:-?)
forall a b. a :-? b
hyperStrict
  greaterThan :: Prod (:-?) a a :-? BoolOf (:-?)
greaterThan        = Prod (:-?) a a :-? BoolOf (:-?)
forall a b. a :-? b
hyperStrict
  lessThanOrEqual :: Prod (:-?) a a :-? BoolOf (:-?)
lessThanOrEqual    = Prod (:-?) a a :-? BoolOf (:-?)
forall a b. a :-? b
hyperStrict
  greaterThanOrEqual :: Prod (:-?) a a :-? BoolOf (:-?)
greaterThanOrEqual = Prod (:-?) a a :-? BoolOf (:-?)
forall a b. a :-? b
hyperStrict

-- instance MinMaxCat (->) a => MinMaxCat (:-?) a where
--   minC = ...
--   maxC = ...

instance EnumCat (->) a => EnumCat (:-?) a where
  succC :: a :-? a
succC = a :-? a
forall a b. a :-? b
hyperStrict
  predC :: a :-? a
predC = a :-? a
forall a b. a :-? b
hyperStrict

-- The following instances are too conservative for instances over non-flat
-- types, such as tuples and many applicatives.
-- 
-- TODO: rework.

instance NumCat (->) a => NumCat (:-?) a where
  negateC :: a :-? a
negateC = a :-? a
forall a b. a :-? b
hyperStrict
  addC :: Prod (:-?) a a :-? a
addC    = Prod (:-?) a a :-? a
forall a b. a :-? b
hyperStrict
  subC :: Prod (:-?) a a :-? a
subC    = Prod (:-?) a a :-? a
forall a b. a :-? b
hyperStrict
  mulC :: Prod (:-?) a a :-? a
mulC    = Prod (:-?) a a :-? a
forall a b. a :-? b
hyperStrict
  powIC :: Ok (:-?) Int => Prod (:-?) a Int :-? a
powIC   = Prod (:-?) a Int :-? a
forall a b. a :-? b
hyperStrict

instance FractionalCat (->) a => FractionalCat (:-?) a where
  recipC :: a :-? a
recipC  = a :-? a
forall a b. a :-? b
hyperStrict
  divideC :: Prod (:-?) a a :-? a
divideC = Prod (:-?) a a :-? a
forall a b. a :-? b
hyperStrict

instance FloatingCat (->) a => FloatingCat (:-?) a where
  expC :: a :-? a
expC = a :-? a
forall a b. a :-? b
hyperStrict
  cosC :: a :-? a
cosC = a :-? a
forall a b. a :-? b
hyperStrict
  sinC :: a :-? a
sinC = a :-? a
forall a b. a :-? b
hyperStrict
  logC :: a :-? a
logC = a :-? a
forall a b. a :-? b
hyperStrict
  sqrtC :: a :-? a
sqrtC = a :-? a
forall a b. a :-? b
hyperStrict

instance RealFracCat (->) a b => RealFracCat (:-?) a b where
  floorC :: a :-? b
floorC    = a :-? b
forall a b. a :-? b
hyperStrict
  ceilingC :: a :-? b
ceilingC  = a :-? b
forall a b. a :-? b
hyperStrict
  truncateC :: a :-? b
truncateC = a :-? b
forall a b. a :-? b
hyperStrict

instance FromIntegralCat (->) a b => FromIntegralCat (:-?) a b where
  fromIntegralC :: a :-? b
fromIntegralC = a :-? b
forall a b. a :-? b
hyperStrict

-- Still to come: IfCat, UnknownCat, RepCat, CoerceCat, 

-- Every demand function must map NoneD to NoneD, so represent a :-? b
-- as Demand b -> Maybe (Demand a), and use Kleisli composition. Or represent
-- as a Kleisli in the first place.