{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Wno-unused-imports #-} -- TEMP

-- | Indexed sets of morphisms

module ConCat.Choice where

import Prelude hiding (id,(.),curry,uncurry,const)
import qualified Prelude as P
import GHC.Types (Constraint)
import Control.Applicative (liftA2)
#ifdef VectorSized
import GHC.TypeLits (KnownNat)
#endif

import Data.Constraint (Dict(..),(:-)(..))  -- temp
import Control.Newtype.Generics (Newtype(..))
import Data.Key (Zip)
import Data.Pointed (Pointed)
import Data.Distributive (Distributive)
import Data.Functor.Rep (Representable)

import ConCat.Misc ((:*),inNew,inNew2)
import ConCat.Category
import ConCat.AltCat (toCcc,unCcc)

-- | Nondeterminism category. Like a set of morphisms all of the same type, but
-- represented as a function whose range is that set. The function's domain is
-- existentially hidden.
newtype Choice con a b = Choice (OptArg con (a -> b))

instance Newtype (Choice con a b) where
  type O (Choice con a b) = OptArg con (a -> b)
  pack :: O (Choice con a b) -> Choice con a b
pack O (Choice con a b)
o = OptArg con (a -> b) -> Choice con a b
forall (con :: * -> Constraint) a b.
OptArg con (a -> b) -> Choice con a b
Choice O (Choice con a b)
OptArg con (a -> b)
o
  unpack :: Choice con a b -> O (Choice con a b)
unpack (Choice OptArg con (a -> b)
o) = O (Choice con a b)
OptArg con (a -> b)
o

-- Equivalently,
-- 
-- data Choice con a b = forall p. con p => Choice (p -> a -> b)

onChoice :: forall con a b q. con () =>
            (forall p. con p => (p -> a -> b) -> q) -> Choice con a b -> q
onChoice :: forall (con :: * -> Constraint) a b q.
con () =>
(forall p. con p => (p -> a -> b) -> q) -> Choice con a b -> q
onChoice forall p. con p => (p -> a -> b) -> q
h (Choice OptArg con (a -> b)
o) = (forall p. con p => (p -> a -> b) -> q) -> OptArg con (a -> b) -> q
forall (con :: * -> Constraint) z q.
con () =>
(forall p. con p => (p -> z) -> q) -> OptArg con z -> q
onOptArg (p -> a -> b) -> q
forall p. con p => (p -> a -> b) -> q
h OptArg con (a -> b)
o
-- onChoice h (Choice o) = onOptArg' (h ()) h
{-# INLINE onChoice #-}

-- | Deterministic (trivially nondeterministic) arrow
exactly :: con () => (a -> b) -> Choice con a b
exactly :: forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> b
f = OptArg con (a -> b) -> Choice con a b
forall (con :: * -> Constraint) a b.
OptArg con (a -> b) -> Choice con a b
Choice ((a -> b) -> OptArg con (a -> b)
forall (con :: * -> Constraint) z. z -> OptArg con z
NoArg a -> b
f)  -- or pure, requiring CartCon con
{-# INLINE exactly #-}

#if 0

-- | Generate any value of type @p@.
chooseC :: forall con p a b. (CartCon con, con p)
        => Choice con (p :* a) b -> Choice con a b
chooseC (Choice (NoArg (f :: p :* a -> b))) =
  Choice @con (Arg (curry f))
chooseC (Choice (Arg (f :: q -> p :* a -> b))) =
  Choice @con (Arg (uncurry (curry . f)))
    <+ inOp @(:*) @(Sat con) @q @p
{-# INLINE chooseC #-}

-- TODO: use onOptArg or onOptArg'

--           Choice f  :: Choice con (p :* a) b
--                  f  :: q -> p :* a -> b
--          curry . f  :: q -> p -> a -> b
-- uncurry (curry . f) :: q :* p -> a -> b

-- Equivalently, \ (q,p) a -> f q (p,a)

-- | Generate any value of type @p@.
choose :: forall con p a b. (CartCon con, con p)
       => (p -> a -> b) -> (a -> b)
choose f = unCcc (chooseC @con (toCcc (uncurry f)))
{-# INLINE choose #-}

#else

-- This version is a bit simpler, but we're getting a plugin failure to do with
-- an unknown p type.

-- | Generate any value of type @p@.
chooseC :: forall con p a b. (CartCon con, con p)
         => Choice con p (a -> b) -> Choice con a b
chooseC :: forall (con :: * -> Constraint) p a b.
(CartCon con, con p) =>
Choice con p (a -> b) -> Choice con a b
chooseC (Choice (NoArg (p -> a -> b
f :: p -> a -> b))) =
  forall (con :: * -> Constraint) a b.
OptArg con (a -> b) -> Choice con a b
Choice @con ((p -> a -> b) -> OptArg con (a -> b)
forall (con :: * -> Constraint) z p.
con p =>
(p -> z) -> OptArg con z
Arg p -> a -> b
f)
chooseC (Choice (Arg (p -> p -> a -> b
f :: q -> p -> a -> b))) =
  forall (con :: * -> Constraint) a b.
OptArg con (a -> b) -> Choice con a b
Choice @con (((p :* p) -> a -> b) -> OptArg con (a -> b)
forall (con :: * -> Constraint) z p.
con p =>
(p -> z) -> OptArg con z
Arg ((p -> p -> a -> b) -> (p :* p) -> 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 p -> p -> a -> b
f))
    (Con (Sat con (p :* p)) => Choice con a b)
-> ((Sat con p && Sat con p) |- Sat con (p :* p)) -> Choice con a b
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall {k} (op :: k -> k -> k) (con :: k -> *) (a :: k) (b :: k).
OpCon op con =>
(con a && con b) |- con (op a b)
forall (op :: * -> * -> *) (con :: * -> *) a b.
OpCon op con =>
(con a && con b) |- con (op a b)
inOp @(:*) @(Sat con) @q @p
{-# INLINE chooseC #-}

#if 0
-- | Generate any value of type @p@.
choose :: forall con p a b. (CartCon con, con p)
        => (p -> a -> b) -> (a -> b)
choose f = unCcc (chooseC @con (toCcc f))
{-# INLINE choose #-}

-- | Generate any value of type @p@.
chooseC' :: forall con p a. (CartCon con, con p)
          => (p -> a) -> Choice con () a
chooseC' f = Choice @con (Arg (const . f))
{-# INLINE chooseC' #-}

-- | Generate any value of type @p@.
choose' :: forall con p a. (CartCon con, con p)
         => (p -> a) -> a
-- choose' f = unCcc (chooseC' @con f) ()
choose' f = choose @con (const . f) ()
{-# INLINE choose' #-}

-- Maybe I want set-valued functions instead of sets of functions.
-- Use a -> p -> b instead of p -> a -> b.

#else

-- | Generate any value of type @p@.
choose :: forall con p a. (CartCon con, con p)
       => (p -> a) -> a
choose :: forall (con :: * -> Constraint) p a.
(CartCon con, con p) =>
(p -> a) -> a
choose = Choice con (p -> a) a -> (p -> a) -> a
forall (k :: * -> * -> *) a b. k a b -> a -> b
unCcc (forall (con :: * -> Constraint) a b.
OptArg con (a -> b) -> Choice con a b
Choice @con ((p -> (p -> a) -> a) -> OptArg con ((p -> a) -> a)
forall (con :: * -> Constraint) z p.
con p =>
(p -> z) -> OptArg con z
Arg (((p -> a) -> p -> a) -> p -> (p -> a) -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (p -> a) -> p -> a
forall a b. (a -> b) -> a -> b
($))))
{-# INLINE choose #-}

--      ($) :: (p -> a) -> p -> a
-- flip ($) :: p -> (p -> a) -> a

#endif

#endif

{--------------------------------------------------------------------
    Category class instances
--------------------------------------------------------------------}

op1C :: forall con a b c d. CartCon con
     => ((a -> b) -> (c -> d))
     -> (Choice con a b -> Choice con c d)
op1C :: forall (con :: * -> Constraint) a b c d.
CartCon con =>
((a -> b) -> c -> d) -> Choice con a b -> Choice con c d
op1C = (O (Choice con a b) -> O (Choice con c d))
-> Choice con a b -> Choice con c d
(OptArg con (a -> b) -> OptArg con (c -> d))
-> Choice con a b -> Choice con c d
forall p q. (Newtype p, Newtype q) => (O p -> O q) -> p -> q
inNew ((OptArg con (a -> b) -> OptArg con (c -> d))
 -> Choice con a b -> Choice con c d)
-> (((a -> b) -> c -> d)
    -> OptArg con (a -> b) -> OptArg con (c -> d))
-> ((a -> b) -> c -> d)
-> Choice con a b
-> Choice con c d
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
. ((a -> b) -> c -> d) -> OptArg con (a -> b) -> OptArg con (c -> d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap'
-- op1C = inNew . fmap
-- op1C = inNew . fmapOpt  -- Experiment
{-# INLINE op1C #-}

op2C :: forall con a b c d e f. CartCon con
     => ((a -> b) -> (c -> d) -> (e -> f))
     -> (Choice con a b -> Choice con c d -> Choice con e f)
op2C :: forall (con :: * -> Constraint) a b c d e f.
CartCon con =>
((a -> b) -> (c -> d) -> e -> f)
-> Choice con a b -> Choice con c d -> Choice con e f
op2C = (O (Choice con a b) -> O (Choice con c d) -> O (Choice con e f))
-> Choice con a b -> Choice con c d -> Choice con e f
(OptArg con (a -> b) -> OptArg con (c -> d) -> OptArg con (e -> f))
-> Choice con a b -> Choice con c d -> Choice con e f
forall p q r.
(Newtype p, Newtype q, Newtype r) =>
(O p -> O q -> O r) -> p -> q -> r
inNew2 ((OptArg con (a -> b)
  -> OptArg con (c -> d) -> OptArg con (e -> f))
 -> Choice con a b -> Choice con c d -> Choice con e f)
-> (((a -> b) -> (c -> d) -> e -> f)
    -> OptArg con (a -> b)
    -> OptArg con (c -> d)
    -> OptArg con (e -> f))
-> ((a -> b) -> (c -> d) -> e -> f)
-> Choice con a b
-> Choice con c d
-> Choice con e f
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
. ((a -> b) -> (c -> d) -> e -> f)
-> OptArg con (a -> b)
-> OptArg con (c -> d)
-> OptArg con (e -> f)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2'
-- op2C = inNew2 . liftA2
-- op2C = inNew2 . liftA2Opt  -- Experiment
{-# INLINE op2C #-}

-- fmap' and liftA2' are class-op-inlining synonyms for fmap and liftA2, defined
-- in ConCat.Category and re-exported from ConCat.AltCat. When I use fmap
-- and liftA2, a rule in AltCat replaces fmap with fmapC, breaking the
-- inlining of fmap in the OptArg instance. As a result, we don't get to
-- eliminate a case that case-binds a variable we need to (but cannot) inline.
-- Look for a better alternative. See 2017-10-20 notes.

instance CartCon con => Category (Choice con) where
  -- type Ok (Choice con) = Ok (->) -- Yes1
  id :: forall a. Ok (Choice con) a => Choice con a a
id = (a -> a) -> Choice con a a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> a
forall a. Ok (->) a => a -> a
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id
  . :: forall b c a.
Ok3 (Choice con) a b c =>
Choice con b c -> Choice con a b -> Choice con a c
(.) = ((b -> c) -> (a -> b) -> a -> c)
-> Choice con b c -> Choice con a b -> Choice con a c
forall (con :: * -> Constraint) a b c d e f.
CartCon con =>
((a -> b) -> (c -> d) -> e -> f)
-> Choice con a b -> Choice con c d -> Choice con e f
op2C (b -> c) -> (a -> b) -> a -> c
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
(.)
  {-# INLINE id #-}
  {-# INLINE (.) #-}

instance CartCon con => MonoidalPCat (Choice con) where
  *** :: forall a b c d.
Ok4 (Choice con) a b c d =>
Choice con a c
-> Choice con b d
-> Choice con (Prod (Choice con) a b) (Prod (Choice con) c d)
(***) = ((a -> c)
 -> (b -> d) -> Prod (Choice con) a b -> Prod (Choice con) c d)
-> Choice con a c
-> Choice con b d
-> Choice con (Prod (Choice con) a b) (Prod (Choice con) c d)
forall (con :: * -> Constraint) a b c d e f.
CartCon con =>
((a -> b) -> (c -> d) -> e -> f)
-> Choice con a b -> Choice con c d -> Choice con e f
op2C (a -> c)
-> (b -> d) -> Prod (Choice con) a b -> Prod (Choice con) c d
forall a b c d.
Ok4 (->) a b c d =>
(a -> c)
-> (b -> d) -> Prod (Choice con) a b -> Prod (Choice con) c d
forall (k :: * -> * -> *) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (Prod (Choice con) a b) (Prod (Choice con) c d)
(***)
  {-# INLINE (***) #-}

instance CartCon con => BraidedPCat (Choice con) where
  swapP :: forall a b.
Ok2 (Choice con) a b =>
Choice con (Prod (Choice con) a b) (Prod (Choice con) b a)
swapP = (Prod (Choice con) a b -> Prod (Choice con) b a)
-> Choice con (Prod (Choice con) a b) (Prod (Choice con) b a)
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a b -> Prod (Choice con) b a
forall a b.
Ok2 (->) a b =>
Prod (Choice con) a b -> Prod (Choice con) b a
forall (k :: * -> * -> *) a b.
(BraidedPCat k, Ok2 k a b) =>
k (Prod (Choice con) a b) (Prod (Choice con) b a)
swapP
  {-# INLINE swapP #-}

instance CartCon con => ProductCat (Choice con) where
  exl :: forall a b.
Ok2 (Choice con) a b =>
Choice con (Prod (Choice con) a b) a
exl = (Prod (Choice con) a b -> a)
-> Choice con (Prod (Choice con) a b) a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a b -> a
forall a b. Ok2 (->) a b => Prod (Choice con) a b -> a
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod (Choice con) a b) a
exl
  exr :: forall a b.
Ok2 (Choice con) a b =>
Choice con (Prod (Choice con) a b) b
exr = (Prod (Choice con) a b -> b)
-> Choice con (Prod (Choice con) a b) b
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a b -> b
forall a b. Ok2 (->) a b => Prod (Choice con) a b -> b
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod (Choice con) a b) b
exr
  dup :: forall a. Ok (Choice con) a => Choice con a (Prod (Choice con) a a)
dup = (a -> Prod (Choice con) a a)
-> Choice con a (Prod (Choice con) a a)
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> Prod (Choice con) a a
forall a. Ok (->) a => a -> Prod (Choice con) a a
forall (k :: * -> * -> *) a.
(ProductCat k, Ok k a) =>
k a (Prod (Choice con) a a)
dup
  {-# INLINE exl #-}
  {-# INLINE exr #-}
  {-# INLINE dup #-}

instance CartCon con => UnitCat (Choice con) where
  lunit :: forall a.
Ok (Choice con) a =>
Choice con a (Prod (Choice con) () a)
lunit = (a -> Prod (Choice con) () a)
-> Choice con a (Prod (Choice con) () a)
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> Prod (Choice con) () a
forall a. Ok (->) a => a -> Prod (Choice con) () a
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k a (Prod (Choice con) () a)
lunit
  runit :: forall a.
Ok (Choice con) a =>
Choice con a (Prod (Choice con) a ())
runit = (a -> Prod (Choice con) a ())
-> Choice con a (Prod (Choice con) a ())
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> Prod (Choice con) a ()
forall a. Ok (->) a => a -> Prod (Choice con) a ()
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k a (Prod (Choice con) a ())
runit
  lcounit :: forall a.
Ok (Choice con) a =>
Choice con (Prod (Choice con) () a) a
lcounit = (Prod (Choice con) () a -> a)
-> Choice con (Prod (Choice con) () a) a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) () a -> a
forall a. Ok (->) a => Prod (Choice con) () a -> a
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k (Prod (Choice con) () a) a
lcounit
  rcounit :: forall a.
Ok (Choice con) a =>
Choice con (Prod (Choice con) a ()) a
rcounit = (Prod (Choice con) a () -> a)
-> Choice con (Prod (Choice con) a ()) a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a () -> a
forall a. Ok (->) a => Prod (Choice con) a () -> a
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k (Prod (Choice con) a ()) a
rcounit
  {-# INLINE lunit #-}
  {-# INLINE runit #-}
  {-# INLINE lcounit #-}
  {-# INLINE rcounit #-}

instance CartCon con => MonoidalSCat (Choice con) where
  +++ :: forall a b c d.
Ok4 (Choice con) a b c d =>
Choice con c a
-> Choice con d b
-> Choice con (Coprod (Choice con) c d) (Coprod (Choice con) a b)
(+++) = ((c -> a)
 -> (d -> b) -> Coprod (Choice con) c d -> Coprod (Choice con) a b)
-> Choice con c a
-> Choice con d b
-> Choice con (Coprod (Choice con) c d) (Coprod (Choice con) a b)
forall (con :: * -> Constraint) a b c d e f.
CartCon con =>
((a -> b) -> (c -> d) -> e -> f)
-> Choice con a b -> Choice con c d -> Choice con e f
op2C (c -> a)
-> (d -> b) -> Coprod (Choice con) c d -> Coprod (Choice con) a b
forall a b c d.
Ok4 (->) a b c d =>
(c -> a)
-> (d -> b) -> Coprod (Choice con) c d -> Coprod (Choice con) a b
forall (k :: * -> * -> *) a b c d.
(MonoidalSCat k, Ok4 k a b c d) =>
k c a
-> k d b -> k (Coprod (Choice con) c d) (Coprod (Choice con) a b)
(+++)
  {-# INLINE (+++) #-}

instance CartCon con => BraidedSCat (Choice con) where
  swapS :: forall a b.
Ok2 (Choice con) a b =>
Choice con (Coprod (Choice con) a b) (Coprod (Choice con) b a)
swapS = (Coprod (Choice con) a b -> Coprod (Choice con) b a)
-> Choice con (Coprod (Choice con) a b) (Coprod (Choice con) b a)
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Coprod (Choice con) a b -> Coprod (Choice con) b a
forall a b.
Ok2 (->) a b =>
Coprod (Choice con) a b -> Coprod (Choice con) b a
forall (k :: * -> * -> *) a b.
(BraidedSCat k, Ok2 k a b) =>
k (Coprod (Choice con) a b) (Coprod (Choice con) b a)
swapS
  {-# INLINE swapS #-}

instance CartCon con => CoproductCat (Choice con) where
  inl :: forall a b.
Ok2 (Choice con) a b =>
Choice con a (Coprod (Choice con) a b)
inl = (a -> Coprod (Choice con) a b)
-> Choice con a (Coprod (Choice con) a b)
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> Coprod (Choice con) a b
forall a b. Ok2 (->) a b => a -> Coprod (Choice con) a b
forall (k :: * -> * -> *) a b.
(CoproductCat k, Ok2 k a b) =>
k a (Coprod (Choice con) a b)
inl
  inr :: forall a b.
Ok2 (Choice con) a b =>
Choice con b (Coprod (Choice con) a b)
inr = (b -> Coprod (Choice con) a b)
-> Choice con b (Coprod (Choice con) a b)
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly b -> Coprod (Choice con) a b
forall a b. Ok2 (->) a b => b -> Coprod (Choice con) a b
forall (k :: * -> * -> *) a b.
(CoproductCat k, Ok2 k a b) =>
k b (Coprod (Choice con) a b)
inr
  jam :: forall a.
Ok (Choice con) a =>
Choice con (Coprod (Choice con) a a) a
jam = (Coprod (Choice con) a a -> a)
-> Choice con (Coprod (Choice con) a a) a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Coprod (Choice con) a a -> a
forall a. Ok (->) a => Coprod (Choice con) a a -> a
forall (k :: * -> * -> *) a.
(CoproductCat k, Ok k a) =>
k (Coprod (Choice con) a a) a
jam

instance CartCon con => DistribCat (Choice con) where
  distl :: forall a u v.
Ok3 (Choice con) a u v =>
Choice
  con
  (Prod (Choice con) a (Coprod (Choice con) u v))
  (Coprod
     (Choice con) (Prod (Choice con) a u) (Prod (Choice con) a v))
distl = (Prod (Choice con) a (Coprod (Choice con) u v)
 -> Coprod
      (Choice con) (Prod (Choice con) a u) (Prod (Choice con) a v))
-> Choice
     con
     (Prod (Choice con) a (Coprod (Choice con) u v))
     (Coprod
        (Choice con) (Prod (Choice con) a u) (Prod (Choice con) a v))
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a (Coprod (Choice con) u v)
-> Coprod
     (Choice con) (Prod (Choice con) a u) (Prod (Choice con) a v)
forall a u v.
Ok3 (->) a u v =>
Prod (Choice con) a (Coprod (Choice con) u v)
-> Coprod
     (Choice con) (Prod (Choice con) a u) (Prod (Choice con) a v)
forall (k :: * -> * -> *) a u v.
(DistribCat k, Ok3 k a u v) =>
k (Prod (Choice con) a (Coprod (Choice con) u v))
  (Coprod
     (Choice con) (Prod (Choice con) a u) (Prod (Choice con) a v))
distl
  distr :: forall u v b.
Ok3 (Choice con) u v b =>
Choice
  con
  (Prod (Choice con) (Coprod (Choice con) u v) b)
  (Coprod
     (Choice con) (Prod (Choice con) u b) (Prod (Choice con) v b))
distr = (Prod (Choice con) (Coprod (Choice con) u v) b
 -> Coprod
      (Choice con) (Prod (Choice con) u b) (Prod (Choice con) v b))
-> Choice
     con
     (Prod (Choice con) (Coprod (Choice con) u v) b)
     (Coprod
        (Choice con) (Prod (Choice con) u b) (Prod (Choice con) v b))
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) (Coprod (Choice con) u v) b
-> Coprod
     (Choice con) (Prod (Choice con) u b) (Prod (Choice con) v b)
forall u v b.
Ok3 (->) u v b =>
Prod (Choice con) (Coprod (Choice con) u v) b
-> Coprod
     (Choice con) (Prod (Choice con) u b) (Prod (Choice con) v b)
forall (k :: * -> * -> *) u v b.
(DistribCat k, Ok3 k u v b) =>
k (Prod (Choice con) (Coprod (Choice con) u v) b)
  (Coprod
     (Choice con) (Prod (Choice con) u b) (Prod (Choice con) v b))
distr
  {-# INLINE distl #-}
  {-# INLINE distr #-}

instance CartCon con => ClosedCat (Choice con) where
  apply :: forall a b.
Ok2 (Choice con) a b =>
Choice con (Prod (Choice con) (Exp (Choice con) a b) a) b
apply = (Prod (Choice con) (Exp (Choice con) a b) a -> b)
-> Choice con (Prod (Choice con) (Exp (Choice con) a b) a) b
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) (Exp (Choice con) a b) a -> b
forall a b.
Ok2 (->) a b =>
Prod (Choice con) (Exp (Choice con) a b) a -> b
forall (k :: * -> * -> *) a b.
(ClosedCat k, Ok2 k a b) =>
k (Prod (Choice con) (Exp (Choice con) a b) a) b
apply
  curry :: forall a b c.
Ok3 (Choice con) a b c =>
Choice con (Prod (Choice con) a b) c
-> Choice con a (Exp (Choice con) b c)
curry = ((Prod (Choice con) a b -> c) -> a -> Exp (Choice con) b c)
-> Choice con (Prod (Choice con) a b) c
-> Choice con a (Exp (Choice con) b c)
forall (con :: * -> Constraint) a b c d.
CartCon con =>
((a -> b) -> c -> d) -> Choice con a b -> Choice con c d
op1C (Prod (Choice con) a b -> c) -> a -> Exp (Choice con) b c
forall a b c.
Ok3 (->) a b c =>
(Prod (Choice con) a b -> c) -> a -> Exp (Choice con) b c
forall (k :: * -> * -> *) a b c.
(ClosedCat k, Ok3 k a b c) =>
k (Prod (Choice con) a b) c -> k a (Exp (Choice con) b c)
curry
  uncurry :: forall a b c.
Ok3 (Choice con) a b c =>
Choice con a (Exp (->) b c) -> Choice con (Prod (->) a b) c
uncurry = ((a -> Exp (Choice con) b c) -> Prod (Choice con) a b -> c)
-> Choice con a (Exp (Choice con) b c)
-> Choice con (Prod (Choice con) a b) c
forall (con :: * -> Constraint) a b c d.
CartCon con =>
((a -> b) -> c -> d) -> Choice con a b -> Choice con c d
op1C (a -> Exp (Choice con) b c) -> Prod (Choice con) a b -> c
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
  {-# INLINE apply #-}
  {-# INLINE curry #-}
  {-# INLINE uncurry #-}

instance CartCon con => TerminalCat (Choice con)

instance CartCon con => ConstCat (Choice con) b where
  const :: forall a.
Ok (Choice con) a =>
ConstObj (Choice con) b -> Choice con a (ConstObj (Choice con) b)
const ConstObj (Choice con) b
b = (a -> ConstObj (Choice con) b)
-> Choice con a (ConstObj (Choice con) b)
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly (ConstObj (Choice con) b -> a -> ConstObj (Choice con) b
forall a.
Ok (->) a =>
ConstObj (Choice con) b -> a -> ConstObj (Choice con) b
forall (k :: * -> * -> *) b a.
(ConstCat k (ConstObj k b), Ok k a) =>
ConstObj k b -> k a (ConstObj k b)
const ConstObj (Choice con) b
b)

instance CartCon con => BoolCat (Choice con) where
  notC :: Choice con (BoolOf (Choice con)) (BoolOf (Choice con))
notC = (BoolOf (Choice con) -> BoolOf (Choice con))
-> Choice con (BoolOf (Choice con)) (BoolOf (Choice con))
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly BoolOf (Choice con) -> BoolOf (Choice con)
forall (k :: * -> * -> *).
BoolCat k =>
k (BoolOf (Choice con)) (BoolOf (Choice con))
notC
  andC :: Choice
  con
  (Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con)))
  (BoolOf (Choice con))
andC = (Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con))
 -> BoolOf (Choice con))
-> Choice
     con
     (Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con)))
     (BoolOf (Choice con))
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con))
-> BoolOf (Choice con)
forall (k :: * -> * -> *).
BoolCat k =>
k (Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con)))
  (BoolOf (Choice con))
andC
  orC :: Choice
  con
  (Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con)))
  (BoolOf (Choice con))
orC  = (Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con))
 -> BoolOf (Choice con))
-> Choice
     con
     (Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con)))
     (BoolOf (Choice con))
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con))
-> BoolOf (Choice con)
forall (k :: * -> * -> *).
BoolCat k =>
k (Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con)))
  (BoolOf (Choice con))
orC
  xorC :: Choice
  con
  (Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con)))
  (BoolOf (Choice con))
xorC = (Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con))
 -> BoolOf (Choice con))
-> Choice
     con
     (Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con)))
     (BoolOf (Choice con))
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con))
-> BoolOf (Choice con)
forall (k :: * -> * -> *).
BoolCat k =>
k (Prod (Choice con) (BoolOf (Choice con)) (BoolOf (Choice con)))
  (BoolOf (Choice con))
xorC

instance (Eq a, CartCon con) => EqCat (Choice con) a where
  equal :: Choice con (Prod (Choice con) a a) (BoolOf (Choice con))
equal    = (Prod (Choice con) a a -> BoolOf (Choice con))
-> Choice con (Prod (Choice con) a a) (BoolOf (Choice con))
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a a -> BoolOf (Choice con)
forall (k :: * -> * -> *) a.
EqCat k a =>
k (Prod k a a) (BoolOf (Choice con))
equal
  notEqual :: Choice con (Prod (Choice con) a a) (BoolOf (Choice con))
notEqual = (Prod (Choice con) a a -> BoolOf (Choice con))
-> Choice con (Prod (Choice con) a a) (BoolOf (Choice con))
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a a -> BoolOf (Choice con)
forall (k :: * -> * -> *) a.
EqCat k a =>
k (Prod k a a) (BoolOf (Choice con))
notEqual

instance (Ord a, CartCon con) => OrdCat (Choice con) a where
  lessThan :: Choice con (Prod (Choice con) a a) (BoolOf (Choice con))
lessThan           = (Prod (Choice con) a a -> BoolOf (Choice con))
-> Choice con (Prod (Choice con) a a) (BoolOf (Choice con))
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a a -> BoolOf (Choice con)
forall (k :: * -> * -> *) a.
OrdCat k a =>
k (Prod k a a) (BoolOf (Choice con))
lessThan
  greaterThan :: Choice con (Prod (Choice con) a a) (BoolOf (Choice con))
greaterThan        = (Prod (Choice con) a a -> BoolOf (Choice con))
-> Choice con (Prod (Choice con) a a) (BoolOf (Choice con))
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a a -> BoolOf (Choice con)
forall (k :: * -> * -> *) a.
OrdCat k a =>
k (Prod k a a) (BoolOf (Choice con))
greaterThan
  lessThanOrEqual :: Choice con (Prod (Choice con) a a) (BoolOf (Choice con))
lessThanOrEqual    = (Prod (Choice con) a a -> BoolOf (Choice con))
-> Choice con (Prod (Choice con) a a) (BoolOf (Choice con))
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a a -> BoolOf (Choice con)
forall (k :: * -> * -> *) a.
OrdCat k a =>
k (Prod k a a) (BoolOf (Choice con))
lessThanOrEqual
  greaterThanOrEqual :: Choice con (Prod (Choice con) a a) (BoolOf (Choice con))
greaterThanOrEqual = (Prod (Choice con) a a -> BoolOf (Choice con))
-> Choice con (Prod (Choice con) a a) (BoolOf (Choice con))
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a a -> BoolOf (Choice con)
forall (k :: * -> * -> *) a.
OrdCat k a =>
k (Prod k a a) (BoolOf (Choice con))
greaterThanOrEqual

instance (Ord a, CartCon con) => MinMaxCat (Choice con) a where
  minC :: Choice con (Prod (Choice con) a a) a
minC = (Prod (Choice con) a a -> a)
-> Choice con (Prod (Choice con) a a) a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a a -> a
forall (k :: * -> * -> *) a. MinMaxCat k a => k (Prod k a a) a
minC
  maxC :: Choice con (Prod (Choice con) a a) a
maxC = (Prod (Choice con) a a -> a)
-> Choice con (Prod (Choice con) a a) a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a a -> a
forall (k :: * -> * -> *) a. MinMaxCat k a => k (Prod k a a) a
maxC

instance (Enum a, CartCon con) => EnumCat (Choice con) a where
  succC :: Choice con a a
succC = (a -> a) -> Choice con a a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> a
forall (k :: * -> * -> *) a. EnumCat k a => k a a
succC
  predC :: Choice con a a
predC = (a -> a) -> Choice con a a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> a
forall (k :: * -> * -> *) a. EnumCat k a => k a a
predC

instance (Num a, CartCon con) => NumCat (Choice con) a where
  addC :: Choice con (Prod (Choice con) a a) a
addC    = (Prod (Choice con) a a -> a)
-> Choice con (Prod (Choice con) a a) a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a a -> a
forall (k :: * -> * -> *) a. NumCat k a => k (Prod k a a) a
addC
  mulC :: Choice con (Prod (Choice con) a a) a
mulC    = (Prod (Choice con) a a -> a)
-> Choice con (Prod (Choice con) a a) a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a a -> a
forall (k :: * -> * -> *) a. NumCat k a => k (Prod k a a) a
mulC
  negateC :: Choice con a a
negateC = (a -> a) -> Choice con a a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> a
forall (k :: * -> * -> *) a. NumCat k a => k a a
negateC
  powIC :: Ok (Choice con) Int => Choice con (Prod (Choice con) a Int) a
powIC   = (Prod (Choice con) a Int -> a)
-> Choice con (Prod (Choice con) a Int) a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a Int -> a
forall (k :: * -> * -> *) a.
(NumCat k a, Ok k Int) =>
k (Prod k a Int) a
powIC

instance (Integral a, con ()) => IntegralCat (Choice con) a where
  divC :: Choice con (Prod (Choice con) a a) a
divC = (Prod (Choice con) a a -> a)
-> Choice con (Prod (Choice con) a a) a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a a -> a
forall (k :: * -> * -> *) a. IntegralCat k a => k (Prod k a a) a
divC
  modC :: Choice con (Prod (Choice con) a a) a
modC = (Prod (Choice con) a a -> a)
-> Choice con (Prod (Choice con) a a) a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a a -> a
forall (k :: * -> * -> *) a. IntegralCat k a => k (Prod k a a) a
modC

instance (Fractional a, con ()) => FractionalCat (Choice con) a where
  recipC :: Choice con a a
recipC  = (a -> a) -> Choice con a a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> a
forall (k :: * -> * -> *) a. FractionalCat k a => k a a
recipC
  divideC :: Choice con (Prod (Choice con) a a) a
divideC = (Prod (Choice con) a a -> a)
-> Choice con (Prod (Choice con) a a) a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) a a -> a
forall (k :: * -> * -> *) a. FractionalCat k a => k (Prod k a a) a
divideC

instance (Floating a, con ()) => FloatingCat (Choice con) a where
  expC :: Choice con a a
expC = (a -> a) -> Choice con a a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> a
forall (k :: * -> * -> *) a. FloatingCat k a => k a a
expC
  cosC :: Choice con a a
cosC = (a -> a) -> Choice con a a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> a
forall (k :: * -> * -> *) a. FloatingCat k a => k a a
cosC
  sinC :: Choice con a a
sinC = (a -> a) -> Choice con a a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> a
forall (k :: * -> * -> *) a. FloatingCat k a => k a a
sinC
  logC :: Choice con a a
logC = (a -> a) -> Choice con a a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> a
forall (k :: * -> * -> *) a. FloatingCat k a => k a a
logC
  sqrtC :: Choice con a a
sqrtC = (a -> a) -> Choice con a a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> a
forall (k :: * -> * -> *) a. FloatingCat k a => k a a
sqrtC

instance (Integral b, RealFrac a, con ()) => RealFracCat (Choice con) a b where
  floorC :: Choice con a b
floorC    = (a -> b) -> Choice con a b
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> b
forall (k :: * -> * -> *) a b. RealFracCat k a b => k a b
floorC
  ceilingC :: Choice con a b
ceilingC  = (a -> b) -> Choice con a b
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> b
forall (k :: * -> * -> *) a b. RealFracCat k a b => k a b
ceilingC
  truncateC :: Choice con a b
truncateC = (a -> b) -> Choice con a b
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> b
forall (k :: * -> * -> *) a b. RealFracCat k a b => k a b
truncateC

instance (Integral a, Num b, con ()) => FromIntegralCat (Choice con) a b where
  fromIntegralC :: Choice con a b
fromIntegralC = (a -> b) -> Choice con a b
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> b
forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k) (b :: k1).
FromIntegralCat k2 a b =>
k2 a b
fromIntegralC

instance (con ()) => BottomCat (Choice con) a b where
  bottomC :: Choice con a b
bottomC = (a -> b) -> Choice con a b
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> b
forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k) (b :: k1).
BottomCat k2 a b =>
k2 a b
bottomC

instance CartCon con => IfCat (Choice con) a where
  ifC :: IfT (Choice con) a
ifC = (Prod (Choice con) (BoolOf (Choice con)) (Prod (Choice con) a a)
 -> a)
-> IfT (Choice con) a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly Prod (Choice con) (BoolOf (Choice con)) (Prod (Choice con) a a)
-> a
forall (k :: * -> * -> *) a. IfCat k a => IfT k a
ifC

instance con () => UnknownCat (Choice con) a b where
  unknownC :: Choice con a b
unknownC = (a -> b) -> Choice con a b
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> b
forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k) (b :: k1).
UnknownCat k2 a b =>
k2 a b
unknownC

instance (RepCat (->) a r, con ()) => RepCat (Choice con) a r where
  reprC :: Choice con a r
reprC = (a -> r) -> Choice con a r
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> r
forall {k} (k1 :: k -> k -> *) (a :: k) (r :: k).
RepCat k1 a r =>
k1 a r
reprC
  abstC :: Choice con r a
abstC = (r -> a) -> Choice con r a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly r -> a
forall {k} (k1 :: k -> k -> *) (a :: k) (r :: k).
RepCat k1 a r =>
k1 r a
abstC

instance OkFunctor (Choice con) h where okFunctor :: forall a. Ok' (Choice con) a |- Ok' (Choice con) (h a)
okFunctor = (Con (Sat Yes1 a) :- Con (Sat Yes1 (h a)))
-> Sat Yes1 a |- Sat Yes1 (h a)
forall a b. (Con a :- Con b) -> a |- b
Entail ((Yes1 a => Dict (Yes1 (h a))) -> Yes1 a :- Yes1 (h a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (Yes1 (h a))
Yes1 a => Dict (Yes1 (h a))
forall (a :: Constraint). a => Dict a
Dict)

instance (CartCon con, Functor h) => FunctorCat (Choice con) h where
  fmapC :: forall a b.
Ok2 (Choice con) a b =>
Choice con a b -> Choice con (h a) (h b)
fmapC = ((a -> b) -> h a -> h b)
-> Choice con a b -> Choice con (h a) (h b)
forall (con :: * -> Constraint) a b c d.
CartCon con =>
((a -> b) -> c -> d) -> Choice con a b -> Choice con c d
op1C (a -> b) -> h a -> h b
forall a b. Ok2 (->) a b => (a -> b) -> h a -> h b
forall (k :: * -> * -> *) (h :: * -> *) a b.
(FunctorCat k h, Ok2 k a b) =>
k a b -> k (h a) (h b)
fmapC
  unzipC :: forall a b.
Ok2 (Choice con) a b =>
Choice con (h (a :* b)) (h a :* h b)
unzipC = (h (a :* b) -> h a :* h b) -> Choice con (h (a :* b)) (h a :* h b)
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly h (a :* b) -> h a :* h b
forall a b. Ok2 (->) a b => h (a :* b) -> h a :* h b
forall (k :: * -> * -> *) (h :: * -> *) a b.
(FunctorCat k h, Ok2 k a b) =>
k (h (a :* b)) (h a :* h b)
unzipC

-- Question: should fmap replicate degrees of freedom or share them?

instance (Zip h, CartCon con) => ZipCat (Choice con) h where
  zipC :: forall a b.
Ok2 (Choice con) a b =>
Choice con (h a :* h b) (h (a :* b))
zipC = ((h a :* h b) -> h (a :* b))
-> Choice con (h a :* h b) (h (a :* b))
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly (h a :* h b) -> h (a :* b)
forall a b. Ok2 (->) a b => (h a :* h b) -> h (a :* b)
forall (k :: * -> * -> *) (h :: * -> *) a b.
(ZipCat k h, Ok2 k a b) =>
k (h a :* h b) (h (a :* b))
zipC

-- TODO: ZapCat instance? I don't think so, but we'll see.

instance (Pointed h, CartCon con) => PointedCat (Choice con) h a where
  pointC :: Choice con a (h a)
pointC = (a -> h a) -> Choice con a (h a)
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly a -> h a
forall (k :: * -> * -> *) (h :: * -> *) a.
PointedCat k h a =>
k a (h a)
pointC

instance (AddCat (->) h a, CartCon con) => AddCat (Choice con) h a where
  sumAC :: Choice con (h a) a
sumAC = (h a -> a) -> Choice con (h a) a
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly h a -> a
forall (k :: * -> * -> *) (h :: * -> *) a.
AddCat k h a =>
k (h a) a
sumAC

-- instance (FunctorCat k h, CartCon con) => Strong (Choice con) h where
--   strength = exactly strength

instance (Distributive g, Functor f, CartCon con)
      => DistributiveCat (Choice con) g f where
  distributeC :: forall a. Ok (Choice con) a => Choice con (f (g a)) (g (f a))
distributeC = (f (g a) -> g (f a)) -> Choice con (f (g a)) (g (f a))
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly f (g a) -> g (f a)
forall a. Ok (->) a => f (g a) -> g (f a)
forall (k :: * -> * -> *) (g :: * -> *) (f :: * -> *) a.
(DistributiveCat k g f, Ok k a) =>
k (f (g a)) (g (f a))
distributeC

instance (Representable f, CartCon con) => RepresentableCat (Choice con) f where
  tabulateC :: forall a. Ok (Choice con) a => Choice con (Rep f -> a) (f a)
tabulateC = ((Rep f -> a) -> f a) -> Choice con (Rep f -> a) (f a)
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly (Rep f -> a) -> f a
forall a. Ok (->) a => (Rep f -> a) -> f a
forall (k :: * -> * -> *) (f :: * -> *) a.
(RepresentableCat k f, Ok k a) =>
k (Rep f -> a) (f a)
tabulateC
  indexC :: forall a. Ok (Choice con) a => Choice con (f a) (Rep f -> a)
indexC    = (f a -> Rep f -> a) -> Choice con (f a) (Rep f -> a)
forall (con :: * -> Constraint) a b.
con () =>
(a -> b) -> Choice con a b
exactly f a -> Rep f -> a
forall a. Ok (->) a => f a -> Rep f -> a
forall (k :: * -> * -> *) (f :: * -> *) a.
(RepresentableCat k f, Ok k a) =>
k (f a) (Rep f -> a)
indexC

{--------------------------------------------------------------------
    Maybe move somewhere else
--------------------------------------------------------------------}

-- A function from a constrained, existentially hidden parameter. Optimizes for
-- the parameter being () in order to avoid accumulating products of units.
data OptArg con z = NoArg z | forall p. con p => Arg (p -> z)

-- Equivalently,

-- data OptArg :: (* -> Constraint) -> * -> * where
--   NoArg ::                z  -> OptArg con z 
--   Arg   :: con p => (p -> z) -> OptArg con z

onOptArg :: forall con z q. con ()
         => (forall p. con p => (p -> z) -> q) -> OptArg con z -> q

onOptArg :: forall (con :: * -> Constraint) z q.
con () =>
(forall p. con p => (p -> z) -> q) -> OptArg con z -> q
onOptArg forall p. con p => (p -> z) -> q
h (NoArg z
z) = (() -> z) -> q
forall p. con p => (p -> z) -> q
h (\ () -> z
z)
onOptArg forall p. con p => (p -> z) -> q
h (Arg p -> z
f)   = (p -> z) -> q
forall p. con p => (p -> z) -> q
h p -> z
f

-- onOptArg h o = h (case o of NoArg z -> \ () -> z
--                             Arg f   -> f)

{-# INLINE onOptArg #-}

onOptArg' :: forall con z q. con ()
          => (z -> q)
          -> (forall p. con p => (p -> z) -> q)
          -> OptArg con z -> q
onOptArg' :: forall (con :: * -> Constraint) z q.
con () =>
(z -> q) -> (forall p. con p => (p -> z) -> q) -> OptArg con z -> q
onOptArg' z -> q
g forall p. con p => (p -> z) -> q
_ (NoArg z
z) = z -> q
g z
z
onOptArg' z -> q
_ forall p. con p => (p -> z) -> q
h (Arg p -> z
f)   = (p -> z) -> q
forall p. con p => (p -> z) -> q
h p -> z
f
{-# INLINE onOptArg' #-}

type CartCon con = (con (), OpCon (:*) (Sat con))

#if 1

instance CartCon con => Functor (OptArg con) where
  fmap :: forall a b. (a -> b) -> OptArg con a -> OptArg con b
fmap a -> b
f (NoArg a
u) = b -> OptArg con b
forall (con :: * -> Constraint) z. z -> OptArg con z
NoArg (a -> b
f a
u)
  fmap a -> b
f (  Arg p -> a
g) = (p -> b) -> OptArg con b
forall (con :: * -> Constraint) z p.
con p =>
(p -> z) -> OptArg con z
Arg (a -> b
f (a -> b) -> (p -> a) -> p -> 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
. p -> a
g)
  {-# INLINE fmap #-}

instance CartCon con => Applicative (OptArg con) where
  pure :: forall a. a -> OptArg con a
pure = a -> OptArg con a
forall (con :: * -> Constraint) z. z -> OptArg con z
NoArg
  NoArg a -> b
f <*> :: forall a b. OptArg con (a -> b) -> OptArg con a -> OptArg con b
<*> NoArg a
a = b -> OptArg con b
forall (con :: * -> Constraint) z. z -> OptArg con z
NoArg (a -> b
f a
a)
  NoArg a -> b
f <*> Arg p -> a
as = (p -> b) -> OptArg con b
forall (con :: * -> Constraint) z p.
con p =>
(p -> z) -> OptArg con z
Arg (a -> b
f (a -> b) -> (p -> a) -> p -> 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
. p -> a
as)
  Arg (p -> a -> b
g :: q -> a -> b) <*> NoArg a
a = (p -> b) -> OptArg con b
forall (con :: * -> Constraint) z p.
con p =>
(p -> z) -> OptArg con z
Arg ((p -> a -> b) -> a -> p -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip p -> a -> b
g a
a)
  Arg (p -> a -> b
g :: q -> a -> b) <*> Arg (p -> a
f :: p -> a) =
    ((p :* p) -> b) -> OptArg con b
forall (con :: * -> Constraint) z p.
con p =>
(p -> z) -> OptArg con z
Arg (\ (p
p,p
q) -> p -> a -> b
g p
q (p -> a
f p
p)) (Con (Sat con (p :* p)) => OptArg con b)
-> ((Sat con p && Sat con p) |- Sat con (p :* p)) -> OptArg con b
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall {k} (op :: k -> k -> k) (con :: k -> *) (a :: k) (b :: k).
OpCon op con =>
(con a && con b) |- con (op a b)
forall (op :: * -> * -> *) (con :: * -> *) a b.
OpCon op con =>
(con a && con b) |- con (op a b)
inOp @(:*) @(Sat con) @p @q
  {-# INLINE pure #-}
  {-# INLINE (<*>) #-}

#else

-- Experiment
fmapOpt :: (a -> b) -> OptArg con a -> OptArg con b
fmapOpt f (NoArg u) = NoArg (f u)
fmapOpt f (  Arg g) = Arg (f . g)
{-# INLINE fmapOpt #-}

liftA2Opt :: forall con a b c. CartCon con =>
     (a -> b -> c) -> OptArg con a -> OptArg con b -> OptArg con c
liftA2Opt h (NoArg a) (NoArg b) = NoArg (h a b)
liftA2Opt h (NoArg a) (Arg bs) = Arg (\ p -> h a (bs p))
liftA2Opt h (Arg as) (NoArg b) = Arg (\ p -> h (as p) b)
liftA2Opt h (Arg as) (NoArg b) = Arg (\ p -> h (as p) b)
liftA2Opt h (Arg (g :: q -> a)) (Arg (f :: p -> b)) =
  Arg (\ (p,q) -> h (g q) (f p)) <+ inOp @(:*) @(Sat con) @p @q
{-# INLINE liftA2Opt #-}

#endif

-- Other classes

-- instance (Monoid a, CartCon con) => Monoid (OptArg con a) where
--   mempty = NoArg mempty
--   mappend = liftA2 mappend