{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE LambdaCase #-}

-- | A normalized polynomial representation for finitary polynomial functors.
--
-- Compared with "Data.Finitary.TreeRep", this module forgets the
-- syntactic tree structure of sums and products and represents a functor as
--
-- > x^n1 + x^n2 + ... + x^nk
--
-- This is especially useful for Day convolution: monomials satisfy
--
-- > Day x^m x^n ≅ x^(m*n)
--
-- which is implemented by 'DayPoly', 'fromDay', and 'toDay'.
--
-- The list order in 'Poly' is operationally significant in Haskell, but
-- mathematically it should be regarded as a chosen ordering of summands.
module Data.Finitary.PolyRep (
  -- * Base Type and its algebra
  Poly, zeroPoly, addPoly, onePoly, multPoly, parPoly,

  -- ** Type-level @Poly@ algebra
  AddPoly, MultPoly, DayPoly,
  SPoly(..),
  sAddPoly, (%++), sMultPoly, sDayPoly,
  
  KnownPoly(..), withKnownPoly,
  
  -- * Evaluating @Poly@ as a Haskell 'Functor'
  Eval(..),

  -- ** Correspondence between sums, products, and Day convolution of @Poly@ and its evaluation
  absurdEval, unitEval,
  fromSum, inlEval, inrEval, toSum,
  fromProduct, toProduct,
  fromDay, toDay,

  -- ** Profunctor traversal
  ptraverseEval,

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

  -- * Internal-only type families
  (++), MultPoly1, DayPoly1
) where

import Data.Kind (Type)

import GHC.TypeNats
import GHC.TypeLits.Witnesses ( (%*), (%+) )
import Data.List.TypeLevel ( type (++) )

import Data.Finite
    ( Finite,
      combineProduct,
      combineSum,
      separateProduct,
      separateSum,
      separateZero, finites )

import Data.Void (absurd)
import Data.Profunctor (Profunctor(..))
import Data.Bifunctor (Bifunctor(..))
import Data.Profunctor.Cartesian
import Data.Type.Equality (TestEquality(..), type (:~:) (..))
import Data.Functor.Day
import Data.Functor.Classes

import Data.PTraversable.Internal.ClassOnly

-- | Finitary polynomial @f(x) = x^e1 + x^e2 + ... + x^en@
--   represented as a list of exponents @[e1, e2, ..., en]@
type Poly = [Nat]

zeroPoly :: Poly
zeroPoly :: Poly
zeroPoly = []

addPoly :: Poly -> Poly -> Poly
addPoly :: Poly -> Poly -> Poly
addPoly = Poly -> Poly -> Poly
forall a. [a] -> [a] -> [a]
(++)

onePoly :: Poly
onePoly :: Poly
onePoly = [Nat
0]

multPoly :: Poly -> Poly -> Poly
multPoly :: Poly -> Poly -> Poly
multPoly = (Nat -> Nat -> Nat) -> Poly -> Poly -> Poly
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
(+)

parPoly :: Poly
parPoly :: Poly
parPoly = [Nat
1]

type AddPoly :: Poly -> Poly -> Poly
type AddPoly r1 r2 = r1 ++ r2

type family MultPoly1 (e :: Nat) (r2 :: Poly) :: Poly where
  MultPoly1 _ '[] = '[]
  MultPoly1 e (f ': fs) = (e + f) : MultPoly1 e fs

type family MultPoly (r1 :: Poly) (r2 :: Poly) :: Poly where
  MultPoly '[] _ = '[]
  MultPoly (e ': es) r2 = AddPoly (MultPoly1 e r2) (MultPoly es r2)

type family DayPoly1 (e :: Nat) (r2 :: Poly) :: Poly where
  DayPoly1 _ '[] = '[]
  DayPoly1 e (f ': fs) = e * f : DayPoly1 e fs

type family DayPoly (r1 :: Poly) (r2 :: Poly) :: Poly where
  DayPoly '[] _ = '[]
  DayPoly (e ': es) r2 = AddPoly (DayPoly1 e r2) (DayPoly es r2)

data SPoly (r :: Poly) where
  SNil :: SPoly '[]
  SCons :: !(SNat e) -> !(SPoly es) -> SPoly (e ': es)

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

instance TestEquality SPoly where
  testEquality :: forall (a :: Poly) (b :: Poly).
SPoly a -> SPoly b -> Maybe (a :~: b)
testEquality SPoly a
SNil SPoly b
SNil = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality SPoly a
SNil SPoly b
_    = Maybe (a :~: b)
forall a. Maybe a
Nothing
  testEquality (SCons SNat e
se SPoly es
ses) (SCons SNat e
sf SPoly es
sfs) = do
    Refl <- SNat e -> SNat e -> Maybe (e :~: e)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SNat e
se SNat e
sf
    Refl <- testEquality ses sfs
    Just Refl
  testEquality SCons{} SPoly b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

sAddPoly, (%++) :: SPoly r1 -> SPoly r2 -> SPoly (AddPoly r1 r2)
sAddPoly :: forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (AddPoly r1 r2)
sAddPoly = SPoly r1 -> SPoly r2 -> SPoly (AddPoly r1 r2)
forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (AddPoly r1 r2)
(%++)
SPoly r1
SNil %++ :: forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (AddPoly r1 r2)
%++ SPoly r2
sr2 = SPoly r2
SPoly (r1 ++ r2)
sr2
SCons SNat e
se SPoly es
ses %++ SPoly r2
sr2 = SNat e -> SPoly (es ++ r2) -> SPoly (e : (es ++ r2))
forall (r :: Nat) (e :: Poly). SNat r -> SPoly e -> SPoly (r : e)
SCons SNat e
se (SPoly es
ses SPoly es -> SPoly r2 -> SPoly (es ++ r2)
forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (AddPoly r1 r2)
%++ SPoly r2
sr2)

sMultPoly1 :: SNat e -> SPoly r2 -> SPoly (MultPoly1 e r2)
sMultPoly1 :: forall (e :: Nat) (r2 :: Poly).
SNat e -> SPoly r2 -> SPoly (MultPoly1 e r2)
sMultPoly1 SNat e
_ SPoly r2
SNil = SPoly '[]
SPoly (MultPoly1 e r2)
SNil
sMultPoly1 SNat e
se (SCons SNat e
sf SPoly es
sfs) = SNat (e + e)
-> SPoly (MultPoly1 e es) -> SPoly ((e + e) : MultPoly1 e es)
forall (r :: Nat) (e :: Poly). SNat r -> SPoly e -> SPoly (r : e)
SCons (SNat e
se SNat e -> SNat e -> SNat (e + e)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat e
sf) (SNat e -> SPoly es -> SPoly (MultPoly1 e es)
forall (e :: Nat) (r2 :: Poly).
SNat e -> SPoly r2 -> SPoly (MultPoly1 e r2)
sMultPoly1 SNat e
se SPoly es
sfs)

sMultPoly :: SPoly r1 -> SPoly r2 -> SPoly (MultPoly r1 r2)
sMultPoly :: forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (MultPoly r1 r2)
sMultPoly SPoly r1
SNil SPoly r2
_ = SPoly '[]
SPoly (MultPoly r1 r2)
SNil
sMultPoly (SCons SNat e
se SPoly es
ses) SPoly r2
sr2 = SNat e -> SPoly r2 -> SPoly (MultPoly1 e r2)
forall (e :: Nat) (r2 :: Poly).
SNat e -> SPoly r2 -> SPoly (MultPoly1 e r2)
sMultPoly1 SNat e
se SPoly r2
sr2 SPoly (MultPoly1 e r2)
-> SPoly (MultPoly es r2)
-> SPoly (AddPoly (MultPoly1 e r2) (MultPoly es r2))
forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (AddPoly r1 r2)
%++ SPoly es -> SPoly r2 -> SPoly (MultPoly es r2)
forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (MultPoly r1 r2)
sMultPoly SPoly es
ses SPoly r2
sr2

sDayPoly1 :: SNat e -> SPoly r2 -> SPoly (DayPoly1 e r2)
sDayPoly1 :: forall (e :: Nat) (r2 :: Poly).
SNat e -> SPoly r2 -> SPoly (DayPoly1 e r2)
sDayPoly1 SNat e
_ SPoly r2
SNil = SPoly '[]
SPoly (DayPoly1 e r2)
SNil
sDayPoly1 SNat e
se (SCons SNat e
sf SPoly es
sfs) = SNat (e * e)
-> SPoly (DayPoly1 e es) -> SPoly ((e * e) : DayPoly1 e es)
forall (r :: Nat) (e :: Poly). SNat r -> SPoly e -> SPoly (r : e)
SCons (SNat e
se SNat e -> SNat e -> SNat (e * e)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n * m)
%* SNat e
sf) (SNat e -> SPoly es -> SPoly (DayPoly1 e es)
forall (e :: Nat) (r2 :: Poly).
SNat e -> SPoly r2 -> SPoly (DayPoly1 e r2)
sDayPoly1 SNat e
se SPoly es
sfs)

sDayPoly :: SPoly r1 -> SPoly r2 -> SPoly (DayPoly r1 r2)
sDayPoly :: forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (DayPoly r1 r2)
sDayPoly SPoly r1
SNil SPoly r2
_ = SPoly '[]
SPoly (DayPoly r1 r2)
SNil
sDayPoly (SCons SNat e
se SPoly es
ses) SPoly r2
sr2 = SNat e -> SPoly r2 -> SPoly (DayPoly1 e r2)
forall (e :: Nat) (r2 :: Poly).
SNat e -> SPoly r2 -> SPoly (DayPoly1 e r2)
sDayPoly1 SNat e
se SPoly r2
sr2 SPoly (DayPoly1 e r2)
-> SPoly (DayPoly es r2)
-> SPoly (AddPoly (DayPoly1 e r2) (DayPoly es r2))
forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (AddPoly r1 r2)
%++ SPoly es -> SPoly r2 -> SPoly (DayPoly es r2)
forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (DayPoly r1 r2)
sDayPoly SPoly es
ses SPoly r2
sr2

class KnownPoly (p :: Poly) where
  sPoly :: SPoly p

instance KnownPoly '[] where
  sPoly :: SPoly '[]
sPoly = SPoly '[]
SNil

instance (KnownNat e, KnownPoly es) => KnownPoly (e ': es) where
  sPoly :: SPoly (e : es)
sPoly = SNat e -> SPoly es -> SPoly (e : es)
forall (r :: Nat) (e :: Poly). SNat r -> SPoly e -> SPoly (r : e)
SCons SNat e
forall (n :: Nat). KnownNat n => SNat n
SNat SPoly es
forall (p :: Poly). KnownPoly p => SPoly p
sPoly

withKnownPoly :: SPoly r -> (KnownPoly r => result) -> result
withKnownPoly :: forall (r :: Poly) result.
SPoly r -> (KnownPoly r => result) -> result
withKnownPoly SPoly r
SNil KnownPoly r => result
body = result
KnownPoly r => result
body
withKnownPoly (SCons SNat e
se SPoly es
ses) KnownPoly r => result
body =
  SNat e -> (KnownNat e => result) -> result
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat e
se (SPoly es -> (KnownPoly es => result) -> result
forall (r :: Poly) result.
SPoly r -> (KnownPoly r => result) -> result
withKnownPoly SPoly es
ses result
KnownPoly r => result
KnownPoly es => result
body)

data Eval (r :: Poly) (x :: Type) where
  EHere :: !(Finite e -> x) -> Eval (e ': es) x
  EThere :: !(Eval es x) -> Eval (e ': es) x

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

unitEval :: Eval '[0] a
unitEval :: forall a. Eval '[0] a
unitEval = (Finite 0 -> a) -> Eval '[0] a
forall (r :: Nat) x (e :: Poly). (Finite r -> x) -> Eval (r : e) x
EHere Finite 0 -> a
forall b. Finite 0 -> b
absurdFinite

absurdFinite :: Finite 0 -> b
absurdFinite :: forall b. Finite 0 -> b
absurdFinite = Void -> b
forall a. Void -> a
absurd (Void -> b) -> (Finite 0 -> Void) -> Finite 0 -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite 0 -> Void
separateZero

deriving instance Functor (Eval r)

instance KnownPoly r => Foldable (Eval r) where
  foldMap :: forall m a. Monoid m => (a -> m) -> Eval r a -> m
foldMap = (a -> m) -> Eval r a -> m
forall (t :: Type -> Type) m a.
(PTraversable t, Monoid m) =>
(a -> m) -> t a -> m
foldMapDefault

instance KnownPoly r => Traversable (Eval r) where
  traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Eval r a -> f (Eval r b)
traverse = (a -> f b) -> Eval r a -> f (Eval r b)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(PTraversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverseDefault

instance KnownPoly r => PTraversable (Eval r) where
  ptraverseWith :: forall (p :: Type -> Type -> Type) 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 :: Type -> Type -> Type) 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
. SPoly r -> p a b -> p (Eval r a) (Eval r b)
forall (p :: Type -> Type -> Type) (r :: Poly) a b.
(Cartesian p, Cocartesian p) =>
SPoly r -> p a b -> p (Eval r a) (Eval r b)
ptraverseEval SPoly r
forall (p :: Poly). KnownPoly p => SPoly p
sPoly

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

instance (KnownPoly r) => Eq1 (Eval r) where
  liftEq :: forall a b. (a -> b -> Bool) -> Eval r a -> Eval r b -> Bool
liftEq a -> b -> Bool
eq = (a -> b -> Bool) -> SPoly r -> Eval r a -> Eval r b -> Bool
forall a b (r :: Poly).
(a -> b -> Bool) -> SPoly r -> Eval r a -> Eval r b -> Bool
liftEqEval a -> b -> Bool
eq SPoly r
forall (p :: Poly). KnownPoly p => SPoly p
sPoly

instance (KnownPoly r, 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 :: Type -> Type) a.
(Ord1 f, Ord a) =>
f a -> f a -> Ordering
compare1

instance (KnownPoly r) => Ord1 (Eval r) where
  liftCompare :: forall a b.
(a -> b -> Ordering) -> Eval r a -> Eval r b -> Ordering
liftCompare a -> b -> Ordering
cmp = (a -> b -> Ordering) -> SPoly r -> Eval r a -> Eval r b -> Ordering
forall a b (r :: Poly).
(a -> b -> Ordering) -> SPoly r -> Eval r a -> Eval r b -> Ordering
liftCompareEval a -> b -> Ordering
cmp SPoly r
forall (p :: Poly). KnownPoly p => SPoly p
sPoly

liftEqEval :: (a -> b -> Bool) -> SPoly r -> Eval r a -> Eval r b -> Bool
liftEqEval :: forall a b (r :: Poly).
(a -> b -> Bool) -> SPoly r -> Eval r a -> Eval r b -> Bool
liftEqEval a -> b -> Bool
_  SPoly r
SNil = Eval r a -> Eval r b -> Bool
Eval '[] a -> Eval r b -> Bool
forall a b. Eval '[] a -> b
absurdEval
liftEqEval a -> b -> Bool
eq (SCons SNat e
se SPoly es
ses) = \case
  EHere Finite e -> a
vec1 -> \case
    EHere Finite e -> b
vec2 -> SNat e -> (KnownNat e => Bool) -> Bool
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat e
se ((a -> b -> Bool) -> (Finite e -> a) -> (Finite e -> b) -> Bool
forall (n :: Nat) a b.
KnownNat n =>
(a -> b -> Bool) -> (Finite n -> a) -> (Finite n -> b) -> Bool
liftEqVec a -> b -> Bool
eq Finite e -> a
vec1 Finite e -> b
Finite e -> b
vec2)
    Eval r b
_ -> Bool
False
  EThere Eval es a
fa -> \case
    EThere Eval es b
fb -> (a -> b -> Bool) -> SPoly es -> Eval es a -> Eval es b -> Bool
forall a b (r :: Poly).
(a -> b -> Bool) -> SPoly r -> Eval r a -> Eval r b -> Bool
liftEqEval a -> b -> Bool
eq SPoly es
ses Eval es a
Eval es a
fa Eval es b
Eval es b
fb
    Eval r b
_ -> Bool
False

liftCompareEval :: (a -> b -> Ordering) -> SPoly r -> Eval r a -> Eval r b -> Ordering
liftCompareEval :: forall a b (r :: Poly).
(a -> b -> Ordering) -> SPoly r -> Eval r a -> Eval r b -> Ordering
liftCompareEval a -> b -> Ordering
_  SPoly r
SNil = Eval r a -> Eval r b -> Ordering
Eval '[] a -> Eval r b -> Ordering
forall a b. Eval '[] a -> b
absurdEval
liftCompareEval a -> b -> Ordering
cmp (SCons SNat e
se SPoly es
ses) = \case
  EHere Finite e -> a
vec1 -> \case
    EHere Finite e -> b
vec2 -> SNat e -> (KnownNat e => Ordering) -> Ordering
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat e
se ((a -> b -> Ordering)
-> (Finite e -> a) -> (Finite e -> b) -> Ordering
forall (n :: Nat) a b.
KnownNat n =>
(a -> b -> Ordering)
-> (Finite n -> a) -> (Finite n -> b) -> Ordering
liftCompareVec a -> b -> Ordering
cmp Finite e -> a
vec1 Finite e -> b
Finite e -> b
vec2)
    EThere Eval es b
_ -> Ordering
LT
  EThere Eval es a
fa -> \case
    EHere Finite e -> b
_ -> Ordering
GT
    EThere Eval es b
fb -> (a -> b -> Ordering)
-> SPoly es -> Eval es a -> Eval es b -> Ordering
forall a b (r :: Poly).
(a -> b -> Ordering) -> SPoly r -> Eval r a -> Eval r b -> Ordering
liftCompareEval a -> b -> Ordering
cmp SPoly es
ses Eval es a
Eval es a
fa Eval es b
Eval es b
fb

liftEqVec :: KnownNat n => (a -> b -> Bool) -> (Finite n -> a) -> (Finite n -> b) -> Bool
liftEqVec :: forall (n :: Nat) a b.
KnownNat n =>
(a -> b -> Bool) -> (Finite n -> a) -> (Finite n -> b) -> Bool
liftEqVec a -> b -> Bool
eq Finite n -> a
vec1 Finite n -> b
vec2 = (Finite n -> Bool) -> [Finite n] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all (\Finite n
i -> Finite n -> a
vec1 Finite n
i a -> b -> Bool
`eq` Finite n -> b
vec2 Finite n
i) [Finite n]
forall (n :: Nat). KnownNat n => [Finite n]
finites

liftCompareVec :: KnownNat n => (a -> b -> Ordering) -> (Finite n -> a) -> (Finite n -> b) -> Ordering
liftCompareVec :: forall (n :: Nat) a b.
KnownNat n =>
(a -> b -> Ordering)
-> (Finite n -> a) -> (Finite n -> b) -> Ordering
liftCompareVec a -> b -> Ordering
cmp Finite n -> a
vec1 Finite n -> b
vec2 = (Finite n -> Ordering -> Ordering)
-> Ordering -> [Finite n] -> Ordering
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Finite n
i Ordering
r -> a -> b -> Ordering
cmp (Finite n -> a
vec1 Finite n
i) (Finite n -> b
vec2 Finite n
i) Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Ordering
r) Ordering
EQ [Finite n]
forall (n :: Nat). KnownNat n => [Finite n]
finites

ptraverseEval :: (Cartesian p, Cocartesian p) => SPoly r -> p a b -> p (Eval r a) (Eval r b)
ptraverseEval :: forall (p :: Type -> Type -> Type) (r :: Poly) a b.
(Cartesian p, Cocartesian p) =>
SPoly r -> p a b -> p (Eval r a) (Eval r b)
ptraverseEval SPoly r
SNil p a b
_ = (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 :: Type -> Type -> Type) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap Eval r a -> Void
Eval '[] a -> Void
forall a b. Eval '[] a -> b
absurdEval p Void (Eval r b)
forall b. p Void b
forall (p :: Type -> Type -> Type) b. Cocartesian p => p Void b
proEmpty
ptraverseEval (SCons SNat e
SNat SPoly es
sr) p a b
p = (Eval r a -> Either (Finite e -> a) (Eval es a))
-> (Either (Finite e -> b) (Eval es b) -> Eval r b)
-> p (Either (Finite e -> a) (Eval es a))
     (Either (Finite e -> b) (Eval es 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 :: Type -> Type -> Type) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap Eval r a -> Either (Finite e -> a) (Eval es a)
Eval (e : es) a -> Either (Finite e -> a) (Eval es a)
forall (x :: Nat) (xs :: Poly) c.
Eval (x : xs) c -> Either (Finite x -> c) (Eval xs c)
splitEval Either (Finite e -> b) (Eval es b) -> Eval r b
Either (Finite e -> b) (Eval es b) -> Eval (e : es) b
forall (x :: Nat) (xs :: Poly) c.
Either (Finite x -> c) (Eval xs c) -> Eval (x : xs) c
mergeEval (p a b -> p (Finite e -> a) (Finite e -> b)
forall (n :: Nat) a b.
KnownNat n =>
p a b -> p (Finite n -> a) (Finite n -> b)
forall (p :: Type -> Type -> Type) (n :: Nat) a b.
(Cartesian p, KnownNat n) =>
p a b -> p (Finite n -> a) (Finite n -> b)
proPower p a b
p p (Finite e -> a) (Finite e -> b)
-> p (Eval es a) (Eval es b)
-> p (Either (Finite e -> a) (Eval es a))
     (Either (Finite e -> b) (Eval es b))
forall a b a' b'. p a b -> p a' b' -> p (Either a a') (Either b b')
forall (p :: Type -> Type -> Type) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ SPoly es -> p a b -> p (Eval es a) (Eval es b)
forall (p :: Type -> Type -> Type) (r :: Poly) a b.
(Cartesian p, Cocartesian p) =>
SPoly r -> p a b -> p (Eval r a) (Eval r b)
ptraverseEval SPoly es
sr p a b
p)
  where
    splitEval :: forall x xs c. Eval (x ': xs) c -> Either (Finite x -> c) (Eval xs c)
    splitEval :: forall (x :: Nat) (xs :: Poly) c.
Eval (x : xs) c -> Either (Finite x -> c) (Eval xs c)
splitEval (EHere Finite e -> c
vecX) = (Finite x -> c) -> Either (Finite x -> c) (Eval xs c)
forall a b. a -> Either a b
Left Finite x -> c
Finite e -> c
vecX
    splitEval (EThere Eval es c
fx) = Eval xs c -> Either (Finite x -> c) (Eval xs c)
forall a b. b -> Either a b
Right Eval xs c
Eval es c
fx

    mergeEval :: forall x xs c. Either (Finite x -> c) (Eval xs c) -> Eval (x ': xs) c
    mergeEval :: forall (x :: Nat) (xs :: Poly) c.
Either (Finite x -> c) (Eval xs c) -> Eval (x : xs) c
mergeEval = ((Finite x -> c) -> Eval (x : xs) c)
-> (Eval xs c -> Eval (x : xs) c)
-> Either (Finite x -> c) (Eval xs c)
-> Eval (x : xs) c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Finite x -> c) -> Eval (x : xs) c
forall (r :: Nat) x (e :: Poly). (Finite r -> x) -> Eval (r : e) x
EHere Eval xs c -> Eval (x : xs) c
forall (r :: Poly) x (e :: Nat). Eval r x -> Eval (e : r) x
EThere

-- ** Operators on @(p :: Poly)@ corresponds to those on @Eval p@

fromSum :: SPoly r1 -> proxy r2 -> Either (Eval r1 x) (Eval r2 x) -> Eval (r1 ++ r2) x
fromSum :: forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1
-> proxy r2 -> Either (Eval r1 x) (Eval r2 x) -> Eval (r1 ++ r2) x
fromSum SPoly r1
r1 proxy r2
r2 = (Eval r1 x -> Eval (r1 ++ r2) x)
-> (Eval r2 x -> Eval (r1 ++ r2) x)
-> Either (Eval r1 x) (Eval r2 x)
-> Eval (r1 ++ r2) x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (SPoly r1 -> proxy r2 -> Eval r1 x -> Eval (r1 ++ r2) x
forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1 -> proxy r2 -> Eval r1 x -> Eval (r1 ++ r2) x
inlEval SPoly r1
r1 proxy r2
r2) (SPoly r1 -> proxy r2 -> Eval r2 x -> Eval (r1 ++ r2) x
forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1 -> proxy r2 -> Eval r2 x -> Eval (r1 ++ r2) x
inrEval SPoly r1
r1 proxy r2
r2)

inlEval :: SPoly r1 -> proxy r2 -> Eval r1 x -> Eval (r1 ++ r2) x
inlEval :: forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1 -> proxy r2 -> Eval r1 x -> Eval (r1 ++ r2) x
inlEval SPoly r1
SNil proxy r2
_ Eval r1 x
fx = Eval '[] x -> Eval r2 x
forall a b. Eval '[] a -> b
absurdEval Eval r1 x
Eval '[] x
fx
inlEval (SCons SNat e
_ SPoly es
r1) proxy r2
r2 Eval r1 x
ex = case Eval r1 x
ex of
  EHere Finite e -> x
xvec -> (Finite e -> x) -> Eval (e : (es ++ r2)) x
forall (r :: Nat) x (e :: Poly). (Finite r -> x) -> Eval (r : e) x
EHere Finite e -> x
xvec
  EThere Eval es x
e1 -> Eval (es ++ r2) x -> Eval (e : (es ++ r2)) x
forall (r :: Poly) x (e :: Nat). Eval r x -> Eval (e : r) x
EThere (SPoly es -> proxy r2 -> Eval es x -> Eval (es ++ r2) x
forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1 -> proxy r2 -> Eval r1 x -> Eval (r1 ++ r2) x
inlEval SPoly es
r1 proxy r2
r2 Eval es x
Eval es x
e1)

inrEval :: SPoly r1 -> proxy r2 -> Eval r2 x -> Eval (r1 ++ r2) x
inrEval :: forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1 -> proxy r2 -> Eval r2 x -> Eval (r1 ++ r2) x
inrEval SPoly r1
SNil proxy r2
_ Eval r2 x
gx = Eval r2 x
Eval (r1 ++ r2) x
gx
inrEval (SCons SNat e
_ SPoly es
r1) proxy r2
r2 Eval r2 x
gx = Eval (es ++ r2) x -> Eval (e : (es ++ r2)) x
forall (r :: Poly) x (e :: Nat). Eval r x -> Eval (e : r) x
EThere (Eval (es ++ r2) x -> Eval (e : (es ++ r2)) x)
-> Eval (es ++ r2) x -> Eval (e : (es ++ r2)) x
forall a b. (a -> b) -> a -> b
$ SPoly es -> proxy r2 -> Eval r2 x -> Eval (es ++ r2) x
forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1 -> proxy r2 -> Eval r2 x -> Eval (r1 ++ r2) x
inrEval SPoly es
r1 proxy r2
r2 Eval r2 x
gx

toSum :: SPoly r1 -> proxy r2 -> Eval (r1 ++ r2) x -> Either (Eval r1 x) (Eval r2 x)
toSum :: forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1
-> proxy r2 -> Eval (r1 ++ r2) x -> Either (Eval r1 x) (Eval r2 x)
toSum SPoly r1
SNil proxy r2
_ Eval (r1 ++ r2) x
fx = Eval r2 x -> Either (Eval r1 x) (Eval r2 x)
forall a b. b -> Either a b
Right Eval r2 x
Eval (r1 ++ r2) x
fx
toSum (SCons SNat e
_ SPoly es
r1) proxy r2
r2 Eval (r1 ++ r2) x
fx = case Eval (r1 ++ r2) x
fx of
  EHere Finite e -> x
vecX -> Eval r1 x -> Either (Eval r1 x) (Eval r2 x)
forall a b. a -> Either a b
Left ((Finite e -> x) -> Eval (e : es) x
forall (r :: Nat) x (e :: Poly). (Finite r -> x) -> Eval (r : e) x
EHere Finite e -> x
vecX)
  EThere Eval es x
fx' -> (Eval es x -> Eval r1 x)
-> Either (Eval es 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 :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Eval es x -> Eval r1 x
Eval es x -> Eval (e : es) x
forall (r :: Poly) x (e :: Nat). Eval r x -> Eval (e : r) x
EThere (Either (Eval es x) (Eval r2 x) -> Either (Eval r1 x) (Eval r2 x))
-> Either (Eval es x) (Eval r2 x) -> Either (Eval r1 x) (Eval r2 x)
forall a b. (a -> b) -> a -> b
$ SPoly es
-> proxy r2 -> Eval (es ++ r2) x -> Either (Eval es x) (Eval r2 x)
forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1
-> proxy r2 -> Eval (r1 ++ r2) x -> Either (Eval r1 x) (Eval r2 x)
toSum SPoly es
r1 proxy r2
r2 Eval es x
Eval (es ++ r2) x
fx'

fromProduct :: SPoly r1 -> SPoly r2 -> Eval r1 x -> Eval r2 x -> Eval (MultPoly r1 r2) x
fromProduct :: forall (r1 :: Poly) (r2 :: Poly) x.
SPoly r1
-> SPoly r2 -> Eval r1 x -> Eval r2 x -> Eval (MultPoly r1 r2) x
fromProduct SPoly r1
SNil SPoly r2
_ Eval r1 x
fx Eval r2 x
_ = Eval '[] x -> Eval '[] x
forall a b. Eval '[] a -> b
absurdEval Eval r1 x
Eval '[] x
fx
fromProduct (SCons SNat e
se SPoly es
ses) SPoly r2
r2 Eval r1 x
fx Eval r2 x
gx = case Eval r1 x
fx of
  EHere Finite e -> x
vecX -> SPoly (MultPoly1 e r2)
-> SPoly (MultPoly es r2)
-> Eval (MultPoly1 e r2) x
-> Eval (MultPoly1 e r2 ++ MultPoly es r2) x
forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1 -> proxy r2 -> Eval r1 x -> Eval (r1 ++ r2) x
inlEval SPoly (MultPoly1 e r2)
pLeft SPoly (MultPoly es r2)
pRight (SNat e
-> SPoly r2
-> (Finite e -> x)
-> Eval r2 x
-> Eval (MultPoly1 e r2) x
forall (e :: Nat) (r2 :: Poly) x.
SNat e
-> SPoly r2
-> (Finite e -> x)
-> Eval r2 x
-> Eval (MultPoly1 e r2) x
fromProduct1 SNat e
se SPoly r2
r2 Finite e -> x
Finite e -> x
vecX Eval r2 x
gx)
  EThere Eval es x
fx' -> SPoly (MultPoly1 e r2)
-> SPoly (MultPoly es r2)
-> Eval (MultPoly es r2) x
-> Eval (MultPoly1 e r2 ++ MultPoly es r2) x
forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1 -> proxy r2 -> Eval r2 x -> Eval (r1 ++ r2) x
inrEval SPoly (MultPoly1 e r2)
pLeft SPoly (MultPoly es r2)
pRight (SPoly es
-> SPoly r2 -> Eval es x -> Eval r2 x -> Eval (MultPoly es r2) x
forall (r1 :: Poly) (r2 :: Poly) x.
SPoly r1
-> SPoly r2 -> Eval r1 x -> Eval r2 x -> Eval (MultPoly r1 r2) x
fromProduct SPoly es
ses SPoly r2
r2 Eval es x
Eval es x
fx' Eval r2 x
gx)
  where
    pLeft :: SPoly (MultPoly1 e r2)
pLeft  = SNat e -> SPoly r2 -> SPoly (MultPoly1 e r2)
forall (e :: Nat) (r2 :: Poly).
SNat e -> SPoly r2 -> SPoly (MultPoly1 e r2)
sMultPoly1 SNat e
se SPoly r2
r2
    pRight :: SPoly (MultPoly es r2)
pRight = SPoly es -> SPoly r2 -> SPoly (MultPoly es r2)
forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (MultPoly r1 r2)
sMultPoly SPoly es
ses SPoly r2
r2

fromProduct1 :: SNat e -> SPoly r2 -> (Finite e -> x) -> Eval r2 x -> Eval (MultPoly1 e r2) x
fromProduct1 :: forall (e :: Nat) (r2 :: Poly) x.
SNat e
-> SPoly r2
-> (Finite e -> x)
-> Eval r2 x
-> Eval (MultPoly1 e r2) x
fromProduct1 SNat e
_ SPoly r2
SNil Finite e -> x
_ Eval r2 x
gx = Eval '[] x -> Eval '[] x
forall a b. Eval '[] a -> b
absurdEval Eval r2 x
Eval '[] x
gx
fromProduct1 SNat e
se (SCons SNat e
sf SPoly es
sfs) Finite e -> x
vec1 Eval r2 x
gx = case Eval r2 x
gx of
  EHere Finite e -> x
vec2 -> (Finite (e + e) -> x) -> Eval ((e + e) : MultPoly1 e es) x
forall (r :: Nat) x (e :: Poly). (Finite r -> x) -> Eval (r : e) x
EHere (SNat e
-> SNat e
-> (Finite e -> x)
-> (Finite e -> x)
-> Finite (e + e)
-> x
forall (n :: Nat) (m :: Nat) x.
SNat n
-> SNat m
-> (Finite n -> x)
-> (Finite m -> x)
-> Finite (n + m)
-> x
appendVec SNat e
se SNat e
sf Finite e -> x
vec1 Finite e -> x
Finite e -> x
vec2)
  EThere Eval es x
gx' -> Eval (MultPoly1 e es) x -> Eval ((e + e) : MultPoly1 e es) x
forall (r :: Poly) x (e :: Nat). Eval r x -> Eval (e : r) x
EThere (Eval (MultPoly1 e es) x -> Eval ((e + e) : MultPoly1 e es) x)
-> Eval (MultPoly1 e es) x -> Eval ((e + e) : MultPoly1 e es) x
forall a b. (a -> b) -> a -> b
$ SNat e
-> SPoly es
-> (Finite e -> x)
-> Eval es x
-> Eval (MultPoly1 e es) x
forall (e :: Nat) (r2 :: Poly) x.
SNat e
-> SPoly r2
-> (Finite e -> x)
-> Eval r2 x
-> Eval (MultPoly1 e r2) x
fromProduct1 SNat e
se SPoly es
sfs Finite e -> x
vec1 Eval es x
Eval es x
gx'

toProduct :: SPoly r1 -> SPoly r2 -> Eval (MultPoly r1 r2) x -> (Eval r1 x, Eval r2 x)
toProduct :: forall (r1 :: Poly) (r2 :: Poly) x.
SPoly r1
-> SPoly r2 -> Eval (MultPoly r1 r2) x -> (Eval r1 x, Eval r2 x)
toProduct SPoly r1
SNil SPoly r2
_ Eval (MultPoly r1 r2) x
e = Eval '[] x -> (Eval r1 x, Eval r2 x)
forall a b. Eval '[] a -> b
absurdEval Eval '[] x
Eval (MultPoly r1 r2) x
e
toProduct (SCons SNat e
se SPoly es
ses) SPoly r2
r2 Eval (MultPoly r1 r2) x
e = case SPoly (MultPoly1 e r2)
-> SPoly (MultPoly es r2)
-> Eval (MultPoly1 e r2 ++ MultPoly es r2) x
-> Either (Eval (MultPoly1 e r2) x) (Eval (MultPoly es r2) x)
forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1
-> proxy r2 -> Eval (r1 ++ r2) x -> Either (Eval r1 x) (Eval r2 x)
toSum SPoly (MultPoly1 e r2)
pLeft SPoly (MultPoly es r2)
pRight Eval (MultPoly1 e r2 ++ MultPoly es r2) x
Eval (MultPoly r1 r2) x
e of
  Left Eval (MultPoly1 e r2) x
e1 -> ((Finite e -> x) -> Eval r1 x)
-> (Finite e -> x, Eval r2 x) -> (Eval r1 x, Eval r2 x)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Finite e -> x) -> Eval r1 x
(Finite e -> x) -> Eval (e : es) x
forall (r :: Nat) x (e :: Poly). (Finite r -> x) -> Eval (r : e) x
EHere ((Finite e -> x, Eval r2 x) -> (Eval r1 x, Eval r2 x))
-> (Finite e -> x, Eval r2 x) -> (Eval r1 x, Eval r2 x)
forall a b. (a -> b) -> a -> b
$ SNat e
-> SPoly r2
-> Eval (MultPoly1 e r2) x
-> (Finite e -> x, Eval r2 x)
forall (e :: Nat) (r2 :: Poly) x.
SNat e
-> SPoly r2
-> Eval (MultPoly1 e r2) x
-> (Finite e -> x, Eval r2 x)
toProduct1 SNat e
se SPoly r2
r2 Eval (MultPoly1 e r2) x
e1
  Right Eval (MultPoly es r2) x
e2 -> (Eval es x -> Eval r1 x)
-> (Eval es x, Eval r2 x) -> (Eval r1 x, Eval r2 x)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Eval es x -> Eval r1 x
Eval es x -> Eval (e : es) x
forall (r :: Poly) x (e :: Nat). Eval r x -> Eval (e : r) x
EThere ((Eval es x, Eval r2 x) -> (Eval r1 x, Eval r2 x))
-> (Eval es x, Eval r2 x) -> (Eval r1 x, Eval r2 x)
forall a b. (a -> b) -> a -> b
$ SPoly es
-> SPoly r2 -> Eval (MultPoly es r2) x -> (Eval es x, Eval r2 x)
forall (r1 :: Poly) (r2 :: Poly) x.
SPoly r1
-> SPoly r2 -> Eval (MultPoly r1 r2) x -> (Eval r1 x, Eval r2 x)
toProduct SPoly es
ses SPoly r2
r2 Eval (MultPoly es r2) x
e2
  where
    pLeft :: SPoly (MultPoly1 e r2)
pLeft  = SNat e -> SPoly r2 -> SPoly (MultPoly1 e r2)
forall (e :: Nat) (r2 :: Poly).
SNat e -> SPoly r2 -> SPoly (MultPoly1 e r2)
sMultPoly1 SNat e
se SPoly r2
r2
    pRight :: SPoly (MultPoly es r2)
pRight = SPoly es -> SPoly r2 -> SPoly (MultPoly es r2)
forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (MultPoly r1 r2)
sMultPoly SPoly es
ses SPoly r2
r2

toProduct1 :: SNat e -> SPoly r2 -> Eval (MultPoly1 e r2) x -> (Finite e -> x, Eval r2 x)
toProduct1 :: forall (e :: Nat) (r2 :: Poly) x.
SNat e
-> SPoly r2
-> Eval (MultPoly1 e r2) x
-> (Finite e -> x, Eval r2 x)
toProduct1 SNat e
_ SPoly r2
SNil Eval (MultPoly1 e r2) x
fx = Eval '[] x -> (Finite e -> x, Eval r2 x)
forall a b. Eval '[] a -> b
absurdEval Eval '[] x
Eval (MultPoly1 e r2) x
fx
toProduct1 SNat e
se (SCons SNat e
sf SPoly es
sfs) Eval (MultPoly1 e r2) x
fx = case Eval (MultPoly1 e r2) x
fx of
  EHere Finite e -> x
vecX -> ((Finite e -> x) -> Eval r2 x)
-> (Finite e -> x, Finite e -> x) -> (Finite e -> x, Eval r2 x)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Finite e -> x) -> Eval r2 x
(Finite e -> x) -> Eval (e : es) x
forall (r :: Nat) x (e :: Poly). (Finite r -> x) -> Eval (r : e) x
EHere ((Finite e -> x, Finite e -> x) -> (Finite e -> x, Eval r2 x))
-> (Finite e -> x, Finite e -> x) -> (Finite e -> x, Eval r2 x)
forall a b. (a -> b) -> a -> b
$ SNat e
-> SNat e
-> (Finite (e + e) -> x)
-> (Finite e -> x, Finite e -> x)
forall (n :: Nat) (m :: Nat) x.
SNat n
-> SNat m
-> (Finite (n + m) -> x)
-> (Finite n -> x, Finite m -> x)
splitVec SNat e
se SNat e
sf Finite e -> x
Finite (e + e) -> x
vecX
  EThere Eval es x
fx'  -> (Eval es x -> Eval r2 x)
-> (Finite e -> x, Eval es x) -> (Finite e -> x, Eval r2 x)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Eval es x -> Eval r2 x
Eval es x -> Eval (e : es) x
forall (r :: Poly) x (e :: Nat). Eval r x -> Eval (e : r) x
EThere ((Finite e -> x, Eval es x) -> (Finite e -> x, Eval r2 x))
-> (Finite e -> x, Eval es x) -> (Finite e -> x, Eval r2 x)
forall a b. (a -> b) -> a -> b
$ SNat e
-> SPoly es
-> Eval (MultPoly1 e es) x
-> (Finite e -> x, Eval es x)
forall (e :: Nat) (r2 :: Poly) x.
SNat e
-> SPoly r2
-> Eval (MultPoly1 e r2) x
-> (Finite e -> x, Eval r2 x)
toProduct1 SNat e
se SPoly es
sfs Eval es x
Eval (MultPoly1 e es) x
fx'

appendVec :: SNat n -> SNat m -> (Finite n -> x) -> (Finite m -> x) -> Finite (n + m) -> x
appendVec :: forall (n :: Nat) (m :: Nat) x.
SNat n
-> SNat m
-> (Finite n -> x)
-> (Finite m -> x)
-> Finite (n + m)
-> x
appendVec SNat n
SNat SNat m
_ Finite n -> x
vec1 Finite m -> x
vec2 = (Finite n -> x)
-> (Finite m -> x) -> Either (Finite n) (Finite m) -> x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Finite n -> x
vec1 Finite m -> x
vec2 (Either (Finite n) (Finite m) -> x)
-> (Finite (n + m) -> Either (Finite n) (Finite m))
-> Finite (n + m)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (n + m) -> Either (Finite n) (Finite m)
forall (n :: Nat) (m :: Nat).
KnownNat n =>
Finite (n + m) -> Either (Finite n) (Finite m)
separateSum

splitVec :: SNat n -> SNat m -> (Finite (n + m) -> x) -> (Finite n -> x, Finite m -> x)
splitVec :: forall (n :: Nat) (m :: Nat) x.
SNat n
-> SNat m
-> (Finite (n + m) -> x)
-> (Finite n -> x, Finite m -> x)
splitVec SNat n
SNat SNat m
_ Finite (n + m) -> x
vec =
  let vec' :: Either (Finite n) (Finite m) -> x
vec' = Finite (n + m) -> x
vec (Finite (n + m) -> x)
-> (Either (Finite n) (Finite m) -> Finite (n + m))
-> Either (Finite n) (Finite m)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either (Finite n) (Finite m) -> Finite (n + m)
forall (n :: Nat) (m :: Nat).
KnownNat n =>
Either (Finite n) (Finite m) -> Finite (n + m)
combineSum
  in (Either (Finite n) (Finite m) -> x
vec' (Either (Finite n) (Finite m) -> x)
-> (Finite n -> Either (Finite n) (Finite m)) -> Finite n -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> Either (Finite n) (Finite m)
forall a b. a -> Either a b
Left, Either (Finite n) (Finite m) -> x
vec' (Either (Finite n) (Finite m) -> x)
-> (Finite m -> Either (Finite n) (Finite m)) -> Finite m -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite m -> Either (Finite n) (Finite m)
forall a b. b -> Either a b
Right)

flatVec :: SNat n -> SNat m -> (Finite n -> Finite m -> x) -> Finite (n * m) -> x
flatVec :: forall (n :: Nat) (m :: Nat) x.
SNat n
-> SNat m -> (Finite n -> Finite m -> x) -> Finite (n * m) -> x
flatVec SNat n
SNat SNat m
_ Finite n -> Finite m -> x
vecXY = (Finite n -> Finite m -> x) -> (Finite n, Finite m) -> x
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Finite n -> Finite m -> x
vecXY ((Finite n, Finite m) -> x)
-> (Finite (n * m) -> (Finite n, Finite m)) -> Finite (n * m) -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (n * m) -> (Finite n, Finite m)
forall (n :: Nat) (m :: Nat).
KnownNat n =>
Finite (n * m) -> (Finite n, Finite m)
separateProduct

matVec :: SNat n -> SNat m -> (Finite (n * m) -> x) -> Finite n -> Finite m -> x
matVec :: forall (n :: Nat) (m :: Nat) x.
SNat n
-> SNat m -> (Finite (n * m) -> x) -> Finite n -> Finite m -> x
matVec SNat n
SNat SNat m
_ Finite (n * m) -> x
vec = ((Finite n, Finite m) -> x) -> Finite n -> Finite m -> x
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Finite (n * m) -> x
vec (Finite (n * m) -> x)
-> ((Finite n, Finite m) -> Finite (n * m))
-> (Finite n, Finite m)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Finite n, Finite m) -> Finite (n * m)
forall (n :: Nat) (m :: Nat).
KnownNat n =>
(Finite n, Finite m) -> Finite (n * m)
combineProduct)

fromDay :: SPoly r1 -> SPoly r2 -> Day (Eval r1) (Eval r2) x -> Eval (DayPoly r1 r2) x
fromDay :: forall (r1 :: Poly) (r2 :: Poly) x.
SPoly r1
-> SPoly r2 -> Day (Eval r1) (Eval r2) x -> Eval (DayPoly r1 r2) x
fromDay SPoly r1
SNil SPoly r2
_ (Day Eval r1 b
fx Eval r2 c
_ b -> c -> x
_) = Eval '[] b -> Eval '[] x
forall a b. Eval '[] a -> b
absurdEval Eval r1 b
Eval '[] b
fx
fromDay (SCons SNat e
se SPoly es
ses) SPoly r2
r2 (Day Eval r1 b
fx Eval r2 c
gy b -> c -> x
op) = case Eval r1 b
fx of
  EHere Finite e -> b
vecX -> SPoly (DayPoly1 e r2)
-> SPoly (DayPoly es r2)
-> Eval (DayPoly1 e r2) x
-> Eval (DayPoly1 e r2 ++ DayPoly es r2) x
forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1 -> proxy r2 -> Eval r1 x -> Eval (r1 ++ r2) x
inlEval SPoly (DayPoly1 e r2)
pLeft SPoly (DayPoly es r2)
pRight (Eval (DayPoly1 e r2) x -> Eval (DayPoly1 e r2 ++ DayPoly es r2) x)
-> Eval (DayPoly1 e r2) x
-> Eval (DayPoly1 e r2 ++ DayPoly es r2) x
forall a b. (a -> b) -> a -> b
$ SNat e
-> SPoly r2
-> (Finite e -> b)
-> Eval r2 c
-> (b -> c -> x)
-> Eval (DayPoly1 e r2) x
forall (e :: Nat) (r2 :: Poly) x y z.
SNat e
-> SPoly r2
-> (Finite e -> x)
-> Eval r2 y
-> (x -> y -> z)
-> Eval (DayPoly1 e r2) z
fromDay1 SNat e
se SPoly r2
r2 Finite e -> b
Finite e -> b
vecX Eval r2 c
gy b -> c -> x
op
  EThere Eval es b
fx' -> SPoly (DayPoly1 e r2)
-> SPoly (DayPoly es r2)
-> Eval (DayPoly es r2) x
-> Eval (DayPoly1 e r2 ++ DayPoly es r2) x
forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1 -> proxy r2 -> Eval r2 x -> Eval (r1 ++ r2) x
inrEval SPoly (DayPoly1 e r2)
pLeft SPoly (DayPoly es r2)
pRight (Eval (DayPoly es r2) x -> Eval (DayPoly1 e r2 ++ DayPoly es r2) x)
-> Eval (DayPoly es r2) x
-> Eval (DayPoly1 e r2 ++ DayPoly es r2) x
forall a b. (a -> b) -> a -> b
$ SPoly es
-> SPoly r2 -> Day (Eval es) (Eval r2) x -> Eval (DayPoly es r2) x
forall (r1 :: Poly) (r2 :: Poly) x.
SPoly r1
-> SPoly r2 -> Day (Eval r1) (Eval r2) x -> Eval (DayPoly r1 r2) x
fromDay SPoly es
ses SPoly r2
r2 (Eval es b
-> Eval r2 c -> (b -> c -> x) -> Day (Eval es) (Eval r2) x
forall (f :: Type -> Type) (g :: Type -> Type) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day Eval es b
Eval es b
fx' Eval r2 c
gy b -> c -> x
op)
  where
    pLeft :: SPoly (DayPoly1 e r2)
pLeft  = SNat e -> SPoly r2 -> SPoly (DayPoly1 e r2)
forall (e :: Nat) (r2 :: Poly).
SNat e -> SPoly r2 -> SPoly (DayPoly1 e r2)
sDayPoly1 SNat e
se SPoly r2
r2
    pRight :: SPoly (DayPoly es r2)
pRight = SPoly es -> SPoly r2 -> SPoly (DayPoly es r2)
forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (DayPoly r1 r2)
sDayPoly SPoly es
ses SPoly r2
r2

fromDay1 :: SNat e -> SPoly r2 -> (Finite e -> x) -> Eval r2 y -> (x -> y -> z) -> Eval (DayPoly1 e r2) z
fromDay1 :: forall (e :: Nat) (r2 :: Poly) x y z.
SNat e
-> SPoly r2
-> (Finite e -> x)
-> Eval r2 y
-> (x -> y -> z)
-> Eval (DayPoly1 e r2) z
fromDay1 SNat e
se SPoly r2
r2 Finite e -> x
vecX Eval r2 y
gy x -> y -> z
op = case SPoly r2
r2 of
  SPoly r2
SNil -> Eval '[] y -> Eval '[] z
forall a b. Eval '[] a -> b
absurdEval Eval r2 y
Eval '[] y
gy
  SCons SNat e
sf SPoly es
sfs -> case Eval r2 y
gy of
    EHere Finite e -> y
vecY -> (Finite (e * e) -> z) -> Eval ((e * e) : DayPoly1 e es) z
forall (r :: Nat) x (e :: Poly). (Finite r -> x) -> Eval (r : e) x
EHere ((Finite (e * e) -> z) -> Eval ((e * e) : DayPoly1 e es) z)
-> (Finite (e * e) -> z) -> Eval ((e * e) : DayPoly1 e es) z
forall a b. (a -> b) -> a -> b
$ SNat e
-> SNat e -> (Finite e -> Finite e -> z) -> Finite (e * e) -> z
forall (n :: Nat) (m :: Nat) x.
SNat n
-> SNat m -> (Finite n -> Finite m -> x) -> Finite (n * m) -> x
flatVec SNat e
se SNat e
sf (\Finite e
i Finite e
j -> x -> y -> z
op (Finite e -> x
vecX Finite e
i) (Finite e -> y
vecY Finite e
Finite e
j))
    EThere Eval es y
gy' -> Eval (DayPoly1 e es) z -> Eval ((e * e) : DayPoly1 e es) z
forall (r :: Poly) x (e :: Nat). Eval r x -> Eval (e : r) x
EThere (Eval (DayPoly1 e es) z -> Eval ((e * e) : DayPoly1 e es) z)
-> Eval (DayPoly1 e es) z -> Eval ((e * e) : DayPoly1 e es) z
forall a b. (a -> b) -> a -> b
$ SNat e
-> SPoly es
-> (Finite e -> x)
-> Eval es y
-> (x -> y -> z)
-> Eval (DayPoly1 e es) z
forall (e :: Nat) (r2 :: Poly) x y z.
SNat e
-> SPoly r2
-> (Finite e -> x)
-> Eval r2 y
-> (x -> y -> z)
-> Eval (DayPoly1 e r2) z
fromDay1 SNat e
se SPoly es
sfs Finite e -> x
vecX Eval es y
Eval es y
gy' x -> y -> z
op

toDay :: SPoly r1 -> SPoly r2 -> Eval (DayPoly r1 r2) x -> Day (Eval r1) (Eval r2) x
toDay :: forall (r1 :: Poly) (r2 :: Poly) x.
SPoly r1
-> SPoly r2 -> Eval (DayPoly r1 r2) x -> Day (Eval r1) (Eval r2) x
toDay SPoly r1
SNil SPoly r2
_ Eval (DayPoly r1 r2) x
fx = Eval '[] x -> Day (Eval r1) (Eval r2) x
forall a b. Eval '[] a -> b
absurdEval Eval '[] x
Eval (DayPoly r1 r2) x
fx
toDay (SCons SNat e
se SPoly es
ses) SPoly r2
r2 Eval (DayPoly r1 r2) x
fx = case SPoly (DayPoly1 e r2)
-> SPoly (DayPoly es r2)
-> Eval (DayPoly1 e r2 ++ DayPoly es r2) x
-> Either (Eval (DayPoly1 e r2) x) (Eval (DayPoly es r2) x)
forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1
-> proxy r2 -> Eval (r1 ++ r2) x -> Either (Eval r1 x) (Eval r2 x)
toSum (SNat e -> SPoly r2 -> SPoly (DayPoly1 e r2)
forall (e :: Nat) (r2 :: Poly).
SNat e -> SPoly r2 -> SPoly (DayPoly1 e r2)
sDayPoly1 SNat e
se SPoly r2
r2) (SPoly es -> SPoly r2 -> SPoly (DayPoly es r2)
forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (DayPoly r1 r2)
sDayPoly SPoly es
ses SPoly r2
r2) Eval (DayPoly1 e r2 ++ DayPoly es r2) x
Eval (DayPoly r1 r2) x
fx of
  Left Eval (DayPoly1 e r2) x
fx' -> (forall x. (Finite e -> x) -> Eval r1 x)
-> Day ((->) (Finite e)) (Eval r2) x -> Day (Eval r1) (Eval r2) x
forall (f :: Type -> Type) (g :: Type -> Type) (h :: Type -> Type)
       a.
(forall x. f x -> g x) -> Day f h a -> Day g h a
trans1 (Finite e -> x) -> Eval r1 x
(Finite e -> x) -> Eval (e : es) x
forall (r :: Nat) x (e :: Poly). (Finite r -> x) -> Eval (r : e) x
forall x. (Finite e -> x) -> Eval r1 x
EHere (Day ((->) (Finite e)) (Eval r2) x -> Day (Eval r1) (Eval r2) x)
-> Day ((->) (Finite e)) (Eval r2) x -> Day (Eval r1) (Eval r2) x
forall a b. (a -> b) -> a -> b
$ SNat e
-> SPoly r2
-> Eval (DayPoly1 e r2) x
-> Day ((->) (Finite e)) (Eval r2) x
forall (e :: Nat) (r2 :: Poly) x.
SNat e
-> SPoly r2
-> Eval (DayPoly1 e r2) x
-> Day ((->) (Finite e)) (Eval r2) x
toDay1 SNat e
se SPoly r2
r2 Eval (DayPoly1 e r2) x
fx'
  Right Eval (DayPoly es r2) x
fx' -> (forall x. Eval es x -> Eval r1 x)
-> Day (Eval es) (Eval r2) x -> Day (Eval r1) (Eval r2) x
forall (f :: Type -> Type) (g :: Type -> Type) (h :: Type -> Type)
       a.
(forall x. f x -> g x) -> Day f h a -> Day g h a
trans1 Eval es x -> Eval r1 x
Eval es x -> Eval (e : es) x
forall (r :: Poly) x (e :: Nat). Eval r x -> Eval (e : r) x
forall x. Eval es x -> Eval r1 x
EThere (Day (Eval es) (Eval r2) x -> Day (Eval r1) (Eval r2) x)
-> Day (Eval es) (Eval r2) x -> Day (Eval r1) (Eval r2) x
forall a b. (a -> b) -> a -> b
$ SPoly es
-> SPoly r2 -> Eval (DayPoly es r2) x -> Day (Eval es) (Eval r2) x
forall (r1 :: Poly) (r2 :: Poly) x.
SPoly r1
-> SPoly r2 -> Eval (DayPoly r1 r2) x -> Day (Eval r1) (Eval r2) x
toDay SPoly es
ses SPoly r2
r2 Eval (DayPoly es r2) x
fx'

toDay1 :: SNat e -> SPoly r2 -> Eval (DayPoly1 e r2) x -> Day ((->) (Finite e)) (Eval r2) x
toDay1 :: forall (e :: Nat) (r2 :: Poly) x.
SNat e
-> SPoly r2
-> Eval (DayPoly1 e r2) x
-> Day ((->) (Finite e)) (Eval r2) x
toDay1 SNat e
_ SPoly r2
SNil Eval (DayPoly1 e r2) x
fx = Eval '[] x -> Day ((->) (Finite e)) (Eval r2) x
forall a b. Eval '[] a -> b
absurdEval Eval '[] x
Eval (DayPoly1 e r2) x
fx
toDay1 SNat e
se (SCons SNat e
sf SPoly es
sfs) Eval (DayPoly1 e r2) x
fx = case Eval (DayPoly1 e r2) x
fx of
  EHere Finite e -> x
vec -> (Finite e -> Finite e)
-> Eval r2 (Finite e)
-> (Finite e -> Finite e -> x)
-> Day ((->) (Finite e)) (Eval r2) x
forall (f :: Type -> Type) (g :: Type -> Type) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day Finite e -> Finite e
forall a. a -> a
id ((Finite e -> Finite e) -> Eval (e : es) (Finite e)
forall (r :: Nat) x (e :: Poly). (Finite r -> x) -> Eval (r : e) x
EHere Finite e -> Finite e
forall a. a -> a
id) (SNat e
-> SNat e -> (Finite (e * e) -> x) -> Finite e -> Finite e -> x
forall (n :: Nat) (m :: Nat) x.
SNat n
-> SNat m -> (Finite (n * m) -> x) -> Finite n -> Finite m -> x
matVec SNat e
se SNat e
sf Finite e -> x
Finite (e * e) -> x
vec)
  EThere Eval es x
fx' -> (forall x. Eval es x -> Eval r2 x)
-> Day ((->) (Finite e)) (Eval es) x
-> Day ((->) (Finite e)) (Eval r2) x
forall (g :: Type -> Type) (h :: Type -> Type) (f :: Type -> Type)
       a.
(forall x. g x -> h x) -> Day f g a -> Day f h a
trans2 Eval es x -> Eval r2 x
Eval es x -> Eval (e : es) x
forall (r :: Poly) x (e :: Nat). Eval r x -> Eval (e : r) x
forall x. Eval es x -> Eval r2 x
EThere (Day ((->) (Finite e)) (Eval es) x
 -> Day ((->) (Finite e)) (Eval r2) x)
-> Day ((->) (Finite e)) (Eval es) x
-> Day ((->) (Finite e)) (Eval r2) x
forall a b. (a -> b) -> a -> b
$ SNat e
-> SPoly es
-> Eval (DayPoly1 e es) x
-> Day ((->) (Finite e)) (Eval es) x
forall (e :: Nat) (r2 :: Poly) x.
SNat e
-> SPoly r2
-> Eval (DayPoly1 e r2) x
-> Day ((->) (Finite e)) (Eval r2) x
toDay1 SNat e
se SPoly es
sfs Eval es x
Eval (DayPoly1 e es) x
fx'

data Encoder a b s t where
  Encoder :: !(SPoly 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 'Data.PTraversable.PTraversable'
--   functor using
--
--   @
--   'Data.PTraversable.ptraverse' 'idEncoder' :: PTraversable t => Encoder a b (t a) (t b)
--   @
--
--   .
idEncoder :: Encoder a b a b
idEncoder :: forall a b. Encoder a b a b
idEncoder = SPoly '[1]
-> (a -> Eval '[1] a) -> (Eval '[1] b -> b) -> Encoder a b a b
forall (r :: Poly) s a b t.
SPoly r -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t
Encoder SPoly '[1]
forall (p :: Poly). KnownPoly p => SPoly p
sPoly a -> Eval '[1] a
forall c. c -> Eval '[1] c
idEnc Eval '[1] b -> b
forall c. Eval '[1] c -> c
idDec
  where
    idEnc :: c -> Eval '[1] c
    idEnc :: forall c. c -> Eval '[1] c
idEnc c
c = (Finite 1 -> c) -> Eval '[1] c
forall (r :: Nat) x (e :: Poly). (Finite r -> x) -> Eval (r : e) x
EHere (c -> Finite 1 -> c
forall a b. a -> b -> a
const c
c)
    
    idDec :: Eval '[1] c -> c
    idDec :: forall c. Eval '[1] c -> c
idDec (EHere Finite e -> c
v) = Finite e -> c
v Finite e
forall a. Bounded a => a
minBound
    -- @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 SPoly r
rep b -> Eval r a
enc Eval r b -> c
dec) = SPoly r -> (a -> Eval r a) -> (Eval r b -> d) -> Encoder a b a d
forall (r :: Poly) s a b t.
SPoly r -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t
Encoder SPoly 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 SPoly r
rep b -> Eval r a
enc Eval r b -> c
dec) = SPoly r -> (a -> Eval r a) -> (Eval r b -> c) -> Encoder a b a c
forall (r :: Poly) s a b t.
SPoly r -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t
Encoder SPoly 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 :: Type -> Type) 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 = SPoly '[0]
-> (a -> Eval '[0] a) -> (Eval '[0] b -> ()) -> Encoder a b a ()
forall (r :: Poly) s a b t.
SPoly r -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t
Encoder (SNat 0 -> SPoly '[] -> SPoly '[0]
forall (r :: Nat) (e :: Poly). SNat r -> SPoly e -> SPoly (r : e)
SCons (forall (n :: Nat). KnownNat n => SNat n
SNat @0) SPoly '[]
SNil) (Eval '[0] a -> a -> Eval '[0] a
forall a b. a -> b -> a
const Eval '[0] a
forall a. Eval '[0] a
unitEval) (() -> Eval '[0] b -> ()
forall a b. a -> b -> a
const ())
  (Encoder SPoly 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 SPoly r
r2 a' -> Eval r a
enc2 Eval r b -> b'
dec2) =
    let enc :: (a, a') -> Eval (MultPoly r r) a
enc (a
s1, a'
s2) = SPoly r -> SPoly r -> Eval r a -> Eval r a -> Eval (MultPoly r r) a
forall (r1 :: Poly) (r2 :: Poly) x.
SPoly r1
-> SPoly r2 -> Eval r1 x -> Eval r2 x -> Eval (MultPoly r1 r2) x
fromProduct SPoly r
r1 SPoly r
r2 (a -> Eval r a
enc1 a
s1) (a' -> Eval r a
enc2 a'
s2)
        dec :: Eval (MultPoly 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 :: Type -> Type -> Type) 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 (MultPoly r r) b -> (Eval r b, Eval r b))
-> Eval (MultPoly r r) b
-> (b, b')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPoly r -> SPoly r -> Eval (MultPoly r r) b -> (Eval r b, Eval r b)
forall (r1 :: Poly) (r2 :: Poly) x.
SPoly r1
-> SPoly r2 -> Eval (MultPoly r1 r2) x -> (Eval r1 x, Eval r2 x)
toProduct SPoly r
r1 SPoly r
r2
    in SPoly (MultPoly r r)
-> ((a, a') -> Eval (MultPoly r r) a)
-> (Eval (MultPoly r r) b -> (b, b'))
-> Encoder a b (a, a') (b, b')
forall (r :: Poly) s a b t.
SPoly r -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t
Encoder (SPoly r -> SPoly r -> SPoly (MultPoly r r)
forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (MultPoly r1 r2)
sMultPoly SPoly r
r1 SPoly r
r2) (a, a') -> Eval (MultPoly r r) a
enc Eval (MultPoly r r) b -> (b, b')
dec

instance Cocartesian (Encoder a b) where
  proEmpty :: forall b. Encoder a b Void b
proEmpty = SPoly '[]
-> (Void -> Eval '[] a) -> (Eval '[] b -> b) -> Encoder a b Void b
forall (r :: Poly) s a b t.
SPoly r -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t
Encoder SPoly '[]
SNil Void -> Eval '[] a
forall a. Void -> a
absurd Eval '[] b -> b
forall a b. Eval '[] a -> b
absurdEval
  (Encoder SPoly 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 SPoly r
r2 a' -> Eval r a
enc2 Eval r b -> b'
dec2) =
    let enc :: Either a a' -> Eval (r ++ r) a
enc = (a -> Eval (r ++ r) a)
-> (a' -> Eval (r ++ r) a) -> Either a a' -> Eval (r ++ r) a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (SPoly r -> SPoly r -> Eval r a -> Eval (r ++ r) a
forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1 -> proxy r2 -> Eval r1 x -> Eval (r1 ++ r2) x
inlEval SPoly r
r1 SPoly r
r2 (Eval r a -> Eval (r ++ r) a)
-> (a -> Eval r a) -> a -> Eval (r ++ r) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eval r a
enc1) (SPoly r -> SPoly r -> Eval r a -> Eval (r ++ r) a
forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1 -> proxy r2 -> Eval r2 x -> Eval (r1 ++ r2) x
inrEval SPoly r
r1 SPoly r
r2 (Eval r a -> Eval (r ++ r) a)
-> (a' -> Eval r a) -> a' -> Eval (r ++ r) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a' -> Eval r a
enc2)
        dec :: Eval (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 :: Type -> Type -> Type) 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 (r ++ r) b -> Either (Eval r b) (Eval r b))
-> Eval (r ++ r) b
-> Either b b'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPoly r
-> SPoly r -> Eval (r ++ r) b -> Either (Eval r b) (Eval r b)
forall (r1 :: Poly) (proxy :: Poly -> Type) (r2 :: Poly) x.
SPoly r1
-> proxy r2 -> Eval (r1 ++ r2) x -> Either (Eval r1 x) (Eval r2 x)
toSum SPoly r
r1 SPoly r
r2
    in SPoly (r ++ r)
-> (Either a a' -> Eval (r ++ r) a)
-> (Eval (r ++ r) b -> Either b b')
-> Encoder a b (Either a a') (Either b b')
forall (r :: Poly) s a b t.
SPoly r -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t
Encoder (SPoly r
r1 SPoly r -> SPoly r -> SPoly (r ++ r)
forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (AddPoly r1 r2)
%++ SPoly r
r2) Either a a' -> Eval (r ++ r) a
enc Eval (r ++ r) b -> Either b b'
dec