{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-----------------------------------------------------------------------------

-- |

-- Module      :  Data.Functor.Product.Singletons

-- Copyright   :  (C) 2021 Ryan Scott

-- License     :  BSD-style (see LICENSE)

-- Maintainer  :  Richard Eisenberg (rae@cs.brynmawr.edu)

-- Stability   :  experimental

-- Portability :  non-portable

--

-- Exports the promoted and singled versions of the 'Product' data type.

--

-----------------------------------------------------------------------------


module Data.Functor.Product.Singletons (
  -- * The 'Product' singleton

  Sing, SProduct(..),

  -- * Defunctionalization symbols

  PairSym0, PairSym1, PairSym2
  ) where

import Control.Applicative
import Control.Applicative.Singletons
import Control.Monad
import Control.Monad.Singletons
import Control.Monad.Zip
import Control.Monad.Zip.Singletons
import Data.Foldable.Singletons hiding (Product)
import Data.Function.Singletons
import Data.Functor.Product
import Data.Kind
import Data.Monoid.Singletons hiding (SProduct(..))
import Data.Singletons
import Data.Singletons.TH
import Data.Traversable.Singletons

{-
In order to keep the type arguments to Product poly-kinded and with inferred
specificities, we define the singleton version of Product, as well as its
defunctionalization symbols, by hand. This is very much in the spirit of the
code in Data.Functor.Const.Singletons. (See the comments above SConst in that
module for more details on this choice.)
-}
type SProduct :: Product f g a -> Type
data SProduct :: Product f g a -> Type where
  SPair :: forall f g a (x :: f a) (y :: g a).
           Sing x -> Sing y -> SProduct ('Pair @f @g @a x y)
type instance Sing = SProduct
instance (SingI x, SingI y) => SingI ('Pair x y) where
  sing :: Sing ('Pair x y)
sing = Sing x -> Sing y -> SProduct ('Pair x y)
forall {k} (f :: k -> *) (g :: k -> *) (a :: k) (arg :: f a)
       (arg :: g a).
Sing arg -> Sing arg -> SProduct ('Pair arg arg)
SPair Sing x
forall {k} (a :: k). SingI a => Sing a
sing Sing y
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI x => SingI1 ('Pair x) where
  liftSing :: forall (x :: g a). Sing x -> Sing ('Pair x x)
liftSing = Sing x -> Sing x -> SProduct ('Pair x x)
forall {k} (f :: k -> *) (g :: k -> *) (a :: k) (arg :: f a)
       (arg :: g a).
Sing arg -> Sing arg -> SProduct ('Pair arg arg)
SPair Sing x
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI2 'Pair where
  liftSing2 :: forall (x :: f a) (y :: g a). Sing x -> Sing y -> Sing ('Pair x y)
liftSing2 = Sing x -> Sing y -> Sing ('Pair x y)
Sing x -> Sing y -> SProduct ('Pair x y)
forall {k} (f :: k -> *) (g :: k -> *) (a :: k) (arg :: f a)
       (arg :: g a).
Sing arg -> Sing arg -> SProduct ('Pair arg arg)
SPair

type PairSym0 :: forall f g a. f a ~> g a ~> Product f g a
data PairSym0 z
type instance Apply PairSym0 x = PairSym1 x
instance SingI PairSym0 where
  sing :: Sing PairSym0
sing = SingFunction2 PairSym0 -> Sing PairSym0
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 Sing t1 -> Sing t2 -> Sing (Apply (Apply PairSym0 t1) t2)
Sing t1 -> Sing t2 -> SProduct ('Pair t1 t2)
SingFunction2 PairSym0
forall {k} (f :: k -> *) (g :: k -> *) (a :: k) (arg :: f a)
       (arg :: g a).
Sing arg -> Sing arg -> SProduct ('Pair arg arg)
SPair

type PairSym1 :: forall f g a. f a -> g a ~> Product f g a
data PairSym1 fa z
type instance Apply (PairSym1 x) y = 'Pair x y
instance SingI x => SingI (PairSym1 x) where
  sing :: Sing (PairSym1 x)
sing = SingFunction1 (PairSym1 x) -> Sing (PairSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (PairSym1 x) -> Sing (PairSym1 x))
-> SingFunction1 (PairSym1 x) -> Sing (PairSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> SProduct ('Pair x t)
forall {k} (f :: k -> *) (g :: k -> *) (a :: k) (arg :: f a)
       (arg :: g a).
Sing arg -> Sing arg -> SProduct ('Pair arg arg)
SPair (forall (a :: f a). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x)
instance SingI1 PairSym1 where
  liftSing :: forall (x :: f a). Sing x -> Sing (PairSym1 x)
liftSing Sing x
s = SingFunction1 (PairSym1 x) -> Sing (PairSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (PairSym1 x) -> Sing (PairSym1 x))
-> SingFunction1 (PairSym1 x) -> Sing (PairSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> SProduct ('Pair x t)
forall {k} (f :: k -> *) (g :: k -> *) (a :: k) (arg :: f a)
       (arg :: g a).
Sing arg -> Sing arg -> SProduct ('Pair arg arg)
SPair Sing x
s

type PairSym2 :: forall f g a. f a -> g a -> Product f g a
type family PairSym2 x y where
  PairSym2 x y = 'Pair x y

$(singletonsOnly [d|
  instance (Functor f, Functor g) => Functor (Product f g) where
      fmap f (Pair x y) = Pair (fmap f x) (fmap f y)
      a <$ (Pair x y) = Pair (a <$ x) (a <$ y)

  instance (Foldable f, Foldable g) => Foldable (Product f g) where
      foldMap f (Pair x y) = foldMap f x `mappend` foldMap f y

  instance (Traversable f, Traversable g) => Traversable (Product f g) where
      traverse f (Pair x y) = liftA2 Pair (traverse f x) (traverse f y)

  instance (Applicative f, Applicative g) => Applicative (Product f g) where
      pure x = Pair (pure x) (pure x)
      Pair f g <*> Pair x y = Pair (f <*> x) (g <*> y)
      liftA2 f (Pair a b) (Pair x y) = Pair (liftA2 f a x) (liftA2 f b y)

  instance (Alternative f, Alternative g) => Alternative (Product f g) where
      empty = Pair empty empty
      Pair x1 y1 <|> Pair x2 y2 = Pair (x1 <|> x2) (y1 <|> y2)

  instance (Monad f, Monad g) => Monad (Product f g) where
      Pair m n >>= f = Pair (m >>= fstP . f) (n >>= sndP . f)
        where
          fstP (Pair a _) = a
          sndP (Pair _ b) = b

  instance (MonadPlus f, MonadPlus g) => MonadPlus (Product f g) where
      mzero = Pair mzero mzero
      Pair x1 y1 `mplus` Pair x2 y2 = Pair (x1 `mplus` x2) (y1 `mplus` y2)

  instance (MonadZip f, MonadZip g) => MonadZip (Product f g) where
      mzipWith f (Pair x1 y1) (Pair x2 y2) = Pair (mzipWith f x1 x2) (mzipWith f y1 y2)
  |])