{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DerivingVia #-}
module Data.Polynomial.Functor(
    Ev(..), Ev₀(..),
    PolynomialFunctor(..),

    toSum, fromSum, toProduct, fromProduct,
    toComp, fromComp
) where

import Data.Kind (Type)

import Data.Functor.Identity
import GHC.Generics hiding (S,C,D)

import Data.Singletons
import Data.Polynomial

data Ev₀ (p :: Poly₀) (x :: Type) where
    MakeEv₀ :: Ev p x -> Ev₀ (NZ p) x

deriving instance Eq x => Eq (Ev₀ p x)
deriving instance Ord x => Ord (Ev₀ p x)
deriving instance Show x => Show (Ev₀ p x)
deriving instance Functor (Ev₀ p)

data Ev (p :: Poly) (x :: Type) where
    End :: Ev 'U x
    Stop :: Ev ('S p) x
    Go :: Ev p x -> Ev ('S p) x
    (:::) :: x -> Ev p x -> Ev ('T p) x

infixr 7 :::

deriving instance Eq x => Eq (Ev p x)
deriving instance Ord x => Ord (Ev p x)
deriving instance Show x => Show (Ev p x)
deriving instance Functor (Ev p)
deriving instance Foldable (Ev p)
deriving instance Traversable (Ev p)

-- | Non-zero polynomial functor
class Functor f => PolynomialFunctor f where
    type PolyRep f :: Poly

    sPolyRep :: Sing (PolyRep f)
    toPoly :: f x -> Ev (PolyRep f) x
    fromPoly :: Ev (PolyRep f) x -> f x

instance SingI p => PolynomialFunctor (Ev p) where
    type PolyRep (Ev p) = p
    sPolyRep :: Sing (PolyRep (Ev p))
sPolyRep = Sing p
Sing (PolyRep (Ev p))
forall {k} (a :: k). SingI a => Sing a
sing
    toPoly :: forall x. Ev p x -> Ev (PolyRep (Ev p)) x
toPoly = Ev p x -> Ev p x
Ev p x -> Ev (PolyRep (Ev p)) x
forall a. a -> a
id
    fromPoly :: forall x. Ev (PolyRep (Ev p)) x -> Ev p x
fromPoly = Ev p x -> Ev p x
Ev (PolyRep (Ev p)) x -> Ev p x
forall a. a -> a
id

instance PolynomialFunctor Proxy where
    type PolyRep Proxy = U
    sPolyRep :: Sing (PolyRep Proxy)
sPolyRep = Sing (PolyRep Proxy)
SPoly 'U
SingU
    toPoly :: forall x. Proxy x -> Ev (PolyRep Proxy) x
toPoly Proxy x
_ = Ev 'U x
Ev (PolyRep Proxy) x
forall x. Ev 'U x
End
    fromPoly :: forall x. Ev (PolyRep Proxy) x -> Proxy x
fromPoly Ev (PolyRep Proxy) x
_ = Proxy x
forall {k} (t :: k). Proxy t
Proxy
 
instance PolynomialFunctor Identity where
    type PolyRep Identity = T U

    sPolyRep :: Sing (PolyRep Identity)
sPolyRep = SPoly 'U -> SPoly ('T 'U)
forall (p :: Poly). SPoly p -> SPoly ('T p)
SingT SPoly 'U
SingU
    toPoly :: forall x. Identity x -> Ev (PolyRep Identity) x
toPoly (Identity x
x) = x
x x -> Ev 'U x -> Ev ('T 'U) x
forall x (p :: Poly). x -> Ev p x -> Ev ('T p) x
::: Ev 'U x
forall x. Ev 'U x
End
    fromPoly :: forall x. Ev (PolyRep Identity) x -> Identity x
fromPoly (x
x ::: Ev p x
End) = x -> Identity x
forall a. a -> Identity a
Identity x
x

instance PolynomialFunctor U1 where
    type PolyRep U1 = U
    sPolyRep :: Sing (PolyRep U1)
sPolyRep = Sing (PolyRep U1)
SPoly 'U
SingU
    toPoly :: forall x. U1 x -> Ev (PolyRep U1) x
toPoly U1 x
_ = Ev 'U x
Ev (PolyRep U1) x
forall x. Ev 'U x
End
    fromPoly :: forall x. Ev (PolyRep U1) x -> U1 x
fromPoly Ev (PolyRep U1) x
_ = U1 x
forall k (p :: k). U1 p
U1

-- | Quick&dirty alternative to @Finitary c => PolynomialFunctor (K1 i c)@
instance PolynomialFunctor (K1 i ()) where
    type PolyRep (K1 i ()) = U
    sPolyRep :: Sing (PolyRep (K1 i ()))
sPolyRep = Sing (PolyRep (K1 i ()))
SPoly 'U
SingU
    toPoly :: forall x. K1 i () x -> Ev (PolyRep (K1 i ())) x
toPoly K1 i () x
_ = Ev 'U x
Ev (PolyRep (K1 i ())) x
forall x. Ev 'U x
End
    fromPoly :: forall x. Ev (PolyRep (K1 i ())) x -> K1 i () x
fromPoly Ev (PolyRep (K1 i ())) x
_ = () -> K1 i () x
forall k i c (p :: k). c -> K1 i c p
K1 ()

-- | Quick&dirty alternative to @Finitary c => PolynomialFunctor (K1 i c)@
instance PolynomialFunctor (K1 i Bool) where
    type PolyRep (K1 i Bool) = S U
    sPolyRep :: Sing (PolyRep (K1 i Bool))
sPolyRep = Sing ('S 'U)
Sing (PolyRep (K1 i Bool))
forall {k} (a :: k). SingI a => Sing a
sing

    toPoly :: forall x. K1 i Bool x -> Ev (PolyRep (K1 i Bool)) x
toPoly (K1 Bool
b) = if Bool
b then Ev 'U x -> Ev ('S 'U) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go Ev 'U x
forall x. Ev 'U x
End else Ev ('S 'U) x
Ev (PolyRep (K1 i Bool)) x
forall (p :: Poly) x. Ev ('S p) x
Stop
    fromPoly :: forall x. Ev (PolyRep (K1 i Bool)) x -> K1 i Bool x
fromPoly Ev (PolyRep (K1 i Bool)) x
Stop = Bool -> K1 i Bool x
forall k i c (p :: k). c -> K1 i c p
K1 Bool
False
    fromPoly (Go Ev p x
_) = Bool -> K1 i Bool x
forall k i c (p :: k). c -> K1 i c p
K1 Bool
True

instance PolynomialFunctor f => PolynomialFunctor (M1 i m f) where
    type PolyRep (M1 _ _ f) = PolyRep f
    sPolyRep :: Sing (PolyRep (M1 i m f))
sPolyRep = forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @f
    toPoly :: forall x. M1 i m f x -> Ev (PolyRep (M1 i m f)) x
toPoly = f x -> Ev (PolyRep f) x
forall x. f x -> Ev (PolyRep f) x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
f x -> Ev (PolyRep f) x
toPoly (f x -> Ev (PolyRep f) x)
-> (M1 i m f x -> f x) -> M1 i m f x -> Ev (PolyRep f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i m f x -> f x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1
    fromPoly :: forall x. Ev (PolyRep (M1 i m f)) x -> M1 i m f x
fromPoly = f x -> M1 i m f x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (f x -> M1 i m f x)
-> (Ev (PolyRep f) x -> f x) -> Ev (PolyRep f) x -> M1 i m f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ev (PolyRep f) x -> f x
forall x. Ev (PolyRep f) x -> f x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
Ev (PolyRep f) x -> f x
fromPoly

instance PolynomialFunctor f => PolynomialFunctor (Rec1 f) where
    type PolyRep (Rec1 f) = PolyRep f
    sPolyRep :: Sing (PolyRep (Rec1 f))
sPolyRep = forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @f
    toPoly :: forall x. Rec1 f x -> Ev (PolyRep (Rec1 f)) x
toPoly = f x -> Ev (PolyRep f) x
forall x. f x -> Ev (PolyRep f) x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
f x -> Ev (PolyRep f) x
toPoly (f x -> Ev (PolyRep f) x)
-> (Rec1 f x -> f x) -> Rec1 f x -> Ev (PolyRep f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec1 f x -> f x
forall k (f :: k -> Type) (p :: k). Rec1 f p -> f p
unRec1
    fromPoly :: forall x. Ev (PolyRep (Rec1 f)) x -> Rec1 f x
fromPoly = f x -> Rec1 f x
forall k (f :: k -> Type) (p :: k). f p -> Rec1 f p
Rec1 (f x -> Rec1 f x)
-> (Ev (PolyRep f) x -> f x) -> Ev (PolyRep f) x -> Rec1 f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ev (PolyRep f) x -> f x
forall x. Ev (PolyRep f) x -> f x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
Ev (PolyRep f) x -> f x
fromPoly

instance (PolynomialFunctor f, PolynomialFunctor g) => PolynomialFunctor (f :+: g) where
    type PolyRep (f :+: g) = PolyRep f + PolyRep g

    sPolyRep :: Sing (PolyRep (f :+: g))
sPolyRep = forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @f Sing (PolyRep f)
-> Sing (PolyRep g) -> Sing (PolyRep f + PolyRep g)
forall k (x :: k) (y :: k).
SPlus k =>
Sing x -> Sing y -> Sing (x + y)
forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x + y)
%+ forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @g

    toPoly :: forall x. (:+:) f g x -> Ev (PolyRep (f :+: g)) x
toPoly (L1 f x
fx) = Sing (PolyRep f)
-> Sing (PolyRep g)
-> (:+:) (Ev (PolyRep f)) (Ev (PolyRep g)) x
-> Ev (PolyRep f + PolyRep g) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum (forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @f) (forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @g) (Ev (PolyRep f) x -> (:+:) (Ev (PolyRep f)) (Ev (PolyRep g)) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (f x -> Ev (PolyRep f) x
forall x. f x -> Ev (PolyRep f) x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
f x -> Ev (PolyRep f) x
toPoly f x
fx))
    toPoly (R1 g x
gx) = Sing (PolyRep f)
-> Sing (PolyRep g)
-> (:+:) (Ev (PolyRep f)) (Ev (PolyRep g)) x
-> Ev (PolyRep f + PolyRep g) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum (forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @f) (forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @g) (Ev (PolyRep g) x -> (:+:) (Ev (PolyRep f)) (Ev (PolyRep g)) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (g x -> Ev (PolyRep g) x
forall x. g x -> Ev (PolyRep g) x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
f x -> Ev (PolyRep f) x
toPoly g x
gx))

    fromPoly :: forall x. Ev (PolyRep (f :+: g)) x -> (:+:) f g x
fromPoly Ev (PolyRep (f :+: g)) x
hx = case Sing (PolyRep f)
-> Sing (PolyRep g)
-> Ev (PolyRep f + PolyRep g) x
-> (:+:) (Ev (PolyRep f)) (Ev (PolyRep g)) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
toSum (forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @f) (forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @g) Ev (PolyRep f + PolyRep g) x
Ev (PolyRep (f :+: g)) x
hx of
        L1 Ev (PolyRep f) x
fx -> f x -> (:+:) f g x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (Ev (PolyRep f) x -> f x
forall x. Ev (PolyRep f) x -> f x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
Ev (PolyRep f) x -> f x
fromPoly Ev (PolyRep f) x
fx)
        R1 Ev (PolyRep g) x
gx -> g x -> (:+:) f g x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (Ev (PolyRep g) x -> g x
forall x. Ev (PolyRep g) x -> g x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
Ev (PolyRep f) x -> f x
fromPoly Ev (PolyRep g) x
gx)

toSum :: Sing p -> Sing q -> Ev (p + q) x -> (Ev p :+: Ev q) x
toSum :: forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
toSum Sing p
sp Sing q
sq Ev (p + q) x
hx = case Sing p
sp of
    Sing p
SPoly p
SingU -> case Ev (p + q) x
hx of
        Ev (p + q) x
Stop -> Ev p x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
Ev 'U x
forall x. Ev 'U x
End
        Go Ev p x
gx -> Ev q x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev q x
Ev p x
gx
    SingS SPoly p
sp' -> case Ev (p + q) x
hx of
        Ev (p + q) x
Stop -> Ev p x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
Ev ('S p) x
forall (p :: Poly) x. Ev ('S p) x
Stop
        Go Ev p x
hx' -> case Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
toSum Sing p
SPoly p
sp' Sing q
sq Ev p x
Ev (p + q) x
hx' of
            L1 Ev p x
fx -> Ev p x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (Ev p x -> Ev ('S p) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go Ev p x
fx)
            R1 Ev q x
gx -> Ev q x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev q x
gx
    SingT SPoly p
sp' -> case Sing q
sq of
        Sing q
SPoly q
SingU -> case Ev (p + q) x
hx of
            Ev (p + q) x
Stop -> Ev q x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev q x
Ev 'U x
forall x. Ev 'U x
End
            Go Ev p x
fx -> Ev p x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
Ev p x
fx
        SingS SPoly p
sq' -> case Ev (p + q) x
hx of
            Ev (p + q) x
Stop -> Ev q x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev q x
Ev ('S p) x
forall (p :: Poly) x. Ev ('S p) x
Stop
            Go Ev p x
hx' -> case Sing p -> Sing p -> Ev (p + p) x -> (:+:) (Ev p) (Ev p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
toSum Sing p
sp Sing p
SPoly p
sq' Ev p x
Ev (p + p) x
hx' of
                L1 Ev p x
fx -> Ev p x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
fx
                R1 Ev p x
gx -> Ev q x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (Ev p x -> Ev ('S p) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go Ev p x
gx)
        SingT SPoly p
sq' -> case Ev (p + q) x
hx of
            x
x ::: Ev p x
hx' -> case Sing p -> Sing p -> Ev (p + p) x -> (:+:) (Ev p) (Ev p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
toSum Sing p
SPoly p
sp' Sing p
SPoly p
sq' Ev p x
Ev (p + p) x
hx' of
                L1 Ev p x
fx -> Ev p x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (x
x x -> Ev p x -> Ev ('T p) x
forall x (p :: Poly). x -> Ev p x -> Ev ('T p) x
::: Ev p x
fx)
                R1 Ev p x
gx -> Ev q x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (x
x x -> Ev p x -> Ev ('T p) x
forall x (p :: Poly). x -> Ev p x -> Ev ('T p) x
::: Ev p x
gx)

fromSum :: Sing p -> Sing q -> (Ev p :+: Ev q) x -> Ev (p + q) x
fromSum :: forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
sp Sing q
sq (:+:) (Ev p) (Ev q) x
fgx = case Sing p
sp of
    Sing p
SPoly p
SingU -> case (:+:) (Ev p) (Ev q) x
fgx of
        L1 Ev p x
End -> Ev (p + q) x
Ev ('S q) x
forall (p :: Poly) x. Ev ('S p) x
Stop
        R1 Ev q x
gx -> Ev q x -> Ev ('S q) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go Ev q x
gx
    SingS SPoly p
sp' -> case (:+:) (Ev p) (Ev q) x
fgx of
        L1 Ev p x
Stop -> Ev (p + q) x
Ev ('S (PlusPoly p q)) x
forall (p :: Poly) x. Ev ('S p) x
Stop
        L1 (Go Ev p x
fx) -> Ev (PlusPoly p q) x -> Ev ('S (PlusPoly p q)) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go (Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
SPoly p
sp' Sing q
sq (Ev p x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
fx))
        R1 Ev q x
gx -> Ev (PlusPoly p q) x -> Ev ('S (PlusPoly p q)) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go (Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
SPoly p
sp' Sing q
sq (Ev q x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev q x
gx))
    SingT SPoly p
sp' -> case Sing q
sq of
        Sing q
SPoly q
SingU -> case (:+:) (Ev p) (Ev q) x
fgx of
            L1 Ev p x
fx -> Ev p x -> Ev ('S p) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go Ev p x
fx
            R1 Ev q x
End -> Ev (p + q) x
Ev ('S ('T p)) x
forall (p :: Poly) x. Ev ('S p) x
Stop
        SingS SPoly p
sq' -> case (:+:) (Ev p) (Ev q) x
fgx of
            L1 Ev p x
fx -> Ev (PlusPoly ('T p) p) x -> Ev ('S (PlusPoly ('T p) p)) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go (Sing p -> Sing p -> (:+:) (Ev p) (Ev p) x -> Ev (p + p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
sp Sing p
SPoly p
sq' (Ev p x -> (:+:) (Ev p) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
fx))
            R1 Ev q x
Stop -> Ev (p + q) x
Ev ('S (PlusPoly ('T p) p)) x
forall (p :: Poly) x. Ev ('S p) x
Stop
            R1 (Go Ev p x
gx) -> Ev (PlusPoly ('T p) p) x -> Ev ('S (PlusPoly ('T p) p)) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go (Sing ('T p)
-> Sing p -> (:+:) (Ev ('T p)) (Ev p) x -> Ev ('T p + p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
Sing ('T p)
sp Sing p
SPoly p
sq' (Ev p x -> (:+:) (Ev ('T p)) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev p x
gx))
        SingT SPoly p
sq' -> case (:+:) (Ev p) (Ev q) x
fgx of
            L1 (x
x ::: Ev p x
fx) -> x
x x -> Ev (PlusPoly p p) x -> Ev ('T (PlusPoly p p)) x
forall x (p :: Poly). x -> Ev p x -> Ev ('T p) x
::: Sing p -> Sing p -> (:+:) (Ev p) (Ev p) x -> Ev (p + p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
SPoly p
sp' Sing p
SPoly p
sq' (Ev p x -> (:+:) (Ev p) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
fx)
            R1 (x
x ::: Ev p x
gx) -> x
x x -> Ev (PlusPoly p p) x -> Ev ('T (PlusPoly p p)) x
forall x (p :: Poly). x -> Ev p x -> Ev ('T p) x
::: Sing p -> Sing p -> (:+:) (Ev p) (Ev p) x -> Ev (p + p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
SPoly p
sp' Sing p
SPoly p
sq' (Ev p x -> (:+:) (Ev p) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev p x
gx)

instance (PolynomialFunctor f, PolynomialFunctor g) => PolynomialFunctor (f :*: g) where
    type PolyRep (f :*: g) = PolyRep f * PolyRep g
    
    sPolyRep :: Sing (PolyRep (f :*: g))
sPolyRep = forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @f Sing (PolyRep f)
-> Sing (PolyRep g) -> Sing (PolyRep f * PolyRep g)
forall k (x :: k) (y :: k).
STimes k =>
Sing x -> Sing y -> Sing (x * y)
forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x * y)
%* forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @g
    toPoly :: forall x. (:*:) f g x -> Ev (PolyRep (f :*: g)) x
toPoly (f x
fx :*: g x
gx) = Sing (PolyRep f)
-> Sing (PolyRep g)
-> (:*:) (Ev (PolyRep f)) (Ev (PolyRep g)) x
-> Ev (PolyRep f * PolyRep g) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:*:) (Ev p) (Ev q) x -> Ev (p * q) x
fromProduct (forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @f) (forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @g) (f x -> Ev (PolyRep f) x
forall x. f x -> Ev (PolyRep f) x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
f x -> Ev (PolyRep f) x
toPoly f x
fx Ev (PolyRep f) x
-> Ev (PolyRep g) x -> (:*:) (Ev (PolyRep f)) (Ev (PolyRep g)) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: g x -> Ev (PolyRep g) x
forall x. g x -> Ev (PolyRep g) x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
f x -> Ev (PolyRep f) x
toPoly g x
gx)
    fromPoly :: forall x. Ev (PolyRep (f :*: g)) x -> (:*:) f g x
fromPoly Ev (PolyRep (f :*: g)) x
hx = case Sing (PolyRep f)
-> Sing (PolyRep g)
-> Ev (PolyRep f * PolyRep g) x
-> (:*:) (Ev (PolyRep f)) (Ev (PolyRep g)) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> Ev (p * q) x -> (:*:) (Ev p) (Ev q) x
toProduct (forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @f) (forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @g) Ev (PolyRep f * PolyRep g) x
Ev (PolyRep (f :*: g)) x
hx of
        (Ev (PolyRep f) x
fx :*: Ev (PolyRep g) x
gx) -> Ev (PolyRep f) x -> f x
forall x. Ev (PolyRep f) x -> f x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
Ev (PolyRep f) x -> f x
fromPoly Ev (PolyRep f) x
fx f x -> g x -> (:*:) f g x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev (PolyRep g) x -> g x
forall x. Ev (PolyRep g) x -> g x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
Ev (PolyRep f) x -> f x
fromPoly Ev (PolyRep g) x
gx

fromProduct :: Sing p -> Sing q -> (Ev p :*: Ev q) x -> Ev (p * q) x
fromProduct :: forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:*:) (Ev p) (Ev q) x -> Ev (p * q) x
fromProduct Sing p
sp Sing q
sq (Ev p x
fx :*: Ev q x
gx) = case Sing p
sp of
    Sing p
SPoly p
SingU -> Ev q x
Ev (p * q) x
gx
    SingS SPoly p
sp' -> case Sing q
sq of
        Sing q
SPoly q
SingU -> Ev p x
Ev (p * q) x
fx
        SingS SPoly p
sq' -> case (Ev p x
fx, Ev q x
gx) of
            (Ev p x
Stop,  Ev q x
Stop)  -> Ev (p * q) x
Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x
forall (p :: Poly) x. Ev ('S p) x
Stop
            (Go Ev p x
fx', Ev q x
Stop)  -> Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
-> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go (Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
 -> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x)
-> Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
-> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x
forall a b. (a -> b) -> a -> b
$ Sing (PlusPoly p p)
-> Sing (TimesPoly p p)
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
-> Ev (PlusPoly p p + TimesPoly p p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum (Sing p
SPoly p
sp' Sing p -> Sing p -> Sing (p + p)
forall k (x :: k) (y :: k).
SPlus k =>
Sing x -> Sing y -> Sing (x + y)
forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x + y)
%+ Sing p
SPoly p
sq') (Sing p
SPoly p
sp' Sing p -> Sing p -> Sing (p * p)
forall k (x :: k) (y :: k).
STimes k =>
Sing x -> Sing y -> Sing (x * y)
forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x * y)
%* Sing p
SPoly p
sq') (Ev (PlusPoly p p) x
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (Ev (PlusPoly p p) x
 -> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x)
-> Ev (PlusPoly p p) x
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
forall a b. (a -> b) -> a -> b
$ Sing p -> Sing p -> (:+:) (Ev p) (Ev p) x -> Ev (p + p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
SPoly p
sp' Sing p
SPoly p
sq' (Ev p x -> (:+:) (Ev p) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
fx'))
            (Ev p x
Stop,  Go Ev p x
gx') -> Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
-> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go (Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
 -> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x)
-> Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
-> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x
forall a b. (a -> b) -> a -> b
$ Sing (PlusPoly p p)
-> Sing (TimesPoly p p)
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
-> Ev (PlusPoly p p + TimesPoly p p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum (Sing p
SPoly p
sp' Sing p -> Sing p -> Sing (p + p)
forall k (x :: k) (y :: k).
SPlus k =>
Sing x -> Sing y -> Sing (x + y)
forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x + y)
%+ Sing p
SPoly p
sq') (Sing p
SPoly p
sp' Sing p -> Sing p -> Sing (p * p)
forall k (x :: k) (y :: k).
STimes k =>
Sing x -> Sing y -> Sing (x * y)
forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x * y)
%* Sing p
SPoly p
sq') (Ev (PlusPoly p p) x
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (Ev (PlusPoly p p) x
 -> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x)
-> Ev (PlusPoly p p) x
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
forall a b. (a -> b) -> a -> b
$ Sing p -> Sing p -> (:+:) (Ev p) (Ev p) x -> Ev (p + p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
SPoly p
sp' Sing p
SPoly p
sq' (Ev p x -> (:+:) (Ev p) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev p x
gx'))
            (Go Ev p x
fx', Go Ev p x
gx') -> Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
-> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go (Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
 -> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x)
-> Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
-> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x
forall a b. (a -> b) -> a -> b
$ Sing (PlusPoly p p)
-> Sing (TimesPoly p p)
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
-> Ev (PlusPoly p p + TimesPoly p p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum (Sing p
SPoly p
sp' Sing p -> Sing p -> Sing (p + p)
forall k (x :: k) (y :: k).
SPlus k =>
Sing x -> Sing y -> Sing (x + y)
forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x + y)
%+ Sing p
SPoly p
sq') (Sing p
SPoly p
sp' Sing p -> Sing p -> Sing (p * p)
forall k (x :: k) (y :: k).
STimes k =>
Sing x -> Sing y -> Sing (x * y)
forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x * y)
%* Sing p
SPoly p
sq') (Ev (TimesPoly p p) x
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (Ev (TimesPoly p p) x
 -> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x)
-> Ev (TimesPoly p p) x
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
forall a b. (a -> b) -> a -> b
$ Sing p -> Sing p -> (:*:) (Ev p) (Ev p) x -> Ev (p * p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:*:) (Ev p) (Ev q) x -> Ev (p * q) x
fromProduct Sing p
SPoly p
sp' Sing p
SPoly p
sq' (Ev p x
fx' Ev p x -> Ev p x -> (:*:) (Ev p) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev p x
gx'))
        SingT SPoly p
sq' -> case Ev q x
gx of
            x
x ::: Ev p x
gx' -> x
x x -> Ev (TimesPoly ('S p) p) x -> Ev ('T (TimesPoly ('S p) p)) x
forall x (p :: Poly). x -> Ev p x -> Ev ('T p) x
::: Sing p -> Sing p -> (:*:) (Ev p) (Ev p) x -> Ev (p * p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:*:) (Ev p) (Ev q) x -> Ev (p * q) x
fromProduct Sing p
sp Sing p
SPoly p
sq' (Ev p x
fx Ev p x -> Ev p x -> (:*:) (Ev p) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev p x
gx')
    SingT SPoly p
sp' -> case Ev p x
fx of
        x
x ::: Ev p x
fx' -> x
x x -> Ev (TimesPoly p q) x -> Ev ('T (TimesPoly p q)) x
forall x (p :: Poly). x -> Ev p x -> Ev ('T p) x
::: Sing p -> Sing q -> (:*:) (Ev p) (Ev q) x -> Ev (p * q) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:*:) (Ev p) (Ev q) x -> Ev (p * q) x
fromProduct Sing p
SPoly p
sp' Sing q
sq (Ev p x
fx' Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev q x
gx)

toProduct :: Sing p -> Sing q -> Ev (p * q) x -> (Ev p :*: Ev q) x
toProduct :: forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> Ev (p * q) x -> (:*:) (Ev p) (Ev q) x
toProduct Sing p
sp Sing q
sq Ev (p * q) x
hx = case Sing p
sp of
    Sing p
SPoly p
SingU -> Ev p x
Ev 'U x
forall x. Ev 'U x
End Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev q x
Ev (p * q) x
hx
    SingS SPoly p
sp' -> case Sing q
sq of
        Sing q
SPoly q
SingU -> Ev p x
Ev (p * q) x
hx Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev q x
Ev 'U x
forall x. Ev 'U x
End
        SingS SPoly p
sq' -> case Ev (p * q) x
hx of
            Ev (p * q) x
Stop -> Ev p x
Ev ('S p) x
forall (p :: Poly) x. Ev ('S p) x
Stop Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev q x
Ev ('S p) x
forall (p :: Poly) x. Ev ('S p) x
Stop
            Go Ev p x
hx' -> case Sing (PlusPoly p p)
-> Sing (TimesPoly p p)
-> Ev (PlusPoly p p + TimesPoly p p) x
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
toSum (Sing p
SPoly p
sp' Sing p -> Sing p -> Sing (p + p)
forall k (x :: k) (y :: k).
SPlus k =>
Sing x -> Sing y -> Sing (x + y)
forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x + y)
%+ Sing p
SPoly p
sq') (Sing p
SPoly p
sp' Sing p -> Sing p -> Sing (p * p)
forall k (x :: k) (y :: k).
STimes k =>
Sing x -> Sing y -> Sing (x * y)
forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x * y)
%* Sing p
SPoly p
sq') Ev p x
Ev (PlusPoly p p + TimesPoly p p) x
hx' of
                L1 Ev (PlusPoly p p) x
hx'' -> case Sing p -> Sing p -> Ev (p + p) x -> (:+:) (Ev p) (Ev p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
toSum Sing p
SPoly p
sp' Sing p
SPoly p
sq' Ev (PlusPoly p p) x
Ev (p + p) x
hx'' of
                    L1 Ev p x
fx' -> Ev p x -> Ev ('S p) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go Ev p x
fx' Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev q x
Ev ('S p) x
forall (p :: Poly) x. Ev ('S p) x
Stop
                    R1 Ev p x
gx' -> Ev p x
Ev ('S p) x
forall (p :: Poly) x. Ev ('S p) x
Stop Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev p x -> Ev ('S p) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go Ev p x
gx'
                R1 Ev (TimesPoly p p) x
hx'' ->
                    let Ev p x
fx' :*: Ev p x
gx' = Sing p -> Sing p -> Ev (p * p) x -> (:*:) (Ev p) (Ev p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> Ev (p * q) x -> (:*:) (Ev p) (Ev q) x
toProduct Sing p
SPoly p
sp' Sing p
SPoly p
sq' Ev (TimesPoly p p) x
Ev (p * p) x
hx''
                    in Ev p x -> Ev ('S p) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go Ev p x
fx' Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev p x -> Ev ('S p) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go Ev p x
gx'
        SingT SPoly p
sq' -> case Ev (p * q) x
hx of
            x
x ::: Ev p x
hx' ->
                let Ev p x
fx :*: Ev p x
gx' = Sing p -> Sing p -> Ev (p * p) x -> (:*:) (Ev p) (Ev p) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> Ev (p * q) x -> (:*:) (Ev p) (Ev q) x
toProduct Sing p
sp Sing p
SPoly p
sq' Ev p x
Ev (p * p) x
hx'
                in Ev p x
fx Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: (x
x x -> Ev p x -> Ev ('T p) x
forall x (p :: Poly). x -> Ev p x -> Ev ('T p) x
::: Ev p x
gx')
    SingT SPoly p
sp' -> case Ev (p * q) x
hx of
        x
x ::: Ev p x
hx' ->
            let Ev p x
fx' :*: Ev q x
gx = Sing p -> Sing q -> Ev (p * q) x -> (:*:) (Ev p) (Ev q) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> Ev (p * q) x -> (:*:) (Ev p) (Ev q) x
toProduct Sing p
SPoly p
sp' Sing q
sq Ev p x
Ev (p * q) x
hx'
            in (x
x x -> Ev p x -> Ev ('T p) x
forall x (p :: Poly). x -> Ev p x -> Ev ('T p) x
::: Ev p x
fx') Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev q x
gx

instance PolynomialFunctor Par1 where
    type PolyRep Par1 = T U
    sPolyRep :: Sing (PolyRep Par1)
sPolyRep = SPoly 'U -> SPoly ('T 'U)
forall (p :: Poly). SPoly p -> SPoly ('T p)
SingT SPoly 'U
SingU

    toPoly :: forall x. Par1 x -> Ev (PolyRep Par1) x
toPoly (Par1 x
x) = x
x x -> Ev 'U x -> Ev ('T 'U) x
forall x (p :: Poly). x -> Ev p x -> Ev ('T p) x
::: Ev 'U x
forall x. Ev 'U x
End
    fromPoly :: forall x. Ev (PolyRep Par1) x -> Par1 x
fromPoly (x
x ::: Ev p x
End) = x -> Par1 x
forall p. p -> Par1 p
Par1 x
x

instance (PolynomialFunctor f, PolynomialFunctor g) => PolynomialFunctor (f :.: g) where
    type PolyRep (f :.: g) = PolyRep f << PolyRep g
    sPolyRep :: Sing (PolyRep (f :.: g))
sPolyRep = forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @f Sing (PolyRep f)
-> Sing (PolyRep g) -> Sing (PolyRep f << PolyRep g)
forall k (x :: k) (y :: k).
SCompose k =>
Sing x -> Sing y -> Sing (x << y)
forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x << y)
%<< forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @g

    toPoly :: forall x. (:.:) f g x -> Ev (PolyRep (f :.: g)) x
toPoly (Comp1 f (g x)
fgx) = SPoly (PolyRep f)
-> SPoly (PolyRep g)
-> Ev (PolyRep f) (Ev (PolyRep g) x)
-> Ev (PolyRep f << PolyRep g) x
forall (p :: Poly) (q :: Poly) x.
SPoly p -> SPoly q -> Ev p (Ev q x) -> Ev (p << q) x
fromComp (forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @f) (forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @g) (f (Ev (PolyRep g) x) -> Ev (PolyRep f) (Ev (PolyRep g) x)
forall x. f x -> Ev (PolyRep f) x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
f x -> Ev (PolyRep f) x
toPoly ((g x -> Ev (PolyRep g) x) -> f (g x) -> f (Ev (PolyRep g) x)
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap g x -> Ev (PolyRep g) x
forall x. g x -> Ev (PolyRep g) x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
f x -> Ev (PolyRep f) x
toPoly f (g x)
fgx))
    fromPoly :: forall x. Ev (PolyRep (f :.: g)) x -> (:.:) f g x
fromPoly Ev (PolyRep (f :.: g)) x
hx = f (g x) -> (:.:) f g x
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (f (g x) -> (:.:) f g x) -> f (g x) -> (:.:) f g x
forall a b. (a -> b) -> a -> b
$ (Ev (PolyRep g) x -> g x) -> f (Ev (PolyRep g) x) -> f (g x)
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: Type -> Type) x.
PolynomialFunctor f =>
Ev (PolyRep f) x -> f x
fromPoly @g) (f (Ev (PolyRep g) x) -> f (g x))
-> f (Ev (PolyRep g) x) -> f (g x)
forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) x.
PolynomialFunctor f =>
Ev (PolyRep f) x -> f x
fromPoly @f (Ev (PolyRep f) (Ev (PolyRep g) x) -> f (Ev (PolyRep g) x))
-> Ev (PolyRep f) (Ev (PolyRep g) x) -> f (Ev (PolyRep g) x)
forall a b. (a -> b) -> a -> b
$ SPoly (PolyRep f)
-> SPoly (PolyRep g)
-> Ev (PolyRep f << PolyRep g) x
-> Ev (PolyRep f) (Ev (PolyRep g) x)
forall (p :: Poly) (q :: Poly) x.
SPoly p -> SPoly q -> Ev (p << q) x -> Ev p (Ev q x)
toComp (forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @f) (forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @g) Ev (PolyRep f << PolyRep g) x
Ev (PolyRep (f :.: g)) x
hx

fromComp :: SPoly p -> SPoly q -> Ev p (Ev q x) -> Ev (p << q) x
fromComp :: forall (p :: Poly) (q :: Poly) x.
SPoly p -> SPoly q -> Ev p (Ev q x) -> Ev (p << q) x
fromComp SPoly p
sp SPoly q
sq Ev p (Ev q x)
fgx = case SPoly p
sp of
    SPoly p
SingU -> Ev (p << q) x
Ev 'U x
forall x. Ev 'U x
End
    SingS SPoly p
sp' -> case Ev p (Ev q x)
fgx of
        Ev p (Ev q x)
Stop -> Ev (p << q) x
Ev ('S (ComposePoly p q)) x
forall (p :: Poly) x. Ev ('S p) x
Stop
        Go Ev p (Ev q x)
fgx' -> Ev (ComposePoly p q) x -> Ev ('S (ComposePoly p q)) x
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go (SPoly p -> SPoly q -> Ev p (Ev q x) -> Ev (p << q) x
forall (p :: Poly) (q :: Poly) x.
SPoly p -> SPoly q -> Ev p (Ev q x) -> Ev (p << q) x
fromComp SPoly p
sp' SPoly q
sq Ev p (Ev q x)
Ev p (Ev q x)
fgx')
    SingT SPoly p
sp' -> case Ev p (Ev q x)
fgx of
        Ev q x
gx ::: Ev p (Ev q x)
fgx' -> Sing q
-> Sing (ComposePoly p q)
-> (:*:) (Ev q) (Ev (ComposePoly p q)) x
-> Ev (q * ComposePoly p q) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> (:*:) (Ev p) (Ev q) x -> Ev (p * q) x
fromProduct Sing q
SPoly q
sq (Sing p
SPoly p
sp' Sing p -> Sing q -> Sing (p << q)
forall k (x :: k) (y :: k).
SCompose k =>
Sing x -> Sing y -> Sing (x << y)
forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x << y)
%<< Sing q
SPoly q
sq) (Ev q x
gx Ev q x
-> Ev (ComposePoly p q) x -> (:*:) (Ev q) (Ev (ComposePoly p q)) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: SPoly p -> SPoly q -> Ev p (Ev q x) -> Ev (p << q) x
forall (p :: Poly) (q :: Poly) x.
SPoly p -> SPoly q -> Ev p (Ev q x) -> Ev (p << q) x
fromComp SPoly p
sp' SPoly q
sq Ev p (Ev q x)
Ev p (Ev q x)
fgx')

toComp :: SPoly p -> SPoly q -> Ev (p << q) x -> Ev p (Ev q x)
toComp :: forall (p :: Poly) (q :: Poly) x.
SPoly p -> SPoly q -> Ev (p << q) x -> Ev p (Ev q x)
toComp SPoly p
sp SPoly q
sq Ev (p << q) x
hx = case SPoly p
sp of
    SPoly p
SingU -> Ev p (Ev q x)
Ev 'U (Ev q x)
forall x. Ev 'U x
End
    SingS SPoly p
sp' -> case Ev (p << q) x
hx of
        Ev (p << q) x
Stop -> Ev p (Ev q x)
Ev ('S p) (Ev q x)
forall (p :: Poly) x. Ev ('S p) x
Stop
        Go Ev p x
hx' -> Ev p (Ev q x) -> Ev ('S p) (Ev q x)
forall (p :: Poly) x. Ev p x -> Ev ('S p) x
Go (SPoly p -> SPoly q -> Ev (p << q) x -> Ev p (Ev q x)
forall (p :: Poly) (q :: Poly) x.
SPoly p -> SPoly q -> Ev (p << q) x -> Ev p (Ev q x)
toComp SPoly p
sp' SPoly q
sq Ev p x
Ev (p << q) x
hx')
    SingT SPoly p
sp' -> 
        let Ev q x
gx :*: Ev (ComposePoly p q) x
hx' = Sing q
-> Sing (ComposePoly p q)
-> Ev (q * ComposePoly p q) x
-> (:*:) (Ev q) (Ev (ComposePoly p q)) x
forall (p :: Poly) (q :: Poly) x.
Sing p -> Sing q -> Ev (p * q) x -> (:*:) (Ev p) (Ev q) x
toProduct Sing q
SPoly q
sq (Sing p
SPoly p
sp' Sing p -> Sing q -> Sing (p << q)
forall k (x :: k) (y :: k).
SCompose k =>
Sing x -> Sing y -> Sing (x << y)
forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x << y)
%<< Sing q
SPoly q
sq) Ev (p << q) x
Ev (q * ComposePoly p q) x
hx
        in Ev q x
gx Ev q x -> Ev p (Ev q x) -> Ev ('T p) (Ev q x)
forall x (p :: Poly). x -> Ev p x -> Ev ('T p) x
::: SPoly p -> SPoly q -> Ev (p << q) x -> Ev p (Ev q x)
forall (p :: Poly) (q :: Poly) x.
SPoly p -> SPoly q -> Ev (p << q) x -> Ev p (Ev q x)
toComp SPoly p
sp' SPoly q
sq Ev (ComposePoly p q) x
Ev (p << q) x
hx'

-- via Generically1
instance (Generic1 f, PolynomialFunctor (Rep1 f)) => PolynomialFunctor (Generically1 f) where
    type PolyRep (Generically1 f) = PolyRep (Rep1 f)
    sPolyRep :: Sing (PolyRep (Generically1 f))
sPolyRep = forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @(Rep1 f)
    toPoly :: forall x. Generically1 f x -> Ev (PolyRep (Generically1 f)) x
toPoly (Generically1 f x
fx) = forall (f :: Type -> Type) x.
PolynomialFunctor f =>
f x -> Ev (PolyRep f) x
toPoly @(Rep1 f) (Rep1 f x -> Ev (PolyRep (Generically1 f)) x)
-> (f x -> Rep1 f x) -> f x -> Ev (PolyRep (Generically1 f)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> Rep1 f x
forall a. f a -> Rep1 f a
forall k (f :: k -> Type) (a :: k). Generic1 f => f a -> Rep1 f a
from1 (f x -> Ev (PolyRep (Generically1 f)) x)
-> f x -> Ev (PolyRep (Generically1 f)) x
forall a b. (a -> b) -> a -> b
$ f x
fx
    fromPoly :: forall x. Ev (PolyRep (Generically1 f)) x -> Generically1 f x
fromPoly = f x -> Generically1 f x
forall {k} (f :: k -> Type) (a :: k). f a -> Generically1 f a
Generically1 (f x -> Generically1 f x)
-> (Ev (PolyRep (Rep1 f)) x -> f x)
-> Ev (PolyRep (Rep1 f)) x
-> Generically1 f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep1 f x -> f x
forall a. Rep1 f a -> f a
forall k (f :: k -> Type) (a :: k). Generic1 f => Rep1 f a -> f a
to1 (Rep1 f x -> f x)
-> (Ev (PolyRep (Rep1 f)) x -> Rep1 f x)
-> Ev (PolyRep (Rep1 f)) x
-> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) x.
PolynomialFunctor f =>
Ev (PolyRep f) x -> f x
fromPoly @(Rep1 f)

deriving
  via Generically1 Maybe
  instance PolynomialFunctor Maybe