{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall -fno-warn-orphans #-}

-- | Orphan instances to be moved into other libraries
--
-- <https://github.com/ekmett/pointed/issues/18>

module ConCat.Orphans where

import Prelude hiding (zipWith)
-- import Control.Applicative (liftA2)
import Control.Arrow ((|||))
import Data.Monoid
import GHC.Generics (U1(..),Par1(..),(:+:)(..),(:*:)(..),(:.:)(..))
-- import Data.Foldable 

import Data.Void
import Data.Key
import Data.Pointed
-- import Data.Copointed
-- import Control.Comonad.Cofree
#if  !MIN_VERSION_vector_sized(1,0,1)
import Data.Distributive (Distributive(..))
import Data.Functor.Rep (Representable(..),distributeRep)
#endif
-- import qualified Data.Functor.Rep as Rep

-- import Data.Stream (Stream(..))
import Control.Newtype.Generics
import Text.PrettyPrint.HughesPJClass hiding ((<>))
import GHC.TypeLits (KnownNat)
import Data.Finite (Finite,finite,finites)
import Data.Vector.Sized (Vector)
import qualified Data.Vector.Sized as V

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

#if 0
-- In keys-3.12 (2018-01-28)

{--------------------------------------------------------------------
    GHC.Generics and keys
-------------------------------------------------------------------
-}

-- Key

type instance Key U1 = Void
type instance Key Par1 = ()
type instance Key (g :.: f) = (Key g , Key f)
type instance Key (f :*: g) = Either (Key f) (Key g)

-- Keyed

instance Keyed U1 where
  mapWithKey _ U1 = U1
  {-# INLINE mapWithKey #-}

instance Keyed Par1 where
  mapWithKey q = fmap (q ())
  {-# INLINE mapWithKey #-}

instance (Keyed g, Keyed f) => Keyed (f :*: g) where
  mapWithKey q (fa :*: ga) = mapWithKey (q . Left) fa :*: mapWithKey (q . Right) ga
  {-# INLINE mapWithKey #-}

instance (Keyed g, Keyed f) => Keyed (g :.: f) where
  mapWithKey q = inNew (mapWithKey (mapWithKey . fmap q . (,)))
  {-# INLINE mapWithKey #-}

#if 0
mapWithKey :: (Key (g :.: f) -> a -> b) -> (g :.: f) a -> (g :.: f) b
           :: ((Key g, Key f) -> a -> b) -> (g :.: f) a -> (g :.: f) b

mapWithKey q
  = \ (Comp1 gfa) -> Comp1 (mapWithKey (\ gk -> mapWithKey (\ fk a -> q (gk, fk) a)) gfa)
  = inNew $ mapWithKey (\ gk -> mapWithKey (\ fk a -> q (gk, fk) a))
  = inNew $ mapWithKey (\ gk -> mapWithKey (\ fk -> q (gk, fk)))
  = inNew $ mapWithKey (\ gk -> mapWithKey (q . (gk,)))
  = inNew $ mapWithKey (\ gk -> mapWithKey . (q .) $ (gk,))
  = inNew $ mapWithKey (\ gk -> mapWithKey . (q .) $ (,) gk)
  = inNew (mapWithKey (mapWithKey . fmap q . (,)))

q   :: ((Key g, Key f) -> a -> b)
gfa :: g (f a)
gk  :: Key g
fk  :: Key f
#endif

-- Zip

instance Zip U1 where
  zipWith = liftA2
  {-# INLINE zipWith #-}

instance Zip Par1 where
  zipWith = liftA2
  {-# INLINE zipWith #-}

instance (Zip f, Zip g) => Zip (f :*: g) where
  zipWith h (fa :*: ga) (fa' :*: ga') =
    zipWith h fa fa' :*: zipWith h ga ga'
  {-# INLINE zipWith #-}

instance (Zip f, Zip g) => Zip (g :.: f) where
  zipWith = inNew2 . zipWith . zipWith
  {-# INLINE zipWith #-}


-- ZipWithKey

instance ZipWithKey U1

instance ZipWithKey Par1

instance (Keyed g, Zip g, Keyed f, Zip f) => ZipWithKey (f :*: g)

instance (Keyed g, Zip g, Keyed f, Zip f) => ZipWithKey (g :.: f)


-- Indexable

instance Indexable U1 where index U1 = \ case

instance Indexable Par1 where index (Par1 a) () = a

instance (Indexable g, Indexable f) =>
         Indexable (f :*: g) where
  index (fa :*: _) (Left  fk) = fa ! fk
  index (_ :*: ga) (Right gk) = ga ! gk
  {-# INLINE index #-}

instance (Indexable g, Indexable f) =>
         Indexable (g :.: f) where
  index (Comp1 gfa) (gk,fk) = gfa ! gk ! fk
  {-# INLINE index #-}


-- Lookup

instance Lookup U1 where lookup = lookupDefault

instance Lookup Par1 where lookup = lookupDefault

instance (Indexable g, Indexable f) => Lookup (f :*: g) where
  lookup = lookupDefault

instance (Indexable g, Indexable f) => Lookup (g :.: f) where
  lookup = lookupDefault


-- Adjustable

instance Adjustable U1 where
  adjust = const (const id)
  {-# INLINE adjust #-}

instance Adjustable Par1 where
  adjust h () = fmap h
  {-# INLINE adjust #-}

instance (Adjustable g, Adjustable f) => Adjustable (f :*: g) where
  adjust h (Left  fk) (fa :*: ga) = adjust h fk fa :*: ga
  adjust h (Right gk) (fa :*: ga) = fa :*: adjust h gk ga
  {-# INLINE adjust #-}

instance (Adjustable g, Adjustable f) => Adjustable (g :.: f) where
  adjust h (gk,fk) = inNew (adjust (adjust h fk) gk)
  {-# INLINE adjust #-}

#endif

#if 0
-- No longer needed with pointed-5.0.1 (2018-01-22)

{--------------------------------------------------------------------
    GHC.Generics and pointed
-------------------------------------------------------------------
-}

instance Pointed U1 where
  point = const U1
  {-# INLINE point #-}

instance Pointed Par1 where
  point = Par1
  {-# INLINE point #-}

instance (Pointed f, Pointed g) => Pointed (f :*: g) where
  point a = point a :*: point a
  {-# INLINE point #-}

instance (Pointed f, Pointed g) => Pointed (g :.: f) where
  point = Comp1 . point . point
  {-# INLINE point #-}

instance Copointed Par1 where
  copoint = unPar1
  {-# INLINE copoint #-}

instance (Copointed f, Copointed g) => Copointed (g :.: f) where
  copoint = copoint . copoint . unComp1
  {-# INLINE copoint #-}

-- TODO: many Pointed and Copointed instances for GHC.Generics types.
-- Offer as a pointed patch, as I did with keys.

instance Pointed f => Pointed (Cofree f) where
  point a = z where z = a :< point z

instance Copointed (Cofree f) where
  copoint (a :< _) = a

#endif

{--------------------------------------------------------------------
    Control.Newtype and keys
-------------------------------------------------------------------
-}

instance Newtype (Par1 t) where
  type O (Par1 t) = t
  pack :: O (Par1 t) -> Par1 t
pack = t -> Par1 t
O (Par1 t) -> Par1 t
forall p. p -> Par1 p
Par1
  unpack :: Par1 t -> O (Par1 t)
unpack = Par1 t -> t
Par1 t -> O (Par1 t)
forall p. Par1 p -> p
unPar1

instance Newtype ((a :*: b) t) where
  type O ((a :*: b) t) = a t :* b t
  pack :: O ((:*:) a b t) -> (:*:) a b t
pack (a t
a,b t
b) = a t
a a t -> b t -> (:*:) a b t
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b t
b
  unpack :: (:*:) a b t -> O ((:*:) a b t)
unpack (a t
a :*: b t
b) = (a t
a,b t
b)

instance Newtype ((a :+: b) t) where
  type O ((a :+: b) t) = a t :+ b t
  pack :: O ((:+:) a b t) -> (:+:) a b t
pack = (a t -> (:+:) a b t)
-> (b t -> (:+:) a b t) -> Either (a t) (b t) -> (:+:) a b t
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a t -> (:+:) a b t
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 b t -> (:+:) a b t
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1
  unpack :: (:+:) a b t -> O ((:+:) a b t)
unpack = (a t -> Either (a t) (b t))
-> (b t -> Either (a t) (b t)) -> (:+:) a b t -> Either (a t) (b t)
forall (a :: * -> *) t c (b :: * -> *).
(a t -> c) -> (b t -> c) -> (:+:) a b t -> c
eitherF a t -> Either (a t) (b t)
forall a b. a -> Either a b
Left b t -> Either (a t) (b t)
forall a b. b -> Either a b
Right

instance Newtype ((a :.: b) t) where
  type O ((a :.: b) t) = a (b t)
  pack :: O ((:.:) a b t) -> (:.:) a b t
pack = a (b t) -> (:.:) a b t
O ((:.:) a b t) -> (:.:) a b t
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1
  unpack :: (:.:) a b t -> O ((:.:) a b t)
unpack = (:.:) a b t -> a (b t)
(:.:) a b t -> O ((:.:) a b t)
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
unComp1

fstF :: (a :*: b) t -> a t
fstF :: forall (a :: * -> *) (b :: * -> *) t. (:*:) a b t -> a t
fstF (a t
a :*: b t
_) = a t
a

sndF :: (a :*: b) t -> b t
sndF :: forall (a :: * -> *) (b :: * -> *) t. (:*:) a b t -> b t
sndF (a t
_ :*: b t
b) = b t
b

eitherF :: (a t -> c) -> (b t -> c) -> ((a :+: b) t -> c)
eitherF :: forall (a :: * -> *) t c (b :: * -> *).
(a t -> c) -> (b t -> c) -> (:+:) a b t -> c
eitherF a t -> c
f b t -> c
_ (L1 a t
a) = a t -> c
f a t
a
eitherF a t -> c
_ b t -> c
g (R1 b t
b) = b t -> c
g b t
b

#if 0
{--------------------------------------------------------------------
    Data.Stream
-------------------------------------------------------------------
-}

instance Pointed Stream where point   = pure
instance Zip     Stream where zipWith = liftA2
-- etc

instance Foldable Stream where
  foldMap f ~(Cons a as) = f a `mappend` foldMap f as
#endif

{--------------------------------------------------------------------
    Pretty
-------------------------------------------------------------------
-}

instance Pretty (U1 a) where
  pPrintPrec :: PrettyLevel -> Rational -> U1 a -> Doc
pPrintPrec PrettyLevel
_ Rational
_ U1 a
U1 = String -> Doc
text String
"U1"

instance Pretty a => Pretty (Par1 a) where
  pPrintPrec :: PrettyLevel -> Rational -> Par1 a -> Doc
pPrintPrec PrettyLevel
l Rational
p (Par1 a
a) = PrettyLevel -> Rational -> String -> a -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> String -> a -> Doc
app PrettyLevel
l Rational
p String
"Par1" a
a

instance (Pretty (f a), Pretty (g a)) => Pretty ((f :*: g) a) where
  pPrintPrec :: PrettyLevel -> Rational -> (:*:) f g a -> Doc
pPrintPrec PrettyLevel
l Rational
p (f a
fa :*: g a
ga) =
    Bool -> Doc -> Doc
maybeParens (Rational
p Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
6) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
     [Doc] -> Doc
sep [PrettyLevel -> Rational -> f a -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
7 f a
fa Doc -> Doc -> Doc
<+> String -> Doc
text String
":*:", PrettyLevel -> Rational -> g a -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
6 g a
ga]

instance Pretty (g (f a)) => Pretty ((g :.: f) a) where
  pPrintPrec :: PrettyLevel -> Rational -> (:.:) g f a -> Doc
pPrintPrec PrettyLevel
l Rational
p (Comp1 g (f a)
gfa) = PrettyLevel -> Rational -> String -> g (f a) -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> String -> a -> Doc
app PrettyLevel
l Rational
p String
"Comp1" g (f a)
gfa

app :: Pretty a => PrettyLevel -> Rational -> String -> a -> Doc
app :: forall a. Pretty a => PrettyLevel -> Rational -> String -> a -> Doc
app PrettyLevel
l Rational
p String
str a
a =
  Bool -> Doc -> Doc
maybeParens (Rational
p Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
appPrec) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
   String -> Doc
text String
str Doc -> Doc -> Doc
<+> PrettyLevel -> Rational -> a -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l (Rational
appPrecRational -> Rational -> Rational
forall a. Num a => a -> a -> a
+Rational
1) a
a

appPrec :: Rational
appPrec :: Rational
appPrec = Rational
10

{--------------------------------------------------------------------
    Distributive
-------------------------------------------------------------------
-}

#if 0

-- In adjunctions-4.4

{--------------------------------------------------------------------
    Representable
-------------------------------------------------------------------
-}

instance Representable U1 where
  type Rep U1 = Void
  tabulate _ = U1
  index U1 = absurd

instance Representable Par1 where
  type Rep Par1 = ()
  tabulate h = Par1 (h ())
  index (Par1 a) () = a

instance (Representable f, Representable g) => Representable (f :*: g) where
  type Rep (f :*: g) = Rep f :+ Rep g
  tabulate h = tabulate (h . Left) :*: tabulate (h . Right)
  index (fa :*: ga) = Rep.index fa `either` Rep.index ga

instance (Representable g, Representable f) => Representable (g :.: f) where
  type Rep (g :.: f) = Rep g :* Rep f
  tabulate :: (Rep g :* Rep f -> a) -> (g :.: f) a
  tabulate h = Comp1 (tabulate <$> tabulate (curry h))
  index (Comp1 gfa) (i,j) = Rep.index (Rep.index gfa i) j

--                                     h   :: Rep g :* Rep f -> a
--                               curry h   :: Rep g -> Rep f -> a
--                     tabulate (curry h)  :: g (Rep f -> a)
--        tabulate <$> tabulate (curry h)  :: g (f a)
-- Comp1 (tabulate <$> tabulate (curry h)) :: (g :.: f) a

#endif

{--------------------------------------------------------------------
    Monoids
-------------------------------------------------------------------
-}

-- instance Zip Sum where zipWith f (Sum a) (Sum b) = Sum (f a b)
-- instance Zip Product where zipWith f (Product a) (Product b) = Product (f a b)

instance Zip Sum     where zipWith :: forall a b c. (a -> b -> c) -> Sum a -> Sum b -> Sum c
zipWith = (a -> b -> c) -> Sum a -> Sum b -> Sum c
(O (Sum a) -> O (Sum b) -> O (Sum c)) -> Sum a -> Sum b -> Sum c
forall p q r.
(Newtype p, Newtype q, Newtype r) =>
(O p -> O q -> O r) -> p -> q -> r
inNew2
instance Zip Product where zipWith :: forall a b c. (a -> b -> c) -> Product a -> Product b -> Product c
zipWith = (a -> b -> c) -> Product a -> Product b -> Product c
(O (Product a) -> O (Product b) -> O (Product c))
-> Product a -> Product b -> Product c
forall p q r.
(Newtype p, Newtype q, Newtype r) =>
(O p -> O q -> O r) -> p -> q -> r
inNew2


{--------------------------------------------------------------------
    Vector (Sized)
-------------------------------------------------------------------
-}

type instance Key (Vector n) = Finite n

-- mapWithKey :: (Key f -> a -> b) -> f a -> f b
-- imap :: (Int -> a -> b) -> Vector n a -> Vector n b

imap' :: KnownNat n => (Finite n -> a -> b) -> Vector n a -> Vector n b
imap' :: forall (n :: Nat) a b.
KnownNat n =>
(Finite n -> a -> b) -> Vector n a -> Vector n b
imap' Finite n -> a -> b
f = (Finite n -> a -> b) -> Vector n a -> Vector n b
forall (n :: Nat) a b.
(Finite n -> a -> b) -> Vector n a -> Vector n b
V.imap (Finite n -> a -> b
f (Finite n -> a -> b)
-> (Finite n -> Finite n) -> Finite n -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Finite n
forall (n :: Nat). KnownNat n => Integer -> Finite n
finite (Integer -> Finite n)
-> (Finite n -> Integer) -> Finite n -> Finite n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral)
{-# INLINE imap' #-}

-- I've requested that something like imap' be added to vector-sized, preferably
-- eliminating the error condition. See
-- <https://github.com/expipiplus1/vector-sized/issues/26>

instance KnownNat n => Keyed (Vector n) where
  mapWithKey :: forall a b. (Key (Vector n) -> a -> b) -> Vector n a -> Vector n b
mapWithKey = (Finite n -> a -> b) -> Vector n a -> Vector n b
(Key (Vector n) -> a -> b) -> Vector n a -> Vector n b
forall (n :: Nat) a b.
KnownNat n =>
(Finite n -> a -> b) -> Vector n a -> Vector n b
imap'
  {-# INLINE mapWithKey #-}

instance Zip (Vector n) where
  zip :: forall a b. Vector n a -> Vector n b -> Vector n (a, b)
zip = Vector n a -> Vector n b -> Vector n (a, b)
forall (n :: Nat) a b. Vector n a -> Vector n b -> Vector n (a, b)
V.zip
  zipWith :: forall a b c.
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipWith = (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
forall a b c (n :: Nat).
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
V.zipWith
  {-# INLINE zip #-}
  {-# INLINE zipWith #-}


#if !MIN_VERSION_vector_sized(1,0,1)
instance KnownNat n => Distributive (Vector n) where
  distribute :: Functor f => f (Vector n a) -> Vector n (f a)
  distribute = distributeRep
  {-# INLINE distribute #-}

instance KnownNat n => Representable (Vector n) where
  type Rep (Vector n) = Finite n
  tabulate = V.generate
  index = V.index
  {-# INLINE tabulate #-}
  {-# INLINE index #-}
#endif

instance KnownNat n => Pointed (Vector n) where
#if 1
  point :: forall a. a -> Vector n a
point = a -> Vector n a
forall (n :: Nat) a. KnownNat n => a -> Vector n a
V.replicate
  {-# INLINE {-[0]-} point #-}
#else
  point = pointV
  {-# INLINE point #-}

pointV :: KnownNat n => a -> Vector n a
pointV = V.replicate
{-# INLINE [0] pointV #-}
#endif

{--------------------------------------------------------------------
    Foldable for functions
--------------------------------------------------------------------}

instance Foldable ((->) Void) where
  foldMap :: forall m a. Monoid m => (a -> m) -> (Void -> a) -> m
foldMap a -> m
_ Void -> a
_ = m
forall a. Monoid a => a
mempty
  {-# INLINE foldMap #-}

instance Foldable ((->) ()) where
  foldMap :: forall m a. Monoid m => (a -> m) -> (() -> a) -> m
foldMap a -> m
h () -> a
as = a -> m
h (() -> a
as ())
  {-# INLINE foldMap #-}

instance Foldable ((->) Bool) where
  foldMap :: forall m a. Monoid m => (a -> m) -> (Bool -> a) -> m
foldMap a -> m
h Bool -> a
as = a -> m
h (Bool -> a
as Bool
False) m -> m -> m
forall a. Semigroup a => a -> a -> a
<> a -> m
h (Bool -> a
as Bool
True)
  {-# INLINE foldMap #-}

instance (Foldable ((->) m), Foldable ((->) n)) => Foldable ((->) (m :+ n)) where
  foldMap :: forall m a. Monoid m => (a -> m) -> ((m :+ n) -> a) -> m
foldMap a -> m
h (m :+ n) -> a
as = (a -> m) -> (m -> a) -> m
forall m a. Monoid m => (a -> m) -> (m -> a) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
h ((m :+ n) -> a
as ((m :+ n) -> a) -> (m -> m :+ n) -> m -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m -> m :+ n
forall a b. a -> Either a b
Left) m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (a -> m) -> (n -> a) -> m
forall m a. Monoid m => (a -> m) -> (n -> a) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
h ((m :+ n) -> a
as ((m :+ n) -> a) -> (n -> m :+ n) -> n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n -> m :+ n
forall a b. b -> Either a b
Right)
  {-# INLINE foldMap #-}

instance (Foldable ((->) m), Foldable ((->) n)) => Foldable ((->) (m :* n)) where
  -- foldMap h as = (foldMap.foldMap) h (curry as)
  foldMap :: forall m a. Monoid m => (a -> m) -> ((m :* n) -> a) -> m
foldMap a -> m
h = (a -> m) -> (:.:) ((->) m) ((->) n) a -> m
forall m a. Monoid m => (a -> m) -> (:.:) ((->) m) ((->) n) a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
h ((:.:) ((->) m) ((->) n) a -> m)
-> (((m :* n) -> a) -> (:.:) ((->) m) ((->) n) a)
-> ((m :* n) -> a)
-> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m -> n -> a) -> (:.:) ((->) m) ((->) n) a
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 ((m -> n -> a) -> (:.:) ((->) m) ((->) n) a)
-> (((m :* n) -> a) -> m -> n -> a)
-> ((m :* n) -> a)
-> (:.:) ((->) m) ((->) n) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((m :* n) -> a) -> m -> n -> a
forall a b c. ((a, b) -> c) -> a -> b -> c
curry
  -- fold as = foldMap fold (curry as)  -- experiment
  -- fold as = fold (fmap fold (curry as))  -- experiment
  -- fold as = fold (fold . curry as)  -- experiment
  {-# INLINE foldMap #-}

instance KnownNat n => Foldable ((->) (Finite n)) where
  foldMap :: forall m a. Monoid m => (a -> m) -> (Finite n -> a) -> m
foldMap a -> m
h Finite n -> a
as = (a -> m) -> [a] -> m
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
h (Finite n -> a
as (Finite n -> a) -> [Finite n] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (n :: Nat). KnownNat n => [Finite n]
finites @n)
  {-# INLINE foldMap #-}

sumToMaybe :: () :+ a -> Maybe a
sumToMaybe :: forall a. (() :+ a) -> Maybe a
sumToMaybe = Maybe a -> () -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing (() -> Maybe a) -> (a -> Maybe a) -> Either () a -> Maybe a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
forall (a :: * -> * -> *) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
||| a -> Maybe a
forall a. a -> Maybe a
Just

maybeToSum :: Maybe a -> () :+ a
maybeToSum :: forall a. Maybe a -> () :+ a
maybeToSum = (() :+ a) -> (a -> () :+ a) -> Maybe a -> () :+ a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> () :+ a
forall a b. a -> Either a b
Left ()) a -> () :+ a
forall a b. b -> Either a b
Right

instance Foldable ((->) a) => Foldable ((->) (Maybe a)) where
  foldMap :: forall m a. Monoid m => (a -> m) -> (Maybe a -> a) -> m
foldMap a -> m
h Maybe a -> a
as = (a -> m) -> ((() :+ a) -> a) -> m
forall m a. Monoid m => (a -> m) -> ((() :+ a) -> a) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
h (Maybe a -> a
as (Maybe a -> a) -> ((() :+ a) -> Maybe a) -> (() :+ a) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() :+ a) -> Maybe a
forall a. (() :+ a) -> Maybe a
sumToMaybe)