-- |
-- Module      :  Control.Functor.Constrained
-- Copyright   :  (c) 2014 Justus Sagemüller
-- License     :  GPL v3 (see COPYING)
-- Maintainer  :  (@) jsag $ hvl.no
-- 

{-# LANGUAGE ConstraintKinds              #-}
{-# LANGUAGE TypeFamilies                 #-}
{-# LANGUAGE TypeOperators                #-}
{-# LANGUAGE FunctionalDependencies       #-}
{-# LANGUAGE FlexibleInstances            #-}
{-# LANGUAGE FlexibleContexts             #-}
{-# LANGUAGE UndecidableInstances         #-}
{-# LANGUAGE CPP                          #-}
#if __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE UndecidableSuperClasses      #-}
#endif


module Control.Functor.Constrained
   ( module Control.Category.Constrained
     -- * Functors
   , Functor(..)
   , (<$>)
   , constrainedFmap
     -- * [Co]product mapping
   , SumToProduct(..)
   ) where


import Control.Category.Constrained

import Prelude hiding (id, (.), Functor(..), filter, (<$>))
import qualified Prelude

import Data.Void

import Data.Type.Coercion
import Data.Complex

import Control.Category.Discrete


class ( Category r, Category t, Object t (f (UnitObject r)) )
           => Functor f r t | f r -> t, f t -> r where
  fmap :: (Object r a, Object t (f a), Object r b, Object t (f b))
     => r a b -> t (f a) (f b)

instance (Prelude.Functor f) => Functor f (->) (->) where
  fmap :: (a -> b) -> f a -> f b
fmap = (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
Prelude.fmap

-- | It is fairly common for functors (typically, container-like) to map 'Either'
--   to tuples in a natural way, thus \"separating the variants\".
--   This is related to 'Data.Foldable.Constrained.Foldable'
--   (with list and tuple monoids), but rather more effective.
class ( CoCartesian r, Cartesian t, Functor f r t, Object t (f (ZeroObject r)) )
           => SumToProduct f r t where
  -- | @
  --   sum2product ≡ mapEither id
  --   @
  sum2product :: ( ObjectSum r a b, ObjectPair t (f a) (f b) )
       => t (f (a+b)) (f a, f b)
  -- | @
  --   mapEither f ≡ sum2product . fmap f
  --   @
  mapEither :: ( Object r a, ObjectSum r b c
               , Object t (f a), ObjectPair t (f b) (f c) )
       => r a (b+c) -> t (f a) (f b, f c)
  filter :: ( Object r a, Object r Bool, Object t (f a) )
       => r a Bool -> t (f a) (f a)

instance SumToProduct [] (->) (->) where
  sum2product :: [a + b] -> ([a], [b])
sum2product [] = ([],[])
  sum2product (Left a
x  : [a + b]
l) = (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs, [b]
ys) where ~([a]
xs,[b]
ys) = [a + b] -> ([a], [b])
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(SumToProduct f r t, ObjectSum r a b, ObjectPair t (f a) (f b)) =>
t (f (a + b)) (f a, f b)
sum2product [a + b]
l
  sum2product (Right b
y : [a + b]
l) = ([a]
xs ,b
yb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
ys) where ~([a]
xs,[b]
ys) = [a + b] -> ([a], [b])
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(SumToProduct f r t, ObjectSum r a b, ObjectPair t (f a) (f b)) =>
t (f (a + b)) (f a, f b)
sum2product [a + b]
l
  mapEither :: (a -> b + c) -> [a] -> ([b], [c])
mapEither a -> b + c
_ [] = ([],[])
  mapEither a -> b + c
f (a
a:[a]
l) = case a -> b + c
f a
a of
      Left b
x  -> (b
xb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
xs, [c]
ys)
      Right c
y -> ([b]
xs ,c
yc -> [c] -> [c]
forall a. a -> [a] -> [a]
:[c]
ys)
   where ~([b]
xs,[c]
ys) = (a -> b + c) -> [a] -> ([b], [c])
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b c.
(SumToProduct f r t, Object r a, ObjectSum r b c, Object t (f a),
 ObjectPair t (f b) (f c)) =>
r a (b + c) -> t (f a) (f b, f c)
mapEither a -> b + c
f [a]
l
  filter :: (a -> Bool) -> [a] -> [a]
filter = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
Prelude.filter


infixl 4 <$>

(<$>) :: (Functor f r (->), Object r a, Object r b)
     => r a b -> f a -> f b
<$> :: r a b -> f a -> f b
(<$>) = r a b -> f a -> f b
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap

  
constrainedFmap :: (Category r, Category t, o a, o b, o (f a), o (f b)) 
      => (   r  a b ->    t  (f a) (f b)  ) 
       -> (o⊢r) a b -> (o⊢t) (f a) (f b)
constrainedFmap :: (r a b -> t (f a) (f b)) -> (⊢) o r a b -> (⊢) o t (f a) (f b)
constrainedFmap r a b -> t (f a) (f b)
q = t (f a) (f b) -> (⊢) o t (f a) (f b)
forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
(Category k, o a, o b) =>
k a b -> (⊢) o k a b
constrained (t (f a) (f b) -> (⊢) o t (f a) (f b))
-> ((⊢) o r a b -> t (f a) (f b))
-> (⊢) o r a b
-> (⊢) o t (f a) (f b)
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. r a b -> t (f a) (f b)
q (r a b -> t (f a) (f b))
-> ((⊢) o r a b -> r a b) -> (⊢) o r a b -> t (f a) (f b)
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. (⊢) o r a b -> r a b
forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
Category k =>
(⊢) o k a b -> k a b
unconstrained

instance (Functor [] k k, o [UnitObject k]) => Functor [] (o⊢k) (o⊢k) where
  fmap :: (⊢) o k a b -> (⊢) o k [a] [b]
fmap (ConstrainedMorphism k a b
f) = k [a] [b] -> (⊢) o k [a] [b]
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (k [a] [b] -> (⊢) o k [a] [b]) -> k [a] [b] -> (⊢) o k [a] [b]
forall a b. (a -> b) -> a -> b
$ k a b -> k [a] [b]
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap k a b
f

instance (o (), o [()], o Void, o [Void]) => SumToProduct [] (o⊢(->)) (o⊢(->)) where
  sum2product :: (⊢) o (->) [a + b] ([a], [b])
sum2product = ([a + b] -> ([a], [b])) -> (⊢) o (->) [a + b] ([a], [b])
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism [a + b] -> ([a], [b])
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(SumToProduct f r t, ObjectSum r a b, ObjectPair t (f a) (f b)) =>
t (f (a + b)) (f a, f b)
sum2product
  mapEither :: (⊢) o (->) a (b + c) -> (⊢) o (->) [a] ([b], [c])
mapEither (ConstrainedMorphism a -> b + c
f) = ([a] -> ([b], [c])) -> (⊢) o (->) [a] ([b], [c])
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (([a] -> ([b], [c])) -> (⊢) o (->) [a] ([b], [c]))
-> ([a] -> ([b], [c])) -> (⊢) o (->) [a] ([b], [c])
forall a b. (a -> b) -> a -> b
$ (a -> b + c) -> [a] -> ([b], [c])
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b c.
(SumToProduct f r t, Object r a, ObjectSum r b c, Object t (f a),
 ObjectPair t (f b) (f c)) =>
r a (b + c) -> t (f a) (f b, f c)
mapEither a -> b + c
f
  filter :: (⊢) o (->) a Bool -> (⊢) o (->) [a] [a]
filter (ConstrainedMorphism a -> Bool
f) = ([a] -> [a]) -> (⊢) o (->) [a] [a]
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (([a] -> [a]) -> (⊢) o (->) [a] [a])
-> ([a] -> [a]) -> (⊢) o (->) [a] [a]
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> [a] -> [a]
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(SumToProduct f r t, Object r a, Object r Bool, Object t (f a)) =>
r a Bool -> t (f a) (f a)
filter a -> Bool
f

  
instance Functor [] Coercion Coercion where fmap :: Coercion a b -> Coercion [a] [b]
fmap Coercion a b
Coercion = Coercion [a] [b]
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
instance Functor Maybe Coercion Coercion where fmap :: Coercion a b -> Coercion (Maybe a) (Maybe b)
fmap Coercion a b
Coercion = Coercion (Maybe a) (Maybe b)
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
instance Functor (Either a) Coercion Coercion where fmap :: Coercion a b -> Coercion (Either a a) (Either a b)
fmap Coercion a b
Coercion = Coercion (Either a a) (Either a b)
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
instance Functor ((->) a) Coercion Coercion where fmap :: Coercion a b -> Coercion (a -> a) (a -> b)
fmap Coercion a b
Coercion = Coercion (a -> a) (a -> b)
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
instance Functor ((,) a) Coercion Coercion where fmap :: Coercion a b -> Coercion (a, a) (a, b)
fmap Coercion a b
Coercion = Coercion (a, a) (a, b)
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
instance Functor IO Coercion Coercion where fmap :: Coercion a b -> Coercion (IO a) (IO b)
fmap Coercion a b
Coercion = Coercion (IO a) (IO b)
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
instance Functor Complex Coercion Coercion where fmap :: Coercion a b -> Coercion (Complex a) (Complex b)
fmap Coercion a b
Coercion = Coercion (Complex a) (Complex b)
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion

instance Functor [] Discrete Discrete where fmap :: Discrete a b -> Discrete [a] [b]
fmap Discrete a b
Refl = Discrete [a] [b]
forall k (a :: k). Discrete a a
Refl
instance Functor Maybe Discrete Discrete where fmap :: Discrete a b -> Discrete (Maybe a) (Maybe b)
fmap Discrete a b
Refl = Discrete (Maybe a) (Maybe b)
forall k (a :: k). Discrete a a
Refl
instance Functor (Either a) Discrete Discrete where fmap :: Discrete a b -> Discrete (Either a a) (Either a b)
fmap Discrete a b
Refl = Discrete (Either a a) (Either a b)
forall k (a :: k). Discrete a a
Refl
instance Functor ((->) a) Discrete Discrete where fmap :: Discrete a b -> Discrete (a -> a) (a -> b)
fmap Discrete a b
Refl = Discrete (a -> a) (a -> b)
forall k (a :: k). Discrete a a
Refl
instance Functor ((,) a) Discrete Discrete where fmap :: Discrete a b -> Discrete (a, a) (a, b)
fmap Discrete a b
Refl = Discrete (a, a) (a, b)
forall k (a :: k). Discrete a a
Refl
instance Functor IO Discrete Discrete where fmap :: Discrete a b -> Discrete (IO a) (IO b)
fmap Discrete a b
Refl = Discrete (IO a) (IO b)
forall k (a :: k). Discrete a a
Refl
instance Functor Complex Discrete Discrete where fmap :: Discrete a b -> Discrete (Complex a) (Complex b)
fmap Discrete a b
Refl = Discrete (Complex a) (Complex b)
forall k (a :: k). Discrete a a
Refl