{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE StandaloneDeriving #-}
module Data.Polynomial(
  -- * Formal polynomials with natural-number (ℕ) coefficients
  Poly(..), Poly₀(..),
  Zero(..), Plus(..), One(..), Times(..),
  evalPoly, evalPoly₀,
  countSummands, polynomialOrder,

  -- * Type-level formal polynomials
  SZero(..), SPlus(..), SOne(..), STimes(..),
  SId(..), SCompose(..),

  SPoly(..), SPoly₀(..),
  
  EvalPoly, sEvalPoly,
  EvalPoly₀, sEvalPoly₀
) where

import Numeric.Natural (Natural)
import Data.Semigroup (Max(..))

import Data.Singletons
import Data.Kind (Type)

-- * Formal polynomials with natural-number (ℕ) coefficients

-- | A __nonzero__ formal polynomial with natural-number coefficient. If we write @{p}@ for the
--   meaning of @p :: Poly@ as a polynomial, the following holds:
--
-- @
-- {U}(x) = 1
-- {S p}(x) = 1 + {p}(x)
-- {T p}(x) = x * {p}(x)
-- @
-- 
-- In other words:
-- 
-- * @U :: Poly@ represents a constant polynomial @{U}(x) = 1@
-- * @S p :: Poly@ represents 1 plus the polynomial @{p}@.
-- * @T p :: Poly@ represents @{p}@ multiplied by the parameter of the polynomial.
-- 
-- Any __nonzero__ polynomial with coefficients in ℕ can be represented using 'Poly'.
-- In fact, they are /uniquely/ represented as a 'Poly' value.
-- For example, @1 + x^2 + x^3@ is uniquely represented as @S (T (T (S (T U))))@.
--
-- @
-- {S (T (T (S (T U))))}(x)
--   = 1 + {T (T (S (T U)))}(x)
--   = 1 + x * {T (S (T U))}(x)
--   = 1 + x * x * {S (T U)}(x)
--   = 1 + x * x * (1 + {T U}(x))
--   = 1 + x * x * (1 + x * {U}(x))
--   = 1 + x * x * (1 + x * 1)
--   = 1 + x^2 + x^3
-- @
data Poly = U | S Poly | T Poly
    deriving (Int -> Poly -> ShowS
[Poly] -> ShowS
Poly -> String
(Int -> Poly -> ShowS)
-> (Poly -> String) -> ([Poly] -> ShowS) -> Show Poly
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Poly -> ShowS
showsPrec :: Int -> Poly -> ShowS
$cshow :: Poly -> String
show :: Poly -> String
$cshowList :: [Poly] -> ShowS
showList :: [Poly] -> ShowS
Show, Poly -> Poly -> Bool
(Poly -> Poly -> Bool) -> (Poly -> Poly -> Bool) -> Eq Poly
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Poly -> Poly -> Bool
== :: Poly -> Poly -> Bool
$c/= :: Poly -> Poly -> Bool
/= :: Poly -> Poly -> Bool
Eq, Eq Poly
Eq Poly =>
(Poly -> Poly -> Ordering)
-> (Poly -> Poly -> Bool)
-> (Poly -> Poly -> Bool)
-> (Poly -> Poly -> Bool)
-> (Poly -> Poly -> Bool)
-> (Poly -> Poly -> Poly)
-> (Poly -> Poly -> Poly)
-> Ord Poly
Poly -> Poly -> Bool
Poly -> Poly -> Ordering
Poly -> Poly -> Poly
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Poly -> Poly -> Ordering
compare :: Poly -> Poly -> Ordering
$c< :: Poly -> Poly -> Bool
< :: Poly -> Poly -> Bool
$c<= :: Poly -> Poly -> Bool
<= :: Poly -> Poly -> Bool
$c> :: Poly -> Poly -> Bool
> :: Poly -> Poly -> Bool
$c>= :: Poly -> Poly -> Bool
>= :: Poly -> Poly -> Bool
$cmax :: Poly -> Poly -> Poly
max :: Poly -> Poly -> Poly
$cmin :: Poly -> Poly -> Poly
min :: Poly -> Poly -> Poly
Ord)

-- | 'Poly₀' is either zero or a 'Poly'.
--
-- @
-- {Z}(x) = 0
-- {NZ p}(x) = {p}(x)
-- @
data Poly₀ = Z | NZ Poly
    deriving (Int -> Poly₀ -> ShowS
[Poly₀] -> ShowS
Poly₀ -> String
(Int -> Poly₀ -> ShowS)
-> (Poly₀ -> String) -> ([Poly₀] -> ShowS) -> Show Poly₀
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Poly₀ -> ShowS
showsPrec :: Int -> Poly₀ -> ShowS
$cshow :: Poly₀ -> String
show :: Poly₀ -> String
$cshowList :: [Poly₀] -> ShowS
showList :: [Poly₀] -> ShowS
Show, Poly₀ -> Poly₀ -> Bool
(Poly₀ -> Poly₀ -> Bool) -> (Poly₀ -> Poly₀ -> Bool) -> Eq Poly₀
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Poly₀ -> Poly₀ -> Bool
== :: Poly₀ -> Poly₀ -> Bool
$c/= :: Poly₀ -> Poly₀ -> Bool
/= :: Poly₀ -> Poly₀ -> Bool
Eq, Eq Poly₀
Eq Poly₀ =>
(Poly₀ -> Poly₀ -> Ordering)
-> (Poly₀ -> Poly₀ -> Bool)
-> (Poly₀ -> Poly₀ -> Bool)
-> (Poly₀ -> Poly₀ -> Bool)
-> (Poly₀ -> Poly₀ -> Bool)
-> (Poly₀ -> Poly₀ -> Poly₀)
-> (Poly₀ -> Poly₀ -> Poly₀)
-> Ord Poly₀
Poly₀ -> Poly₀ -> Bool
Poly₀ -> Poly₀ -> Ordering
Poly₀ -> Poly₀ -> Poly₀
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Poly₀ -> Poly₀ -> Ordering
compare :: Poly₀ -> Poly₀ -> Ordering
$c< :: Poly₀ -> Poly₀ -> Bool
< :: Poly₀ -> Poly₀ -> Bool
$c<= :: Poly₀ -> Poly₀ -> Bool
<= :: Poly₀ -> Poly₀ -> Bool
$c> :: Poly₀ -> Poly₀ -> Bool
> :: Poly₀ -> Poly₀ -> Bool
$c>= :: Poly₀ -> Poly₀ -> Bool
>= :: Poly₀ -> Poly₀ -> Bool
$cmax :: Poly₀ -> Poly₀ -> Poly₀
max :: Poly₀ -> Poly₀ -> Poly₀
$cmin :: Poly₀ -> Poly₀ -> Poly₀
min :: Poly₀ -> Poly₀ -> Poly₀
Ord)

-- * Semiring
--
-- The algebra of natural-number-coefficient polynomial can be seen as the free semiring on a singleton set.
-- In other words, it's an expression with one unknown parameter @x@, interpretable in any semiring.

class Zero a where
    zero :: a
    default zero :: Num a => a
    zero = a
0

class Plus a where
    plus :: a -> a -> a
    default plus :: Num a => a -> a -> a
    plus = a -> a -> a
forall a. Num a => a -> a -> a
(+)

class One a where
    one :: a
    default one :: Num a => a
    one = a
1

class Times a where
    times :: a -> a -> a
    default times :: Num a => a -> a -> a
    times = a -> a -> a
forall a. Num a => a -> a -> a
(*)

evalPoly :: (Plus a, One a, Times a) => Poly -> a -> a
evalPoly :: forall a. (Plus a, One a, Times a) => Poly -> a -> a
evalPoly Poly
U = a -> a -> a
forall a b. a -> b -> a
const a
forall a. One a => a
one
evalPoly (S Poly
p) = \a
a -> a
forall a. One a => a
one a -> a -> a
forall a. Plus a => a -> a -> a
`plus` Poly -> a -> a
forall a. (Plus a, One a, Times a) => Poly -> a -> a
evalPoly Poly
p a
a
evalPoly (T Poly
p) = \a
a -> a
a a -> a -> a
forall a. Times a => a -> a -> a
`times` Poly -> a -> a
forall a. (Plus a, One a, Times a) => Poly -> a -> a
evalPoly Poly
p a
a

evalPoly₀ :: (Zero a, Plus a, One a, Times a) => Poly₀ -> a -> a
evalPoly₀ :: forall a. (Zero a, Plus a, One a, Times a) => Poly₀ -> a -> a
evalPoly₀ Poly₀
Z = a -> a -> a
forall a b. a -> b -> a
const a
forall a. Zero a => a
zero
evalPoly₀ (NZ Poly
p) = Poly -> a -> a
forall a. (Plus a, One a, Times a) => Poly -> a -> a
evalPoly Poly
p

countSummands :: Poly₀ -> Int
countSummands :: Poly₀ -> Int
countSummands Poly₀
p = Poly₀ -> Int -> Int
forall a. (Zero a, Plus a, One a, Times a) => Poly₀ -> a -> a
evalPoly₀ Poly₀
p Int
1

polynomialOrder :: Poly -> Int
polynomialOrder :: Poly -> Int
polynomialOrder Poly
p = Max Int -> Int
forall a. Max a -> a
getMax (Max Int -> Int) -> Max Int -> Int
forall a b. (a -> b) -> a -> b
$ Poly -> Max Int -> Max Int
forall a. (Plus a, One a, Times a) => Poly -> a -> a
evalPoly Poly
p (Int -> Max Int
forall a. a -> Max a
Max Int
1)

instance Zero Int
instance Plus Int
instance One Int
instance Times Int

instance Zero Natural
instance Plus Natural
instance One Natural
instance Times Natural

instance (Bounded a, Ord a) => Zero (Max a) where
    zero :: Max a
zero = a -> Max a
forall a. a -> Max a
Max a
forall a. Bounded a => a
minBound

-- | max-plus algebra (assuming addition in 'Num' preserves order)
instance (Ord a) => Plus (Max a) where
    plus :: Max a -> Max a -> Max a
plus = Max a -> Max a -> Max a
forall a. Semigroup a => a -> a -> a
(<>)

-- | max-plus algebra (assuming addition in 'Num' preserves order)
instance (Ord a, Num a) => One (Max a) where
    one :: Max a
one = Max a
0

-- | max-plus algebra
instance (Ord a, Num a) => Times (Max a) where
    times :: Max a -> Max a -> Max a
times (Max a
x) (Max a
y) = a -> Max a
forall a. a -> Max a
Max (a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
y)

instance Plus Poly where
    plus :: Poly -> Poly -> Poly
plus Poly
U Poly
y = Poly -> Poly
S Poly
y
    plus (S Poly
x) Poly
y = Poly -> Poly
S (Poly -> Poly -> Poly
forall a. Plus a => a -> a -> a
plus Poly
x Poly
y)
    plus (T Poly
x) Poly
U = Poly -> Poly
S (Poly -> Poly
T Poly
x)
    plus (T Poly
x) (S Poly
y) = Poly -> Poly
S (Poly -> Poly -> Poly
forall a. Plus a => a -> a -> a
plus (Poly -> Poly
T Poly
x) Poly
y)
    plus (T Poly
x) (T Poly
y) = Poly -> Poly
T (Poly -> Poly -> Poly
forall a. Plus a => a -> a -> a
plus Poly
x Poly
y)

instance One Poly where
    one :: Poly
one = Poly
U

instance Times Poly where
    times :: Poly -> Poly -> Poly
times Poly
U Poly
y = Poly
y
    times (S Poly
x) Poly
U = Poly -> Poly
S Poly
x
    times (S Poly
x) (S Poly
y) = Poly -> Poly
S (Poly -> Poly -> Poly
forall a. Plus a => a -> a -> a
plus (Poly -> Poly -> Poly
forall a. Plus a => a -> a -> a
plus Poly
x Poly
y) (Poly -> Poly -> Poly
forall a. Times a => a -> a -> a
times Poly
x Poly
y))
    times (S Poly
x) (T Poly
y) = Poly -> Poly
T (Poly -> Poly -> Poly
forall a. Times a => a -> a -> a
times (Poly -> Poly
S Poly
x) Poly
y)
    times (T Poly
x) Poly
y = Poly -> Poly
T (Poly -> Poly -> Poly
forall a. Times a => a -> a -> a
times Poly
x Poly
y)

instance Zero Poly₀ where
    zero :: Poly₀
zero = Poly₀
Z

instance Plus Poly₀ where
    plus :: Poly₀ -> Poly₀ -> Poly₀
plus Poly₀
Z Poly₀
y = Poly₀
y
    plus (NZ Poly
x) Poly₀
Z = Poly -> Poly₀
NZ Poly
x
    plus (NZ Poly
x) (NZ Poly
y) = Poly -> Poly₀
NZ (Poly -> Poly -> Poly
forall a. Plus a => a -> a -> a
plus Poly
x Poly
y)

instance One Poly₀ where
    one :: Poly₀
one = Poly -> Poly₀
NZ Poly
forall a. One a => a
one

instance Times Poly₀ where
    times :: Poly₀ -> Poly₀ -> Poly₀
times Poly₀
Z Poly₀
_ = Poly₀
Z
    times (NZ Poly
_) Poly₀
Z = Poly₀
Z
    times (NZ Poly
x) (NZ Poly
y) = Poly -> Poly₀
NZ (Poly -> Poly -> Poly
forall a. Times a => a -> a -> a
times Poly
x Poly
y)


-- * Singletons

data SPoly a where
    SingU :: SPoly 'U
    SingS :: SPoly p -> SPoly ('S p)
    SingT :: SPoly p -> SPoly ('T p)

type instance Sing = SPoly
deriving instance Show (SPoly p)

instance SingKind Poly where
    type Demote Poly = Poly

    fromSing :: forall (a :: Poly). Sing a -> Demote Poly
fromSing Sing a
SPoly a
SingU = Demote Poly
Poly
U
    fromSing (SingS SPoly p
p) = Poly -> Poly
S (Sing p -> Demote Poly
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Poly). Sing a -> Demote Poly
fromSing Sing p
SPoly p
p)
    fromSing (SingT SPoly p
p) = Poly -> Poly
T (Sing p -> Demote Poly
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Poly). Sing a -> Demote Poly
fromSing Sing p
SPoly p
p)

    toSing :: Demote Poly -> SomeSing Poly
toSing Demote Poly
Poly
U = Sing 'U -> SomeSing Poly
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'U
SPoly 'U
SingU
    toSing (S Poly
p) = Demote Poly
-> (forall (a :: Poly). Sing a -> SomeSing Poly) -> SomeSing Poly
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Poly
Poly
p (Sing ('S a) -> SomeSing Poly
SPoly ('S a) -> SomeSing Poly
forall k (a :: k). Sing a -> SomeSing k
SomeSing (SPoly ('S a) -> SomeSing Poly)
-> (SPoly a -> SPoly ('S a)) -> SPoly a -> SomeSing Poly
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPoly a -> SPoly ('S a)
forall (p :: Poly). SPoly p -> SPoly ('S p)
SingS)
    toSing (T Poly
p) = Demote Poly
-> (forall (a :: Poly). Sing a -> SomeSing Poly) -> SomeSing Poly
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Poly
Poly
p (Sing ('T a) -> SomeSing Poly
SPoly ('T a) -> SomeSing Poly
forall k (a :: k). Sing a -> SomeSing k
SomeSing (SPoly ('T a) -> SomeSing Poly)
-> (SPoly a -> SPoly ('T a)) -> SPoly a -> SomeSing Poly
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPoly a -> SPoly ('T a)
forall (p :: Poly). SPoly p -> SPoly ('T p)
SingT)

instance SingI 'U where sing :: Sing 'U
sing = Sing 'U
SPoly 'U
SingU
instance SingI p => SingI ('S p) where sing :: Sing ('S p)
sing = SPoly p -> SPoly ('S p)
forall (p :: Poly). SPoly p -> SPoly ('S p)
SingS Sing p
SPoly p
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI p => SingI ('T p) where sing :: Sing ('T p)
sing = SPoly p -> SPoly ('T p)
forall (p :: Poly). SPoly p -> SPoly ('T p)
SingT Sing p
SPoly p
forall {k} (a :: k). SingI a => Sing a
sing

data SPoly₀ a where
    SingZ :: SPoly₀ 'Z
    SingNZ :: SPoly p -> SPoly₀ ('NZ p)

type instance Sing = SPoly₀
deriving instance Show (SPoly₀ p)

instance SingKind Poly₀ where
    type Demote Poly₀ = Poly₀

    fromSing :: forall (a :: Poly₀). Sing a -> Demote Poly₀
fromSing Sing a
SPoly₀ a
SingZ = Demote Poly₀
Poly₀
Z
    fromSing (SingNZ SPoly p
p) = Poly -> Poly₀
NZ (Sing p -> Demote Poly
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Poly). Sing a -> Demote Poly
fromSing Sing p
SPoly p
p)

    toSing :: Demote Poly₀ -> SomeSing Poly₀
toSing Demote Poly₀
Poly₀
Z = Sing 'Z -> SomeSing Poly₀
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'Z
SPoly₀ 'Z
SingZ
    toSing (NZ Poly
p) = Demote Poly
-> (forall (a :: Poly). Sing a -> SomeSing Poly₀) -> SomeSing Poly₀
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Poly
Poly
p (Sing ('NZ a) -> SomeSing Poly₀
SPoly₀ ('NZ a) -> SomeSing Poly₀
forall k (a :: k). Sing a -> SomeSing k
SomeSing (SPoly₀ ('NZ a) -> SomeSing Poly₀)
-> (SPoly a -> SPoly₀ ('NZ a)) -> SPoly a -> SomeSing Poly₀
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPoly a -> SPoly₀ ('NZ a)
forall (p :: Poly). SPoly p -> SPoly₀ ('NZ p)
SingNZ)

instance SingI 'Z where sing :: Sing 'Z
sing = Sing 'Z
SPoly₀ 'Z
SingZ
instance SingI p => SingI ('NZ p) where sing :: Sing ('NZ p)
sing = SPoly p -> SPoly₀ ('NZ p)
forall (p :: Poly). SPoly p -> SPoly₀ ('NZ p)
SingNZ Sing p
SPoly p
forall {k} (a :: k). SingI a => Sing a
sing

--------

-- * Promoted semiring classes

class SZero (k :: Type) where
    type TZero k :: k
    sZero :: Sing (TZero k)

infixl 6 +
infixl 6 %+
class SPlus (k :: Type) where
    type (+) (x :: k) (y :: k) :: k
    (%+) :: forall (x :: k) (y :: k). Sing x -> Sing y -> Sing (x + y)

class SOne (k :: Type) where
    type TOne k :: k
    sOne :: Sing (TOne k)

infixl 7 *
infixl 7 %*
class STimes (k :: Type) where
    type (*) (x :: k) (y :: k) :: k
    (%*) :: forall (x :: k) (y :: k). Sing x -> Sing y -> Sing (x * y)

class SId (k :: Type) where
    type TId k :: k
    sId :: Sing (TId k)

infixl 8 <<
infixl 8 %<<
class SCompose (k :: Type) where
    type (<<) (x :: k) (y :: k) :: k
    (%<<) :: forall (x :: k) (y :: k). Sing x -> Sing y -> Sing (x << y)



instance SZero Poly₀ where
    type TZero Poly₀ = 'Z
    sZero :: Sing (TZero Poly₀)
sZero = Sing (TZero Poly₀)
SPoly₀ 'Z
SingZ

type family PlusPoly (x :: Poly) (y :: Poly) :: Poly where
    PlusPoly U y = S y
    PlusPoly (S x) y = S (PlusPoly x y)
    PlusPoly (T x) U = S (T x)
    PlusPoly (T x) (S y) = S (PlusPoly (T x) y)
    PlusPoly (T x) (T y) = T (PlusPoly x y)

instance SPlus Poly where
    type x + y = PlusPoly x y

    Sing x
SPoly x
SingU %+ :: forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x + y)
%+ Sing y
y = SPoly y -> SPoly ('S y)
forall (p :: Poly). SPoly p -> SPoly ('S p)
SingS Sing y
SPoly y
y
    SingS SPoly p
x %+ Sing y
y = SPoly (PlusPoly p y) -> SPoly ('S (PlusPoly p y))
forall (p :: Poly). SPoly p -> SPoly ('S p)
SingS (Sing p
SPoly p
x Sing p -> Sing y -> Sing (p + y)
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 y
y)
    SingT SPoly p
x %+ Sing y
y = case Sing y
y of
        Sing y
SPoly y
SingU -> SPoly ('T p) -> SPoly ('S ('T p))
forall (p :: Poly). SPoly p -> SPoly ('S p)
SingS (SPoly p -> SPoly ('T p)
forall (p :: Poly). SPoly p -> SPoly ('T p)
SingT SPoly p
x)
        SingS SPoly p
y' -> SPoly (PlusPoly ('T p) p) -> SPoly ('S (PlusPoly ('T p) p))
forall (p :: Poly). SPoly p -> SPoly ('S p)
SingS (SPoly p -> SPoly ('T p)
forall (p :: Poly). SPoly p -> SPoly ('T p)
SingT SPoly p
x Sing ('T p) -> Sing p -> Sing ('T 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
y')
        SingT SPoly p
y' -> SPoly (PlusPoly p p) -> SPoly ('T (PlusPoly p p))
forall (p :: Poly). SPoly p -> SPoly ('T p)
SingT (Sing p
SPoly p
x 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
y')

type family PlusPoly₀ x y :: Poly₀ where
    PlusPoly₀ Z y = y
    PlusPoly₀ (NZ x) Z = NZ x
    PlusPoly₀ (NZ x) (NZ y) = NZ (PlusPoly x y)

instance SPlus Poly₀ where
    type x + y = PlusPoly₀ x y

    Sing x
SPoly₀ x
SingZ %+ :: forall (x :: Poly₀) (y :: Poly₀). Sing x -> Sing y -> Sing (x + y)
%+ Sing y
y = Sing y
Sing (x + y)
y
    SingNZ SPoly p
x %+ Sing y
SPoly₀ y
SingZ = SPoly p -> SPoly₀ ('NZ p)
forall (p :: Poly). SPoly p -> SPoly₀ ('NZ p)
SingNZ SPoly p
x
    SingNZ SPoly p
x %+ SingNZ SPoly p
y = SPoly (PlusPoly p p) -> SPoly₀ ('NZ (PlusPoly p p))
forall (p :: Poly). SPoly p -> SPoly₀ ('NZ p)
SingNZ (Sing p
SPoly p
x 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
y)


instance SOne Poly where
    type TOne Poly = 'U
    sOne :: Sing (TOne Poly)
sOne = Sing (TOne Poly)
SPoly 'U
SingU

instance SOne Poly₀ where
    type TOne Poly₀ = 'NZ 'U
    sOne :: Sing (TOne Poly₀)
sOne = SPoly 'U -> SPoly₀ ('NZ 'U)
forall (p :: Poly). SPoly p -> SPoly₀ ('NZ p)
SingNZ Sing (TOne Poly)
SPoly 'U
forall k. SOne k => Sing (TOne k)
sOne

type family TimesPoly x y :: Poly where
    TimesPoly U y = y
    TimesPoly (S x) U = S x
    TimesPoly (S x) (S y) = S ((x + y) + TimesPoly x y)
    TimesPoly (S x) (T y) = T (TimesPoly (S x) y)
    TimesPoly (T x) y = T (TimesPoly x y)

type family TimesPoly₀ x y :: Poly₀ where
    TimesPoly₀ Z _ = Z
    TimesPoly₀ (NZ _) Z = Z
    TimesPoly₀ (NZ x) (NZ y) = NZ (TimesPoly x y)

instance STimes Poly where
    type x * y = TimesPoly x y
    Sing x
SPoly x
SingU %* :: forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x * y)
%* Sing y
y = Sing y
Sing (x * y)
y
    SingS SPoly p
x %* Sing y
SPoly y
SingU = SPoly p -> SPoly ('S p)
forall (p :: Poly). SPoly p -> SPoly ('S p)
SingS SPoly p
x
    SingS SPoly p
x %* SingS SPoly p
y = SPoly (PlusPoly (PlusPoly p p) (TimesPoly p p))
-> SPoly ('S (PlusPoly (PlusPoly p p) (TimesPoly p p)))
forall (p :: Poly). SPoly p -> SPoly ('S p)
SingS ((Sing p
SPoly p
x 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
y) Sing (PlusPoly p p)
-> Sing (TimesPoly p p) -> Sing (PlusPoly p p + TimesPoly 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
x 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
y))
    SingS SPoly p
x %* SingT SPoly p
y = SPoly (TimesPoly ('S p) p) -> SPoly ('T (TimesPoly ('S p) p))
forall (p :: Poly). SPoly p -> SPoly ('T p)
SingT (SPoly p -> SPoly ('S p)
forall (p :: Poly). SPoly p -> SPoly ('S p)
SingS SPoly p
x Sing ('S p) -> Sing p -> Sing ('S 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
y)
    SingT SPoly p
x %* Sing y
y = SPoly (TimesPoly p y) -> SPoly ('T (TimesPoly p y))
forall (p :: Poly). SPoly p -> SPoly ('T p)
SingT (Sing p
SPoly p
x Sing p -> Sing y -> Sing (p * y)
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 y
y)

instance STimes Poly₀ where
    type x * y = TimesPoly₀ x y
    Sing x
SPoly₀ x
SingZ %* :: forall (x :: Poly₀) (y :: Poly₀). Sing x -> Sing y -> Sing (x * y)
%* Sing y
_ = Sing (x * y)
SPoly₀ 'Z
SingZ
    SingNZ SPoly p
_ %* Sing y
SPoly₀ y
SingZ = Sing (x * y)
SPoly₀ 'Z
SingZ
    SingNZ SPoly p
x %* SingNZ SPoly p
y = SPoly (TimesPoly p p) -> SPoly₀ ('NZ (TimesPoly p p))
forall (p :: Poly). SPoly p -> SPoly₀ ('NZ p)
SingNZ (Sing p
SPoly p
x 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
y)

instance SId Poly where
    type TId Poly = 'S 'U
    sId :: Sing (TId Poly)
sId = SPoly 'U -> SPoly ('S 'U)
forall (p :: Poly). SPoly p -> SPoly ('S p)
SingS SPoly 'U
SingU

instance SId Poly₀ where
    type TId Poly₀ = 'NZ ('S 'U)
    sId :: Sing (TId Poly₀)
sId = SPoly ('S 'U) -> SPoly₀ ('NZ ('S 'U))
forall (p :: Poly). SPoly p -> SPoly₀ ('NZ p)
SingNZ Sing (TId Poly)
SPoly ('S 'U)
forall k. SId k => Sing (TId k)
sId

type family ComposePoly (x :: Poly) (y :: Poly) where
    ComposePoly U _ = U
    ComposePoly (S x) y = S (ComposePoly x y)
    ComposePoly (T x) y = TimesPoly y (ComposePoly x y)

type family ConstantPart' (x :: Poly) where
    ConstantPart' U = S U
    ConstantPart' (S x) = S (ConstantPart' x)
    ConstantPart' (T _) = U

type family ComposePoly₀ (x :: Poly₀) (y :: Poly₀) where
    ComposePoly₀ Z _ = Z
    ComposePoly₀ (NZ U) Z = NZ U
    ComposePoly₀ (NZ (S x)) Z = NZ (ConstantPart' x)
    ComposePoly₀ (NZ (T _)) Z = Z
    ComposePoly₀ (NZ x) (NZ y) = NZ (ComposePoly x y)

instance SCompose Poly where
    type x << y = ComposePoly x y
    Sing x
SPoly x
SingU %<< :: forall (x :: Poly) (y :: Poly). Sing x -> Sing y -> Sing (x << y)
%<< Sing y
_ = Sing (x << y)
SPoly 'U
SingU
    SingS SPoly p
x %<< Sing y
y = SPoly (ComposePoly p y) -> SPoly ('S (ComposePoly p y))
forall (p :: Poly). SPoly p -> SPoly ('S p)
SingS (Sing p
SPoly p
x Sing p -> Sing y -> Sing (p << y)
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 y
y)
    SingT SPoly p
x %<< Sing y
y = Sing y
y Sing y -> Sing (ComposePoly p y) -> Sing (y * ComposePoly p y)
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
x Sing p -> Sing y -> Sing (p << y)
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 y
y)

instance SCompose Poly₀ where
    type x << y = ComposePoly₀ x y

    Sing x
SPoly₀ x
SingZ %<< :: forall (x :: Poly₀) (y :: Poly₀). Sing x -> Sing y -> Sing (x << y)
%<< Sing y
_ = Sing (x << y)
SPoly₀ 'Z
SingZ
    SingNZ SPoly p
SingU %<< Sing y
SPoly₀ y
SingZ = SPoly 'U -> SPoly₀ ('NZ 'U)
forall (p :: Poly). SPoly p -> SPoly₀ ('NZ p)
SingNZ SPoly 'U
SingU
    SingNZ (SingS SPoly p
x) %<< Sing y
SPoly₀ y
SingZ = SPoly (ConstantPart' p) -> SPoly₀ ('NZ (ConstantPart' p))
forall (p :: Poly). SPoly p -> SPoly₀ ('NZ p)
SingNZ (SPoly p -> SPoly (ConstantPart' p)
forall (x :: Poly). SPoly x -> SPoly (ConstantPart' x)
sConstantPart SPoly p
x)
    SingNZ (SingT SPoly p
_) %<< Sing y
SPoly₀ y
SingZ = Sing (x << y)
SPoly₀ 'Z
SingZ
    SingNZ SPoly p
x %<< SingNZ SPoly p
y = SPoly (ComposePoly p p) -> SPoly₀ ('NZ (ComposePoly p p))
forall (p :: Poly). SPoly p -> SPoly₀ ('NZ p)
SingNZ (Sing p
SPoly p
x Sing p -> Sing p -> Sing (p << p)
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 p
SPoly p
y)

sConstantPart :: SPoly x -> SPoly (ConstantPart' x)
sConstantPart :: forall (x :: Poly). SPoly x -> SPoly (ConstantPart' x)
sConstantPart SPoly x
SingU = SPoly 'U -> SPoly ('S 'U)
forall (p :: Poly). SPoly p -> SPoly ('S p)
SingS SPoly 'U
SingU
sConstantPart (SingS SPoly p
x) = SPoly (ConstantPart' p) -> SPoly ('S (ConstantPart' p))
forall (p :: Poly). SPoly p -> SPoly ('S p)
SingS (SPoly p -> SPoly (ConstantPart' p)
forall (x :: Poly). SPoly x -> SPoly (ConstantPart' x)
sConstantPart SPoly p
x)
sConstantPart (SingT SPoly p
_) = SPoly (ConstantPart' x)
SPoly 'U
SingU

type family EvalPoly (x :: Poly) k (arg :: k) :: k where
    EvalPoly U k _ = TOne k
    EvalPoly (S p) k arg = TOne k + EvalPoly p k arg
    EvalPoly (T p) k arg = arg * EvalPoly p k arg

sEvalPoly :: (SOne k, SPlus k, STimes k) => SPoly x -> Sing arg -> Sing (EvalPoly x k arg)
sEvalPoly :: forall k (x :: Poly) (arg :: k).
(SOne k, SPlus k, STimes k) =>
SPoly x -> Sing arg -> Sing (EvalPoly x k arg)
sEvalPoly SPoly x
SingU Sing arg
_ = Sing (EvalPoly x k arg)
Sing (TOne k)
forall k. SOne k => Sing (TOne k)
sOne
sEvalPoly (SingS SPoly p
p) Sing arg
arg = Sing (TOne k)
forall k. SOne k => Sing (TOne k)
sOne Sing (TOne k)
-> Sing (EvalPoly p k arg) -> Sing (TOne k + EvalPoly p k arg)
forall (x :: k) (y :: k). Sing x -> Sing y -> Sing (x + y)
forall k (x :: k) (y :: k).
SPlus k =>
Sing x -> Sing y -> Sing (x + y)
%+ SPoly p -> Sing arg -> Sing (EvalPoly p k arg)
forall k (x :: Poly) (arg :: k).
(SOne k, SPlus k, STimes k) =>
SPoly x -> Sing arg -> Sing (EvalPoly x k arg)
sEvalPoly SPoly p
p Sing arg
arg
sEvalPoly (SingT SPoly p
p) Sing arg
arg = Sing arg
arg Sing arg
-> Sing (EvalPoly p k arg) -> Sing (arg * EvalPoly p k arg)
forall (x :: k) (y :: k). Sing x -> Sing y -> Sing (x * y)
forall k (x :: k) (y :: k).
STimes k =>
Sing x -> Sing y -> Sing (x * y)
%* SPoly p -> Sing arg -> Sing (EvalPoly p k arg)
forall k (x :: Poly) (arg :: k).
(SOne k, SPlus k, STimes k) =>
SPoly x -> Sing arg -> Sing (EvalPoly x k arg)
sEvalPoly SPoly p
p Sing arg
arg

type family EvalPoly₀ (x :: Poly₀) k (arg :: k) :: k where
    EvalPoly₀ Z k _ = TZero k
    EvalPoly₀ (NZ p) k arg = EvalPoly p k arg

sEvalPoly₀ :: (SZero k, SOne k, SPlus k, STimes k) => SPoly₀ x -> Sing arg -> Sing (EvalPoly₀ x k arg)
sEvalPoly₀ :: forall k (x :: Poly₀) (arg :: k).
(SZero k, SOne k, SPlus k, STimes k) =>
SPoly₀ x -> Sing arg -> Sing (EvalPoly₀ x k arg)
sEvalPoly₀ SPoly₀ x
SingZ Sing arg
_ = Sing (EvalPoly₀ x k arg)
Sing (TZero k)
forall k. SZero k => Sing (TZero k)
sZero
sEvalPoly₀ (SingNZ SPoly p
p) Sing arg
arg = SPoly p -> Sing arg -> Sing (EvalPoly p k arg)
forall k (x :: Poly) (arg :: k).
(SOne k, SPlus k, STimes k) =>
SPoly x -> Sing arg -> Sing (EvalPoly x k arg)
sEvalPoly SPoly p
p Sing arg
arg