{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE RankNTypes #-}

module Data.Finitary.TreeRep(
  -- * Base Type and its algebra
  Rep, TreeRep(..),
  addRep, multRep, emptyRep, unitRep,

  -- ** Example representations
  idRep, maybeRep,

  -- ** Type-level @Rep@ algebra
  AddRep, MultRep,
  SRep(..), STreeRep(..),
  (%++), (%*), sEmptyRep, sUnitRep, sIdRep,
  KnownRep(..), KnownTreeRep(..),
  withKnownRep, withKnownTreeRep,
  
  -- * Evaluating @Rep@ as a Haskell 'Functor'
  Eval(..), EvalT(..),

  -- ** Correspondence between sums and products of @Rep@ and its evaluation
  fromSum, inlEval, inrEval, toSum,
  fromProduct, toProduct,
  absurdEval, unitEval,

  -- ** Profunctor traversal
  ptraverseEval, ptraverseEvalT,

  -- * Building bidirectional encodings as a @Eval r@ with @Profunctor@
  Encoder(..), idEncoder,
) where

import Data.Kind (Type)

import Data.Bifunctor (Bifunctor(..))
import Data.Void (absurd)
import Data.Functor.Classes ( Eq1(..), Ord1(..), compare1, eq1 )

import Data.Profunctor (Profunctor (..))
import Data.Profunctor.Cartesian
    ( Cartesian(proUnit, (***)), Cocartesian(proEmpty, (+++)) )
import Data.PTraversable

-- | Representation of a finitary functor.
--
-- If we write @{r}@ to mean the type @r :: Rep@
-- represents,
--
-- > r = [t1, t2, ...]
--
-- represent sum type
--
-- > {t1} + {t2} + ...
--
-- ==== Theories
--
-- @Rep@ can be thought of as a datatype representing
-- a thing called /skew semiring freely generated from one generator/.
-- 
-- Semiring is an abstract algebraic structure with addition and multiplication,
-- but not necessarily have subtraction. Typical instance of semiring is
-- @Integer@ or @Natural@.
--
-- Skew semiring is another abstract algebraic structure similar to semiring:
-- it has addition @+@ and multiplication @*@ with their respective units @0@ and @1@.
-- What differentiates skew semiring is it distinguishes /the order of additions/.
-- In any semiring, @x + y@ and @y + x@ must be equal; but in a skew semiring they can be
-- different.
-- 
-- Formally, a skew semiring is a set @A@ equipped with two binary operations @(+),(*) :: A -> A -> A@
-- and two nullary operations @0,1 :: A@, satisfying following equational axioms:
--
-- - Addition @(A, (+), 0)@ is a monoid
--   - @x + (y + z) === (x + y) + z@
--   - @x + 0 === x === 0 + x@
-- - Multiplication @(A, (*), 1)@ is a monoid
--   - @x * (y * z) === (x * y) * z@
--   - @x * 1 === x === 1 * x@
-- - Multiplication from right distributes to left addition
--   - @0 * z === 0@
--   - @(x + y) * z === (x * z) + (y * z)@
-- 
-- Note that both addition @(+)@ and multiplication @(*)@ are not guaranteed to be commutative,
-- and distributive law exists only for one side.
-- 
-- @Rep@ can be thought of as the free skew semiring on one generator @a@,
-- or in other words the type of normal forms of skew semiring expressions built from
-- @(+,*,0,1)@ and one variable @a@.
--
-- > Rep := 0 | TreeRep + Rep
-- > TreeRep := 1 | a * Rep
--
-- ==== Why skew semiring, and not a full semiring?
--
-- The 'Enum' class assigns every finitary type @x@ a canonical bijection @x ≅ Finite n@,
-- giving each value a unique index from @0@ to @n-1@. Two types with the same cardinality
-- are "equal" in the semiring when this bijection is /order-preserving/. Under this notion
-- of equality, the familiar type constructors satisfy /some/ semiring laws but not all:
--
-- [Addition is @Either@]
--   @Either a b@ encodes all @Left@-values before @Right@-values.
--   Concatenating the two sequences is order-preserving.
--
-- [Multiplication is @(,)@]
--   @(a, b)@ encodes in row-major (lexicographic) order: @(a₀,b₀),(a₀,b₁),…,(a₁,b₀),…@
--
-- [Right distributivity holds]
--   @(Either a b, c) ≅ Either (a,c) (b,c)@ is order-preserving:
--   the first @|a|·|c|@ indices map to @Left@, the remaining @|b|·|c|@ to @Right@. ✓
--
-- [Left distributivity fails]
--   @(a, Either b c) ≅ Either (a,b) (a,c)@ is NOT order-preserving in general.
--   The left side interleaves @b@- and @c@-values as it sweeps through @a@,
--   whereas the right side puts all @(a,b)@ pairs before all @(a,c)@ pairs. ✗
--
-- [Addition is not commutative]
--   @Either a b ≇ Either b a@ as ordered types: the first puts @a@-values first,
--   the second puts @b@-values first.
--
-- This is exactly the definition of a /skew/ semiring.
--
-- Because 'Rep' is the free skew semiring on one generator, 'Eval' @r a@ describes
-- finitary functors that respect this structure: given any 'Enum' instance for @a@,
-- 'Eval' @r a@ inherits a canonical 'Enum' instance determined entirely by @r@.

type Rep = [TreeRep]

-- | Representation of a simple (= not a sum of multiple reps)
--   finitary functor.
--
-- - @UnitRep@ represents a unit type: @{UnitRep}(a) = ()@.
-- - @ParRep r@ represents a type with one parameter type prepended:
--   @{ParRep r}(a) = (a, {r}(a))@.
data TreeRep =
    UnitRep
  | ParRep Rep
  deriving (TreeRep -> TreeRep -> Bool
(TreeRep -> TreeRep -> Bool)
-> (TreeRep -> TreeRep -> Bool) -> Eq TreeRep
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TreeRep -> TreeRep -> Bool
== :: TreeRep -> TreeRep -> Bool
$c/= :: TreeRep -> TreeRep -> Bool
/= :: TreeRep -> TreeRep -> Bool
Eq, Eq TreeRep
Eq TreeRep =>
(TreeRep -> TreeRep -> Ordering)
-> (TreeRep -> TreeRep -> Bool)
-> (TreeRep -> TreeRep -> Bool)
-> (TreeRep -> TreeRep -> Bool)
-> (TreeRep -> TreeRep -> Bool)
-> (TreeRep -> TreeRep -> TreeRep)
-> (TreeRep -> TreeRep -> TreeRep)
-> Ord TreeRep
TreeRep -> TreeRep -> Bool
TreeRep -> TreeRep -> Ordering
TreeRep -> TreeRep -> TreeRep
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: TreeRep -> TreeRep -> Ordering
compare :: TreeRep -> TreeRep -> Ordering
$c< :: TreeRep -> TreeRep -> Bool
< :: TreeRep -> TreeRep -> Bool
$c<= :: TreeRep -> TreeRep -> Bool
<= :: TreeRep -> TreeRep -> Bool
$c> :: TreeRep -> TreeRep -> Bool
> :: TreeRep -> TreeRep -> Bool
$c>= :: TreeRep -> TreeRep -> Bool
>= :: TreeRep -> TreeRep -> Bool
$cmax :: TreeRep -> TreeRep -> TreeRep
max :: TreeRep -> TreeRep -> TreeRep
$cmin :: TreeRep -> TreeRep -> TreeRep
min :: TreeRep -> TreeRep -> TreeRep
Ord, Int -> TreeRep -> ShowS
Rep -> ShowS
TreeRep -> String
(Int -> TreeRep -> ShowS)
-> (TreeRep -> String) -> (Rep -> ShowS) -> Show TreeRep
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TreeRep -> ShowS
showsPrec :: Int -> TreeRep -> ShowS
$cshow :: TreeRep -> String
show :: TreeRep -> String
$cshowList :: Rep -> ShowS
showList :: Rep -> ShowS
Show)

addRep :: Rep -> Rep -> Rep
addRep :: Rep -> Rep -> Rep
addRep = Rep -> Rep -> Rep
forall a. [a] -> [a] -> [a]
(++)

multRep :: Rep -> Rep -> Rep
multRep :: Rep -> Rep -> Rep
multRep Rep
r1 Rep
r2 = (TreeRep -> Rep) -> Rep -> Rep
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (TreeRep -> Rep -> Rep
`multTreeRep` Rep
r2) Rep
r1

emptyRep :: Rep
emptyRep :: Rep
emptyRep = []

unitRep :: Rep
unitRep :: Rep
unitRep = [TreeRep
UnitRep]

multTreeRep :: TreeRep -> Rep -> Rep
multTreeRep :: TreeRep -> Rep -> Rep
multTreeRep TreeRep
UnitRep Rep
r2 = Rep
r2
multTreeRep (ParRep Rep
s1) Rep
r2 = [Rep -> TreeRep
ParRep (Rep -> TreeRep) -> Rep -> TreeRep
forall a b. (a -> b) -> a -> b
$ Rep -> Rep -> Rep
multRep Rep
s1 Rep
r2]

-- | Representation of the identity functor
idRep :: Rep
idRep :: Rep
idRep = [Rep -> TreeRep
ParRep [TreeRep
UnitRep]]

-- | Representation of @Maybe@
maybeRep :: Rep
maybeRep :: Rep
maybeRep = TreeRep
UnitRep TreeRep -> Rep -> Rep
forall a. a -> [a] -> [a]
: Rep
idRep

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

-- * Type-level promoted Rep and its singleton reflection

-- | 'addRep' at type level
type family AddRep (r1 :: Rep) (r2 :: Rep) :: Rep where
  AddRep '[] r2 = r2
  AddRep (t ': r1) r2 = t : AddRep r1 r2

-- | 'multRep' at type level
type family MultRep (r1 :: Rep) (r2 :: Rep) :: Rep where
  MultRep '[] _ = '[]
  MultRep (UnitRep ': r1) r2 = AddRep r2 (MultRep r1 r2)
  MultRep (ParRep sub1 ': r1) r2 = ParRep (MultRep sub1 r2) ': MultRep r1 r2

-- | Singleton value for type-level @Rep@
data SRep (r :: Rep) where
  SEmpty :: SRep '[]
  SCase :: !(STreeRep t) -> !(SRep r) -> SRep (t ': r)

deriving instance Eq (SRep r)
deriving instance Ord (SRep r)
deriving instance Show (SRep r)

-- | Singleton value for type-level @TreeRep@
data STreeRep (t :: TreeRep) where
  SUnit :: STreeRep 'UnitRep
  SPar :: !(SRep r) -> STreeRep ('ParRep r)

deriving instance Show (STreeRep t)
deriving instance Eq (STreeRep r)
deriving instance Ord (STreeRep r)

-- | Compute the witness of 'AddRep'
(%++) :: SRep r1 -> SRep r2 -> SRep (AddRep r1 r2)
SRep r1
SEmpty %++ :: forall (r1 :: Rep) (r2 :: Rep).
SRep r1 -> SRep r2 -> SRep (AddRep r1 r2)
%++ SRep r2
sr2 = SRep r2
SRep (AddRep r1 r2)
sr2
SCase STreeRep t
st1 SRep r
sr1 %++ SRep r2
sr2 = STreeRep t -> SRep (AddRep r r2) -> SRep (t : AddRep r r2)
forall (r :: TreeRep) (t :: Rep).
STreeRep r -> SRep t -> SRep (r : t)
SCase STreeRep t
st1 (SRep r
sr1 SRep r -> SRep r2 -> SRep (AddRep r r2)
forall (r1 :: Rep) (r2 :: Rep).
SRep r1 -> SRep r2 -> SRep (AddRep r1 r2)
%++ SRep r2
sr2)

-- | Compute the witness of 'MultRep'
(%*) :: SRep r1 -> SRep r2 -> SRep (MultRep r1 r2)
SRep r1
sr1 %* :: forall (r1 :: Rep) (r2 :: Rep).
SRep r1 -> SRep r2 -> SRep (MultRep r1 r2)
%* SRep r2
sr2 = case SRep r1
sr1 of
  SRep r1
SEmpty -> SRep '[]
SRep (MultRep r1 r2)
SEmpty
  SCase STreeRep t
SUnit SRep r
sr1' -> SRep r2
sr2 SRep r2 -> SRep (MultRep r r2) -> SRep (AddRep r2 (MultRep r r2))
forall (r1 :: Rep) (r2 :: Rep).
SRep r1 -> SRep r2 -> SRep (AddRep r1 r2)
%++ (SRep r
sr1' SRep r -> SRep r2 -> SRep (MultRep r r2)
forall (r1 :: Rep) (r2 :: Rep).
SRep r1 -> SRep r2 -> SRep (MultRep r1 r2)
%* SRep r2
sr2)
  SCase (SPar SRep r
ssub1) SRep r
sr1' -> STreeRep ('ParRep (MultRep r r2))
-> SRep (MultRep r r2)
-> SRep ('ParRep (MultRep r r2) : MultRep r r2)
forall (r :: TreeRep) (t :: Rep).
STreeRep r -> SRep t -> SRep (r : t)
SCase (SRep (MultRep r r2) -> STreeRep ('ParRep (MultRep r r2))
forall (r :: Rep). SRep r -> STreeRep ('ParRep r)
SPar (SRep r
ssub1 SRep r -> SRep r2 -> SRep (MultRep r r2)
forall (r1 :: Rep) (r2 :: Rep).
SRep r1 -> SRep r2 -> SRep (MultRep r1 r2)
%* SRep r2
sr2)) (SRep r
sr1' SRep r -> SRep r2 -> SRep (MultRep r r2)
forall (r1 :: Rep) (r2 :: Rep).
SRep r1 -> SRep r2 -> SRep (MultRep r1 r2)
%* SRep r2
sr2)

sEmptyRep :: SRep '[]
sEmptyRep :: SRep '[]
sEmptyRep = SRep '[]
forall (r :: Rep). KnownRep r => SRep r
sRep

sUnitRep :: SRep '[ 'UnitRep ]
sUnitRep :: SRep '[ 'UnitRep]
sUnitRep = SRep '[ 'UnitRep]
forall (r :: Rep). KnownRep r => SRep r
sRep

sIdRep :: SRep '[ 'ParRep '[ 'UnitRep ] ]
sIdRep :: SRep '[ 'ParRep '[ 'UnitRep]]
sIdRep = SRep '[ 'ParRep '[ 'UnitRep]]
forall (r :: Rep). KnownRep r => SRep r
sRep

{-

TODO: promotion and demotion, and document (add,mult) corresponds
      between (Rep,SRep) using them

withSomeSRep :: Rep -> (forall rep. SRep rep -> result) -> result
demoteSRep :: SRep rep -> Rep

-}

-- ** Class based singleton value creation

class KnownRep (r :: Rep) where
  sRep :: SRep r

class KnownTreeRep (t :: TreeRep) where
  sTreeRep :: STreeRep t

instance KnownRep '[] where
  sRep :: SRep '[]
sRep = SRep '[]
SEmpty

instance (KnownTreeRep t, KnownRep r) => KnownRep (t ': r) where
  sRep :: SRep (t : r)
sRep = STreeRep t -> SRep r -> SRep (t : r)
forall (r :: TreeRep) (t :: Rep).
STreeRep r -> SRep t -> SRep (r : t)
SCase STreeRep t
forall (t :: TreeRep). KnownTreeRep t => STreeRep t
sTreeRep SRep r
forall (r :: Rep). KnownRep r => SRep r
sRep

instance KnownTreeRep 'UnitRep where
  sTreeRep :: STreeRep 'UnitRep
sTreeRep = STreeRep 'UnitRep
SUnit

instance KnownRep r => KnownTreeRep ('ParRep r) where
  sTreeRep :: STreeRep ('ParRep r)
sTreeRep = SRep r -> STreeRep ('ParRep r)
forall (r :: Rep). SRep r -> STreeRep ('ParRep r)
SPar SRep r
forall (r :: Rep). KnownRep r => SRep r
sRep

withKnownRep :: SRep r -> (KnownRep r => result) -> result
withKnownRep :: forall (r :: Rep) result.
SRep r -> (KnownRep r => result) -> result
withKnownRep SRep r
SEmpty KnownRep r => result
body = result
KnownRep r => result
body
withKnownRep (SCase STreeRep t
t SRep r
r) KnownRep r => result
body =
  STreeRep t -> (KnownTreeRep t => result) -> result
forall (t :: TreeRep) result.
STreeRep t -> (KnownTreeRep t => result) -> result
withKnownTreeRep STreeRep t
t (SRep r -> (KnownRep r => result) -> result
forall (r :: Rep) result.
SRep r -> (KnownRep r => result) -> result
withKnownRep SRep r
r result
KnownRep r => result
KnownRep r => result
body)

withKnownTreeRep :: STreeRep t -> (KnownTreeRep t => result) -> result
withKnownTreeRep :: forall (t :: TreeRep) result.
STreeRep t -> (KnownTreeRep t => result) -> result
withKnownTreeRep STreeRep t
SUnit KnownTreeRep t => result
body = result
KnownTreeRep t => result
body
withKnownTreeRep (SPar SRep r
r) KnownTreeRep t => result
body = SRep r -> (KnownRep r => result) -> result
forall (r :: Rep) result.
SRep r -> (KnownRep r => result) -> result
withKnownRep SRep r
r result
KnownTreeRep t => result
KnownRep r => result
body

{-

TODO: The current withKnown(Tree)Rep impl. is correct but
*very* inefficient: it basically tears down and reconstructs the
same singleton value.

A trick used in @reflection@ packages like this might work:

> newtype Requires c x = MkRequires (c => x)
> withKnownRep !r body = unsafeCoerce (MkRequires body) r

but I must study about these use of unsafe first.

-}


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

-- * Interpreting @Rep@ as a real data type

data Eval (r :: Rep) (a :: Type) where
  EHere :: !(EvalT t a) -> Eval (t ': r) a
  EThere :: !(Eval r a) -> Eval (t ': r) a

data EvalT (t :: TreeRep) (a :: Type) where
  EUnit :: EvalT 'UnitRep a
  EPar :: a -> Eval r a -> EvalT ('ParRep r) a

-- Instances

deriving instance Functor (Eval r)
deriving instance Foldable (Eval r)
deriving instance Traversable (Eval r)

ptraverseEval :: (Cartesian p, Cocartesian p)
  => SRep r -> p a b -> p (Eval r a) (Eval r b)
ptraverseEval :: forall (p :: * -> * -> *) (r :: Rep) a b.
(Cartesian p, Cocartesian p) =>
SRep r -> p a b -> p (Eval r a) (Eval r b)
ptraverseEval SRep r
r p a b
p = case SRep r
r of
  SRep r
SEmpty -> (Eval r a -> Void) -> p Void (Eval r b) -> p (Eval r a) (Eval r b)
forall a b c. (a -> b) -> p b c -> p a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap Eval r a -> Void
Eval '[] a -> Void
forall a any. Eval '[] a -> any
absurdEval p Void (Eval r b)
forall b. p Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty 
  SCase STreeRep t
t SRep r
r' -> (Eval r a -> Either (EvalT t a) (Eval r a))
-> (Either (EvalT t b) (Eval r b) -> Eval r b)
-> p (Either (EvalT t a) (Eval r a))
     (Either (EvalT t b) (Eval r b))
-> p (Eval r a) (Eval r b)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap Eval r a -> Either (EvalT t a) (Eval r a)
Eval (t : r) a -> Either (EvalT t a) (Eval r a)
forall (t :: TreeRep) (r :: Rep) c.
Eval (t : r) c -> Either (EvalT t c) (Eval r c)
splitEval Either (EvalT t b) (Eval r b) -> Eval r b
Either (EvalT t b) (Eval r b) -> Eval (t : r) b
forall (t :: TreeRep) (r :: Rep) c.
Either (EvalT t c) (Eval r c) -> Eval (t : r) c
mergeEval (STreeRep t -> p a b -> p (EvalT t a) (EvalT t b)
forall (p :: * -> * -> *) (t :: TreeRep) a b.
(Cartesian p, Cocartesian p) =>
STreeRep t -> p a b -> p (EvalT t a) (EvalT t b)
ptraverseEvalT STreeRep t
t p a b
p p (EvalT t a) (EvalT t b)
-> p (Eval r a) (Eval r b)
-> p (Either (EvalT t a) (Eval r a))
     (Either (EvalT t b) (Eval r b))
forall a b a' b'. p a b -> p a' b' -> p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ SRep r -> p a b -> p (Eval r a) (Eval r b)
forall (p :: * -> * -> *) (r :: Rep) a b.
(Cartesian p, Cocartesian p) =>
SRep r -> p a b -> p (Eval r a) (Eval r b)
ptraverseEval SRep r
r' p a b
p)
  where
    splitEval :: forall t r c.
      Eval (t ': r) c -> Either (EvalT t c) (Eval r c)
    splitEval :: forall (t :: TreeRep) (r :: Rep) c.
Eval (t : r) c -> Either (EvalT t c) (Eval r c)
splitEval (EHere EvalT t c
x) = EvalT t c -> Either (EvalT t c) (Eval r c)
forall a b. a -> Either a b
Left EvalT t c
EvalT t c
x
    splitEval (EThere Eval r c
x) = Eval r c -> Either (EvalT t c) (Eval r c)
forall a b. b -> Either a b
Right Eval r c
Eval r c
x

    mergeEval :: forall t r c.
      Either (EvalT t c) (Eval r c) -> Eval (t ': r) c
    mergeEval :: forall (t :: TreeRep) (r :: Rep) c.
Either (EvalT t c) (Eval r c) -> Eval (t : r) c
mergeEval = (EvalT t c -> Eval (t : r) c)
-> (Eval r c -> Eval (t : r) c)
-> Either (EvalT t c) (Eval r c)
-> Eval (t : r) c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either EvalT t c -> Eval (t : r) c
forall (r :: TreeRep) a (t :: Rep). EvalT r a -> Eval (r : t) a
EHere Eval r c -> Eval (t : r) c
forall (r :: Rep) a (t :: TreeRep). Eval r a -> Eval (t : r) a
EThere

ptraverseEvalT :: (Cartesian p, Cocartesian p)
  => STreeRep t -> p a b -> p (EvalT t a) (EvalT t b)
ptraverseEvalT :: forall (p :: * -> * -> *) (t :: TreeRep) a b.
(Cartesian p, Cocartesian p) =>
STreeRep t -> p a b -> p (EvalT t a) (EvalT t b)
ptraverseEvalT STreeRep t
t p a b
p = case STreeRep t
t of
  STreeRep t
SUnit -> (() -> EvalT t b) -> p (EvalT t a) () -> p (EvalT t a) (EvalT t b)
forall b c a. (b -> c) -> p a b -> p a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap (EvalT t b -> () -> EvalT t b
forall a b. a -> b -> a
const EvalT t b
EvalT 'UnitRep b
forall a. EvalT 'UnitRep a
EUnit) p (EvalT t a) ()
forall a. p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit
  SPar SRep r
r -> (EvalT t a -> (a, Eval r a))
-> ((b, Eval r b) -> EvalT t b)
-> p (a, Eval r a) (b, Eval r b)
-> p (EvalT t a) (EvalT t b)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap EvalT t a -> (a, Eval r a)
EvalT ('ParRep r) a -> (a, Eval r a)
forall (r :: Rep) c. EvalT ('ParRep r) c -> (c, Eval r c)
unEPar ((b -> Eval r b -> EvalT t b) -> (b, Eval r b) -> EvalT t b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry b -> Eval r b -> EvalT t b
b -> Eval r b -> EvalT ('ParRep r) b
forall a (r :: Rep). a -> Eval r a -> EvalT ('ParRep r) a
EPar) (p a b
p p a b -> p (Eval r a) (Eval r b) -> p (a, Eval r a) (b, Eval r b)
forall a b a' b'. p a b -> p a' b' -> p (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** SRep r -> p a b -> p (Eval r a) (Eval r b)
forall (p :: * -> * -> *) (r :: Rep) a b.
(Cartesian p, Cocartesian p) =>
SRep r -> p a b -> p (Eval r a) (Eval r b)
ptraverseEval SRep r
r p a b
p)
  where
    unEPar :: forall r c. EvalT (ParRep r) c -> (c, Eval r c)
    unEPar :: forall (r :: Rep) c. EvalT ('ParRep r) c -> (c, Eval r c)
unEPar (EPar c
a Eval r c
x) = (c
a,Eval r c
Eval r c
x)

instance KnownRep r => PTraversable (Eval r) where
  ptraverseWith :: forall (p :: * -> * -> *) as a b bs.
(Cartesian p, Cocartesian p) =>
(as -> Eval r a) -> (Eval r b -> bs) -> p a b -> p as bs
ptraverseWith as -> Eval r a
from Eval r b -> bs
to = (as -> Eval r a)
-> (Eval r b -> bs) -> p (Eval r a) (Eval r b) -> p as bs
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap as -> Eval r a
from Eval r b -> bs
to (p (Eval r a) (Eval r b) -> p as bs)
-> (p a b -> p (Eval r a) (Eval r b)) -> p a b -> p as bs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SRep r -> p a b -> p (Eval r a) (Eval r b)
forall (p :: * -> * -> *) (r :: Rep) a b.
(Cartesian p, Cocartesian p) =>
SRep r -> p a b -> p (Eval r a) (Eval r b)
ptraverseEval SRep r
forall (r :: Rep). KnownRep r => SRep r
sRep

deriving instance Functor (EvalT t)
deriving instance Foldable (EvalT t)
deriving instance Traversable (EvalT t)

instance KnownTreeRep t => PTraversable (EvalT t) where
  ptraverseWith :: forall (p :: * -> * -> *) as a b bs.
(Cartesian p, Cocartesian p) =>
(as -> EvalT t a) -> (EvalT t b -> bs) -> p a b -> p as bs
ptraverseWith as -> EvalT t a
from EvalT t b -> bs
to = (as -> EvalT t a)
-> (EvalT t b -> bs) -> p (EvalT t a) (EvalT t b) -> p as bs
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap as -> EvalT t a
from EvalT t b -> bs
to (p (EvalT t a) (EvalT t b) -> p as bs)
-> (p a b -> p (EvalT t a) (EvalT t b)) -> p a b -> p as bs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STreeRep t -> p a b -> p (EvalT t a) (EvalT t b)
forall (p :: * -> * -> *) (t :: TreeRep) a b.
(Cartesian p, Cocartesian p) =>
STreeRep t -> p a b -> p (EvalT t a) (EvalT t b)
ptraverseEvalT STreeRep t
forall (t :: TreeRep). KnownTreeRep t => STreeRep t
sTreeRep

instance Eq a => Eq (Eval r a) where
  == :: Eval r a -> Eval r a -> Bool
(==) = Eval r a -> Eval r a -> Bool
forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1

instance Eq1 (Eval r) where
  liftEq :: forall a b. (a -> b -> Bool) -> Eval r a -> Eval r b -> Bool
liftEq a -> b -> Bool
eq (EHere EvalT t a
x) (EHere EvalT t b
y) = (a -> b -> Bool) -> EvalT t a -> EvalT t b -> Bool
forall a b. (a -> b -> Bool) -> EvalT t a -> EvalT t b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
eq EvalT t a
x EvalT t b
EvalT t b
y
  liftEq a -> b -> Bool
eq (EThere Eval r a
x) (EThere Eval r b
y) = (a -> b -> Bool) -> Eval r a -> Eval r b -> Bool
forall a b. (a -> b -> Bool) -> Eval r a -> Eval r b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
eq Eval r a
x Eval r b
Eval r b
y
  -- mismatched constructors
  liftEq a -> b -> Bool
_ Eval r a
_ Eval r b
_ = Bool
False

instance Eq a => Eq (EvalT t a) where
  == :: EvalT t a -> EvalT t a -> Bool
(==) = EvalT t a -> EvalT t a -> Bool
forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1

instance Eq1 (EvalT t) where
  liftEq :: forall a b. (a -> b -> Bool) -> EvalT t a -> EvalT t b -> Bool
liftEq a -> b -> Bool
_ EvalT t a
EUnit EvalT t b
EUnit = Bool
True
  liftEq a -> b -> Bool
eq (EPar a
a Eval r a
x) (EPar b
b Eval r b
y) = a -> b -> Bool
eq a
a b
b Bool -> Bool -> Bool
&& (a -> b -> Bool) -> Eval r a -> Eval r b -> Bool
forall a b. (a -> b -> Bool) -> Eval r a -> Eval r b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
eq Eval r a
x Eval r b
Eval r b
y

instance Ord a => Ord (Eval r a) where
  compare :: Eval r a -> Eval r a -> Ordering
compare = Eval r a -> Eval r a -> Ordering
forall (f :: * -> *) a. (Ord1 f, Ord a) => f a -> f a -> Ordering
compare1

instance Ord1 (Eval r) where
  liftCompare :: forall a b.
(a -> b -> Ordering) -> Eval r a -> Eval r b -> Ordering
liftCompare a -> b -> Ordering
cmp (EHere EvalT t a
x) (EHere EvalT t b
y) = (a -> b -> Ordering) -> EvalT t a -> EvalT t b -> Ordering
forall a b.
(a -> b -> Ordering) -> EvalT t a -> EvalT t b -> Ordering
forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare a -> b -> Ordering
cmp EvalT t a
x EvalT t b
EvalT t b
y
  liftCompare a -> b -> Ordering
_   (EHere EvalT t a
_) (EThere Eval r b
_) = Ordering
LT
  liftCompare a -> b -> Ordering
_   (EThere Eval r a
_) (EHere EvalT t b
_) = Ordering
GT
  liftCompare a -> b -> Ordering
cmp (EThere Eval r a
x) (EThere Eval r b
y) = (a -> b -> Ordering) -> Eval r a -> Eval r b -> Ordering
forall a b.
(a -> b -> Ordering) -> Eval r a -> Eval r b -> Ordering
forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare a -> b -> Ordering
cmp Eval r a
x Eval r b
Eval r b
y

instance Ord a => Ord (EvalT t a) where
  compare :: EvalT t a -> EvalT t a -> Ordering
compare = EvalT t a -> EvalT t a -> Ordering
forall (f :: * -> *) a. (Ord1 f, Ord a) => f a -> f a -> Ordering
compare1

instance Ord1 (EvalT t) where
  liftCompare :: forall a b.
(a -> b -> Ordering) -> EvalT t a -> EvalT t b -> Ordering
liftCompare a -> b -> Ordering
_ EvalT t a
EUnit EvalT t b
EUnit = Ordering
EQ
  liftCompare a -> b -> Ordering
cmp (EPar a
a Eval r a
x) (EPar b
b Eval r b
y) = a -> b -> Ordering
cmp a
a b
b Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> (a -> b -> Ordering) -> Eval r a -> Eval r b -> Ordering
forall a b.
(a -> b -> Ordering) -> Eval r a -> Eval r b -> Ordering
forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare a -> b -> Ordering
cmp Eval r a
x Eval r b
Eval r b
y

-- ** Add/Mult of @Rep@ corresponds to sum/product of Eval

absurdEval :: Eval '[] a -> any
absurdEval :: forall a any. Eval '[] a -> any
absurdEval Eval '[] a
x = case Eval '[] a
x of {}

unitEval :: Eval '[UnitRep] a
unitEval :: forall a. Eval '[ 'UnitRep] a
unitEval = EvalT 'UnitRep a -> Eval '[ 'UnitRep] a
forall (r :: TreeRep) a (t :: Rep). EvalT r a -> Eval (r : t) a
EHere EvalT 'UnitRep a
forall a. EvalT 'UnitRep a
EUnit

fromSum :: SRep r1 -> proxy r2 -> Either (Eval r1 x) (Eval r2 x) -> Eval (AddRep r1 r2) x
fromSum :: forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1
-> proxy r2
-> Either (Eval r1 x) (Eval r2 x)
-> Eval (AddRep r1 r2) x
fromSum SRep r1
r1 proxy r2
r2 = (Eval r1 x -> Eval (AddRep r1 r2) x)
-> (Eval r2 x -> Eval (AddRep r1 r2) x)
-> Either (Eval r1 x) (Eval r2 x)
-> Eval (AddRep r1 r2) x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (SRep r1 -> proxy r2 -> Eval r1 x -> Eval (AddRep r1 r2) x
forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1 -> proxy r2 -> Eval r1 x -> Eval (AddRep r1 r2) x
inlEval SRep r1
r1 proxy r2
r2) (SRep r1 -> proxy r2 -> Eval r2 x -> Eval (AddRep r1 r2) x
forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1 -> proxy r2 -> Eval r2 x -> Eval (AddRep r1 r2) x
inrEval SRep r1
r1 proxy r2
r2)

inlEval :: SRep r1 -> proxy r2 -> Eval r1 x -> Eval (AddRep r1 r2) x
inlEval :: forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1 -> proxy r2 -> Eval r1 x -> Eval (AddRep r1 r2) x
inlEval SRep r1
SEmpty proxy r2
_ Eval r1 x
x = Eval '[] x -> Eval r2 x
forall a any. Eval '[] a -> any
absurdEval Eval r1 x
Eval '[] x
x
inlEval (SCase STreeRep t
_ SRep r
r1) proxy r2
r2 Eval r1 x
x = case Eval r1 x
x of
  EHere EvalT t x
x' -> EvalT t x -> Eval (t : AddRep r r2) x
forall (r :: TreeRep) a (t :: Rep). EvalT r a -> Eval (r : t) a
EHere EvalT t x
x'
  EThere Eval r x
x' -> Eval (AddRep r r2) x -> Eval (t : AddRep r r2) x
forall (r :: Rep) a (t :: TreeRep). Eval r a -> Eval (t : r) a
EThere (SRep r -> proxy r2 -> Eval r x -> Eval (AddRep r r2) x
forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1 -> proxy r2 -> Eval r1 x -> Eval (AddRep r1 r2) x
inlEval SRep r
r1 proxy r2
r2 Eval r x
Eval r x
x')

inrEval :: SRep r1 -> proxy r2 -> Eval r2 x -> Eval (AddRep r1 r2) x
inrEval :: forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1 -> proxy r2 -> Eval r2 x -> Eval (AddRep r1 r2) x
inrEval SRep r1
SEmpty proxy r2
_ Eval r2 x
y = Eval r2 x
Eval (AddRep r1 r2) x
y
inrEval (SCase STreeRep t
_ SRep r
r1) proxy r2
r2 Eval r2 x
y = Eval (AddRep r r2) x -> Eval (t : AddRep r r2) x
forall (r :: Rep) a (t :: TreeRep). Eval r a -> Eval (t : r) a
EThere (SRep r -> proxy r2 -> Eval r2 x -> Eval (AddRep r r2) x
forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1 -> proxy r2 -> Eval r2 x -> Eval (AddRep r1 r2) x
inrEval SRep r
r1 proxy r2
r2 Eval r2 x
y)

toSum :: SRep r1 -> proxy r2 -> Eval (AddRep r1 r2) x -> Either (Eval r1 x) (Eval r2 x)
toSum :: forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1
-> proxy r2
-> Eval (AddRep r1 r2) x
-> Either (Eval r1 x) (Eval r2 x)
toSum SRep r1
SEmpty proxy r2
_r2 Eval (AddRep r1 r2) x
z = Eval r2 x -> Either (Eval r1 x) (Eval r2 x)
forall a b. b -> Either a b
Right Eval r2 x
Eval (AddRep r1 r2) x
z
toSum (SCase STreeRep t
_ SRep r
r1) proxy r2
r2 Eval (AddRep r1 r2) x
z = case Eval (AddRep r1 r2) x
z of
  EHere EvalT t x
x -> Eval r1 x -> Either (Eval r1 x) (Eval r2 x)
forall a b. a -> Either a b
Left (EvalT t x -> Eval (t : r) x
forall (r :: TreeRep) a (t :: Rep). EvalT r a -> Eval (r : t) a
EHere EvalT t x
x)
  EThere Eval r x
z' -> (Eval r x -> Eval r1 x)
-> Either (Eval r x) (Eval r2 x) -> Either (Eval r1 x) (Eval r2 x)
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Eval r x -> Eval r1 x
Eval r x -> Eval (t : r) x
forall (r :: Rep) a (t :: TreeRep). Eval r a -> Eval (t : r) a
EThere (Either (Eval r x) (Eval r2 x) -> Either (Eval r1 x) (Eval r2 x))
-> Either (Eval r x) (Eval r2 x) -> Either (Eval r1 x) (Eval r2 x)
forall a b. (a -> b) -> a -> b
$ SRep r
-> proxy r2
-> Eval (AddRep r r2) x
-> Either (Eval r x) (Eval r2 x)
forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1
-> proxy r2
-> Eval (AddRep r1 r2) x
-> Either (Eval r1 x) (Eval r2 x)
toSum SRep r
r1 proxy r2
r2 Eval r x
Eval (AddRep r r2) x
z'

fromProduct :: SRep r1 -> SRep r2 -> Eval r1 x -> Eval r2 x -> Eval (MultRep r1 r2) x
fromProduct :: forall (r1 :: Rep) (r2 :: Rep) x.
SRep r1
-> SRep r2 -> Eval r1 x -> Eval r2 x -> Eval (MultRep r1 r2) x
fromProduct SRep r1
r1 SRep r2
r2 Eval r1 x
x Eval r2 x
y = case SRep r1
r1 of
  SRep r1
SEmpty -> Eval '[] x -> Eval '[] x
forall a any. Eval '[] a -> any
absurdEval Eval r1 x
Eval '[] x
x
  SCase STreeRep t
SUnit SRep r
r1' -> case Eval r1 x
x of
    EHere EvalT t x
EUnit -> SRep r2
-> SRep (MultRep r r2)
-> Eval r2 x
-> Eval (AddRep r2 (MultRep r r2)) x
forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1 -> proxy r2 -> Eval r1 x -> Eval (AddRep r1 r2) x
inlEval SRep r2
r2 (SRep r
r1' SRep r -> SRep r2 -> SRep (MultRep r r2)
forall (r1 :: Rep) (r2 :: Rep).
SRep r1 -> SRep r2 -> SRep (MultRep r1 r2)
%* SRep r2
r2) Eval r2 x
y
    EThere Eval r x
x' -> SRep r2
-> SRep (MultRep r r2)
-> Eval (MultRep r r2) x
-> Eval (AddRep r2 (MultRep r r2)) x
forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1 -> proxy r2 -> Eval r2 x -> Eval (AddRep r1 r2) x
inrEval SRep r2
r2 (SRep r
r1' SRep r -> SRep r2 -> SRep (MultRep r r2)
forall (r1 :: Rep) (r2 :: Rep).
SRep r1 -> SRep r2 -> SRep (MultRep r1 r2)
%* SRep r2
r2) (SRep r -> SRep r2 -> Eval r x -> Eval r2 x -> Eval (MultRep r r2) x
forall (r1 :: Rep) (r2 :: Rep) x.
SRep r1
-> SRep r2 -> Eval r1 x -> Eval r2 x -> Eval (MultRep r1 r2) x
fromProduct SRep r
r1' SRep r2
r2 Eval r x
Eval r x
x' Eval r2 x
y)
  SCase (SPar SRep r
sub1) SRep r
r1' -> case Eval r1 x
x of
    EHere (EPar x
a Eval r x
x') -> EvalT ('ParRep (MultRep r r2)) x
-> Eval ('ParRep (MultRep r r2) : MultRep r r2) x
forall (r :: TreeRep) a (t :: Rep). EvalT r a -> Eval (r : t) a
EHere (x -> Eval (MultRep r r2) x -> EvalT ('ParRep (MultRep r r2)) x
forall a (r :: Rep). a -> Eval r a -> EvalT ('ParRep r) a
EPar x
a (SRep r -> SRep r2 -> Eval r x -> Eval r2 x -> Eval (MultRep r r2) x
forall (r1 :: Rep) (r2 :: Rep) x.
SRep r1
-> SRep r2 -> Eval r1 x -> Eval r2 x -> Eval (MultRep r1 r2) x
fromProduct SRep r
sub1 SRep r2
r2 Eval r x
Eval r x
x' Eval r2 x
y))
    EThere Eval r x
x' -> Eval (MultRep r r2) x
-> Eval ('ParRep (MultRep r r2) : MultRep r r2) x
forall (r :: Rep) a (t :: TreeRep). Eval r a -> Eval (t : r) a
EThere (SRep r -> SRep r2 -> Eval r x -> Eval r2 x -> Eval (MultRep r r2) x
forall (r1 :: Rep) (r2 :: Rep) x.
SRep r1
-> SRep r2 -> Eval r1 x -> Eval r2 x -> Eval (MultRep r1 r2) x
fromProduct SRep r
r1' SRep r2
r2 Eval r x
Eval r x
x' Eval r2 x
y)

toProduct :: SRep r1 -> SRep r2 -> Eval (MultRep r1 r2) x -> (Eval r1 x, Eval r2 x)
toProduct :: forall (r1 :: Rep) (r2 :: Rep) x.
SRep r1
-> SRep r2 -> Eval (MultRep r1 r2) x -> (Eval r1 x, Eval r2 x)
toProduct SRep r1
r1 SRep r2
r2 Eval (MultRep r1 r2) x
z = case SRep r1
r1 of
  SRep r1
SEmpty -> Eval '[] x -> (Eval r1 x, Eval r2 x)
forall a any. Eval '[] a -> any
absurdEval Eval '[] x
Eval (MultRep r1 r2) x
z
  SCase STreeRep t
SUnit SRep r
r1' -> case SRep r2
-> SRep (MultRep r r2)
-> Eval (AddRep r2 (MultRep r r2)) x
-> Either (Eval r2 x) (Eval (MultRep r r2) x)
forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1
-> proxy r2
-> Eval (AddRep r1 r2) x
-> Either (Eval r1 x) (Eval r2 x)
toSum SRep r2
r2 (SRep r
r1' SRep r -> SRep r2 -> SRep (MultRep r r2)
forall (r1 :: Rep) (r2 :: Rep).
SRep r1 -> SRep r2 -> SRep (MultRep r1 r2)
%* SRep r2
r2) Eval (MultRep r1 r2) x
Eval (AddRep r2 (MultRep r r2)) x
z of
    Left Eval r2 x
y -> (EvalT 'UnitRep x -> Eval ('UnitRep : r) x
forall (r :: TreeRep) a (t :: Rep). EvalT r a -> Eval (r : t) a
EHere EvalT 'UnitRep x
forall a. EvalT 'UnitRep a
EUnit, Eval r2 x
y)
    Right Eval (MultRep r r2) x
z' -> (Eval r x -> Eval r1 x)
-> (Eval r x, Eval r2 x) -> (Eval r1 x, Eval r2 x)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Eval r x -> Eval r1 x
Eval r x -> Eval ('UnitRep : r) x
forall (r :: Rep) a (t :: TreeRep). Eval r a -> Eval (t : r) a
EThere ((Eval r x, Eval r2 x) -> (Eval r1 x, Eval r2 x))
-> (Eval r x, Eval r2 x) -> (Eval r1 x, Eval r2 x)
forall a b. (a -> b) -> a -> b
$ SRep r -> SRep r2 -> Eval (MultRep r r2) x -> (Eval r x, Eval r2 x)
forall (r1 :: Rep) (r2 :: Rep) x.
SRep r1
-> SRep r2 -> Eval (MultRep r1 r2) x -> (Eval r1 x, Eval r2 x)
toProduct SRep r
r1' SRep r2
r2 Eval (MultRep r r2) x
z'
  SCase (SPar SRep r
sub1) SRep r
r1' -> case Eval (MultRep r1 r2) x
z of
    EHere (EPar x
a Eval r x
z') -> (Eval r x -> Eval r1 x)
-> (Eval r x, Eval r2 x) -> (Eval r1 x, Eval r2 x)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (EvalT ('ParRep r) x -> Eval r1 x
EvalT ('ParRep r) x -> Eval ('ParRep r : r) x
forall (r :: TreeRep) a (t :: Rep). EvalT r a -> Eval (r : t) a
EHere (EvalT ('ParRep r) x -> Eval r1 x)
-> (Eval r x -> EvalT ('ParRep r) x) -> Eval r x -> Eval r1 x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Eval r x -> EvalT ('ParRep r) x
forall a (r :: Rep). a -> Eval r a -> EvalT ('ParRep r) a
EPar x
a) ((Eval r x, Eval r2 x) -> (Eval r1 x, Eval r2 x))
-> (Eval r x, Eval r2 x) -> (Eval r1 x, Eval r2 x)
forall a b. (a -> b) -> a -> b
$ SRep r -> SRep r2 -> Eval (MultRep r r2) x -> (Eval r x, Eval r2 x)
forall (r1 :: Rep) (r2 :: Rep) x.
SRep r1
-> SRep r2 -> Eval (MultRep r1 r2) x -> (Eval r1 x, Eval r2 x)
toProduct SRep r
sub1 SRep r2
r2 Eval r x
Eval (MultRep r r2) x
z'
    EThere Eval r x
z' -> (Eval r x -> Eval r1 x)
-> (Eval r x, Eval r2 x) -> (Eval r1 x, Eval r2 x)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Eval r x -> Eval r1 x
Eval r x -> Eval ('ParRep r : r) x
forall (r :: Rep) a (t :: TreeRep). Eval r a -> Eval (t : r) a
EThere ((Eval r x, Eval r2 x) -> (Eval r1 x, Eval r2 x))
-> (Eval r x, Eval r2 x) -> (Eval r1 x, Eval r2 x)
forall a b. (a -> b) -> a -> b
$ SRep r -> SRep r2 -> Eval (MultRep r r2) x -> (Eval r x, Eval r2 x)
forall (r1 :: Rep) (r2 :: Rep) x.
SRep r1
-> SRep r2 -> Eval (MultRep r1 r2) x -> (Eval r1 x, Eval r2 x)
toProduct SRep r
r1' SRep r2
r2 Eval r x
Eval (MultRep r r2) x
z'

-- * Encoding / Decoding

data Encoder a b s t where
  Encoder :: !(SRep r) -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t

-- | Encoder for the identity functor.
--
--   It can be used to construct an encoder for arbitrary 'PTraversable'
--   functor using @'ptraverse' 'idEncoder'@.
idEncoder :: Encoder a b a b
idEncoder :: forall a b. Encoder a b a b
idEncoder = SRep '[ 'ParRep '[ 'UnitRep]]
-> (a -> Eval '[ 'ParRep '[ 'UnitRep]] a)
-> (Eval '[ 'ParRep '[ 'UnitRep]] b -> b)
-> Encoder a b a b
forall (r :: Rep) s a b t.
SRep r -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t
Encoder SRep '[ 'ParRep '[ 'UnitRep]]
sIdRep a -> Eval '[ 'ParRep '[ 'UnitRep]] a
forall c. c -> Eval '[ 'ParRep '[ 'UnitRep]] c
idEnc Eval '[ 'ParRep '[ 'UnitRep]] b -> b
forall c. Eval '[ 'ParRep '[ 'UnitRep]] c -> c
idDec
  where
    idEnc :: c -> Eval '[ParRep '[UnitRep]] c
    idEnc :: forall c. c -> Eval '[ 'ParRep '[ 'UnitRep]] c
idEnc c
c = EvalT ('ParRep '[ 'UnitRep]) c -> Eval '[ 'ParRep '[ 'UnitRep]] c
forall (r :: TreeRep) a (t :: Rep). EvalT r a -> Eval (r : t) a
EHere (c -> Eval '[ 'UnitRep] c -> EvalT ('ParRep '[ 'UnitRep]) c
forall a (r :: Rep). a -> Eval r a -> EvalT ('ParRep r) a
EPar c
c Eval '[ 'UnitRep] c
forall a. Eval '[ 'UnitRep] a
unitEval)
    
    idDec :: Eval '[ParRep '[UnitRep]] c -> c
    idDec :: forall c. Eval '[ 'ParRep '[ 'UnitRep]] c -> c
idDec (EHere (EPar c
c Eval r c
_)) = c
c
    -- @EThere rest@ case is unnecessary to be
    -- a complete pattern match, because @rest@ has
    -- an uninhabited type @Eval '[] c@.

deriving instance Functor (Encoder a b s)

instance Profunctor (Encoder a b) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> Encoder a b b c -> Encoder a b a d
dimap a -> b
f c -> d
g (Encoder SRep r
rep b -> Eval r a
enc Eval r b -> c
dec) = SRep r -> (a -> Eval r a) -> (Eval r b -> d) -> Encoder a b a d
forall (r :: Rep) s a b t.
SRep r -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t
Encoder SRep r
rep (b -> Eval r a
enc (b -> Eval r a) -> (a -> b) -> a -> Eval r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) (c -> d
g (c -> d) -> (Eval r b -> c) -> Eval r b -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eval r b -> c
dec)
  lmap :: forall a b c. (a -> b) -> Encoder a b b c -> Encoder a b a c
lmap a -> b
f (Encoder SRep r
rep b -> Eval r a
enc Eval r b -> c
dec) = SRep r -> (a -> Eval r a) -> (Eval r b -> c) -> Encoder a b a c
forall (r :: Rep) s a b t.
SRep r -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t
Encoder SRep r
rep (b -> Eval r a
enc (b -> Eval r a) -> (a -> b) -> a -> Eval r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) Eval r b -> c
dec
  rmap :: forall b c a. (b -> c) -> Encoder a b a b -> Encoder a b a c
rmap = (b -> c) -> Encoder a b a b -> Encoder a b a c
forall a b. (a -> b) -> Encoder a b a a -> Encoder a b a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap

instance Cartesian (Encoder a b) where
  proUnit :: forall a. Encoder a b a ()
proUnit = SRep '[ 'UnitRep]
-> (a -> Eval '[ 'UnitRep] a)
-> (Eval '[ 'UnitRep] b -> ())
-> Encoder a b a ()
forall (r :: Rep) s a b t.
SRep r -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t
Encoder (STreeRep 'UnitRep -> SRep '[] -> SRep '[ 'UnitRep]
forall (r :: TreeRep) (t :: Rep).
STreeRep r -> SRep t -> SRep (r : t)
SCase STreeRep 'UnitRep
SUnit SRep '[]
SEmpty) (Eval '[ 'UnitRep] a -> a -> Eval '[ 'UnitRep] a
forall a b. a -> b -> a
const (EvalT 'UnitRep a -> Eval '[ 'UnitRep] a
forall (r :: TreeRep) a (t :: Rep). EvalT r a -> Eval (r : t) a
EHere EvalT 'UnitRep a
forall a. EvalT 'UnitRep a
EUnit)) (() -> Eval '[ 'UnitRep] b -> ()
forall a b. a -> b -> a
const ())
  (Encoder SRep r
r1 a -> Eval r a
enc1 Eval r b -> b
dec1) *** :: forall a b a' b'.
Encoder a b a b -> Encoder a b a' b' -> Encoder a b (a, a') (b, b')
*** (Encoder SRep r
r2 a' -> Eval r a
enc2 Eval r b -> b'
dec2) =
    let enc :: (a, a') -> Eval (MultRep r r) a
enc (a
s1, a'
s2) = SRep r -> SRep r -> Eval r a -> Eval r a -> Eval (MultRep r r) a
forall (r1 :: Rep) (r2 :: Rep) x.
SRep r1
-> SRep r2 -> Eval r1 x -> Eval r2 x -> Eval (MultRep r1 r2) x
fromProduct SRep r
r1 SRep r
r2 (a -> Eval r a
enc1 a
s1) (a' -> Eval r a
enc2 a'
s2)
        dec :: Eval (MultRep r r) b -> (b, b')
dec = (Eval r b -> b)
-> (Eval r b -> b') -> (Eval r b, Eval r b) -> (b, b')
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Eval r b -> b
dec1 Eval r b -> b'
dec2 ((Eval r b, Eval r b) -> (b, b'))
-> (Eval (MultRep r r) b -> (Eval r b, Eval r b))
-> Eval (MultRep r r) b
-> (b, b')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SRep r -> SRep r -> Eval (MultRep r r) b -> (Eval r b, Eval r b)
forall (r1 :: Rep) (r2 :: Rep) x.
SRep r1
-> SRep r2 -> Eval (MultRep r1 r2) x -> (Eval r1 x, Eval r2 x)
toProduct SRep r
r1 SRep r
r2
    in SRep (MultRep r r)
-> ((a, a') -> Eval (MultRep r r) a)
-> (Eval (MultRep r r) b -> (b, b'))
-> Encoder a b (a, a') (b, b')
forall (r :: Rep) s a b t.
SRep r -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t
Encoder (SRep r
r1 SRep r -> SRep r -> SRep (MultRep r r)
forall (r1 :: Rep) (r2 :: Rep).
SRep r1 -> SRep r2 -> SRep (MultRep r1 r2)
%* SRep r
r2) (a, a') -> Eval (MultRep r r) a
enc Eval (MultRep r r) b -> (b, b')
dec

instance Cocartesian (Encoder a b) where
  proEmpty :: forall b. Encoder a b Void b
proEmpty = SRep '[]
-> (Void -> Eval '[] a) -> (Eval '[] b -> b) -> Encoder a b Void b
forall (r :: Rep) s a b t.
SRep r -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t
Encoder SRep '[]
SEmpty Void -> Eval '[] a
forall a. Void -> a
absurd Eval '[] b -> b
forall a any. Eval '[] a -> any
absurdEval
  (Encoder SRep r
r1 a -> Eval r a
enc1 Eval r b -> b
dec1) +++ :: forall a b a' b'.
Encoder a b a b
-> Encoder a b a' b' -> Encoder a b (Either a a') (Either b b')
+++ (Encoder SRep r
r2 a' -> Eval r a
enc2 Eval r b -> b'
dec2) =
    let enc :: Either a a' -> Eval (AddRep r r) a
enc = (a -> Eval (AddRep r r) a)
-> (a' -> Eval (AddRep r r) a)
-> Either a a'
-> Eval (AddRep r r) a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (SRep r -> SRep r -> Eval r a -> Eval (AddRep r r) a
forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1 -> proxy r2 -> Eval r1 x -> Eval (AddRep r1 r2) x
inlEval SRep r
r1 SRep r
r2 (Eval r a -> Eval (AddRep r r) a)
-> (a -> Eval r a) -> a -> Eval (AddRep r r) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eval r a
enc1) (SRep r -> SRep r -> Eval r a -> Eval (AddRep r r) a
forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1 -> proxy r2 -> Eval r2 x -> Eval (AddRep r1 r2) x
inrEval SRep r
r1 SRep r
r2 (Eval r a -> Eval (AddRep r r) a)
-> (a' -> Eval r a) -> a' -> Eval (AddRep r r) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a' -> Eval r a
enc2)
        dec :: Eval (AddRep r r) b -> Either b b'
dec = (Eval r b -> b)
-> (Eval r b -> b') -> Either (Eval r b) (Eval r b) -> Either b b'
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Eval r b -> b
dec1 Eval r b -> b'
dec2 (Either (Eval r b) (Eval r b) -> Either b b')
-> (Eval (AddRep r r) b -> Either (Eval r b) (Eval r b))
-> Eval (AddRep r r) b
-> Either b b'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SRep r
-> SRep r -> Eval (AddRep r r) b -> Either (Eval r b) (Eval r b)
forall (r1 :: Rep) (proxy :: Rep -> *) (r2 :: Rep) x.
SRep r1
-> proxy r2
-> Eval (AddRep r1 r2) x
-> Either (Eval r1 x) (Eval r2 x)
toSum SRep r
r1 SRep r
r2
    in SRep (AddRep r r)
-> (Either a a' -> Eval (AddRep r r) a)
-> (Eval (AddRep r r) b -> Either b b')
-> Encoder a b (Either a a') (Either b b')
forall (r :: Rep) s a b t.
SRep r -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t
Encoder (SRep r
r1 SRep r -> SRep r -> SRep (AddRep r r)
forall (r1 :: Rep) (r2 :: Rep).
SRep r1 -> SRep r2 -> SRep (AddRep r1 r2)
%++ SRep r
r2) Either a a' -> Eval (AddRep r r) a
enc Eval (AddRep r r) b -> Either b b'
dec