{-# 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
  P(..), P₀(..),
  Zero(..), Plus(..), One(..), Times(..),
  evalPoly, evalPoly₀,
  countSummands, polynomialOrder,

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

  SingP(..), SingP₀(..),
  
  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 :: P@ 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 :: P@ represents a constant polynomial @{U}(x) = 1@
-- * @S p :: P@ represents 1 plus the polynomial @{p}@.
-- * @T p :: P@ represents @{p}@ multiplied by the parameter of the polynomial.
-- 
-- Any __nonzero__ polynomial with coefficients in ℕ can be represented using 'P'.
-- In fact, they are /uniquely/ represented as a 'P' 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 P = U | S P | T P
    deriving (Int -> P -> ShowS
[P] -> ShowS
P -> String
(Int -> P -> ShowS) -> (P -> String) -> ([P] -> ShowS) -> Show P
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> P -> ShowS
showsPrec :: Int -> P -> ShowS
$cshow :: P -> String
show :: P -> String
$cshowList :: [P] -> ShowS
showList :: [P] -> ShowS
Show, P -> P -> Bool
(P -> P -> Bool) -> (P -> P -> Bool) -> Eq P
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: P -> P -> Bool
== :: P -> P -> Bool
$c/= :: P -> P -> Bool
/= :: P -> P -> Bool
Eq, Eq P
Eq P =>
(P -> P -> Ordering)
-> (P -> P -> Bool)
-> (P -> P -> Bool)
-> (P -> P -> Bool)
-> (P -> P -> Bool)
-> (P -> P -> P)
-> (P -> P -> P)
-> Ord P
P -> P -> Bool
P -> P -> Ordering
P -> P -> P
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 :: P -> P -> Ordering
compare :: P -> P -> Ordering
$c< :: P -> P -> Bool
< :: P -> P -> Bool
$c<= :: P -> P -> Bool
<= :: P -> P -> Bool
$c> :: P -> P -> Bool
> :: P -> P -> Bool
$c>= :: P -> P -> Bool
>= :: P -> P -> Bool
$cmax :: P -> P -> P
max :: P -> P -> P
$cmin :: P -> P -> P
min :: P -> P -> P
Ord)

-- | 'P₀' is either zero or a 'P'.
--
-- @
-- {Z}(x) = 0
-- {NZ p}(x) = {p}(x)
-- @
data P₀ = Z | NZ P
    deriving (Int -> P₀ -> ShowS
[P₀] -> ShowS
P₀ -> String
(Int -> P₀ -> ShowS)
-> (P₀ -> String) -> ([P₀] -> ShowS) -> Show P₀
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> P₀ -> ShowS
showsPrec :: Int -> P₀ -> ShowS
$cshow :: P₀ -> String
show :: P₀ -> String
$cshowList :: [P₀] -> ShowS
showList :: [P₀] -> ShowS
Show, P₀ -> P₀ -> Bool
(P₀ -> P₀ -> Bool) -> (P₀ -> P₀ -> Bool) -> Eq P₀
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: P₀ -> P₀ -> Bool
== :: P₀ -> P₀ -> Bool
$c/= :: P₀ -> P₀ -> Bool
/= :: P₀ -> P₀ -> Bool
Eq, Eq P₀
Eq P₀ =>
(P₀ -> P₀ -> Ordering)
-> (P₀ -> P₀ -> Bool)
-> (P₀ -> P₀ -> Bool)
-> (P₀ -> P₀ -> Bool)
-> (P₀ -> P₀ -> Bool)
-> (P₀ -> P₀ -> P₀)
-> (P₀ -> P₀ -> P₀)
-> Ord P₀
P₀ -> P₀ -> Bool
P₀ -> P₀ -> Ordering
P₀ -> P₀ -> P₀
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 :: P₀ -> P₀ -> Ordering
compare :: P₀ -> P₀ -> Ordering
$c< :: P₀ -> P₀ -> Bool
< :: P₀ -> P₀ -> Bool
$c<= :: P₀ -> P₀ -> Bool
<= :: P₀ -> P₀ -> Bool
$c> :: P₀ -> P₀ -> Bool
> :: P₀ -> P₀ -> Bool
$c>= :: P₀ -> P₀ -> Bool
>= :: P₀ -> P₀ -> Bool
$cmax :: P₀ -> P₀ -> P₀
max :: P₀ -> P₀ -> P₀
$cmin :: P₀ -> P₀ -> P₀
min :: P₀ -> P₀ -> P₀
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) => P -> a -> a
evalPoly :: forall a. (Plus a, One a, Times a) => P -> a -> a
evalPoly P
U = a -> a -> a
forall a b. a -> b -> a
const a
forall a. One a => a
one
evalPoly (S P
p) = \a
a -> a
forall a. One a => a
one a -> a -> a
forall a. Plus a => a -> a -> a
`plus` P -> a -> a
forall a. (Plus a, One a, Times a) => P -> a -> a
evalPoly P
p a
a
evalPoly (T P
p) = \a
a -> a
a a -> a -> a
forall a. Times a => a -> a -> a
`times` P -> a -> a
forall a. (Plus a, One a, Times a) => P -> a -> a
evalPoly P
p a
a

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

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

polynomialOrder :: P -> Int
polynomialOrder :: P -> Int
polynomialOrder P
p = Max Int -> Int
forall a. Max a -> a
getMax (Max Int -> Int) -> Max Int -> Int
forall a b. (a -> b) -> a -> b
$ P -> Max Int -> Max Int
forall a. (Plus a, One a, Times a) => P -> a -> a
evalPoly P
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 P where
    plus :: P -> P -> P
plus P
U P
y = P -> P
S P
y
    plus (S P
x) P
y = P -> P
S (P -> P -> P
forall a. Plus a => a -> a -> a
plus P
x P
y)
    plus (T P
x) P
U = P -> P
S (P -> P
T P
x)
    plus (T P
x) (S P
y) = P -> P
S (P -> P -> P
forall a. Plus a => a -> a -> a
plus (P -> P
T P
x) P
y)
    plus (T P
x) (T P
y) = P -> P
T (P -> P -> P
forall a. Plus a => a -> a -> a
plus P
x P
y)

instance One P where
    one :: P
one = P
U

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

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

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

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

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


-- * Singletons

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

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

instance SingKind P where
    type Demote P = P

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

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

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

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

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

instance SingKind P₀ where
    type Demote P₀ = P₀

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

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

instance SingI 'Z where sing :: Sing 'Z
sing = Sing 'Z
SingP₀ 'Z
SingZ
instance SingI p => SingI ('NZ p) where sing :: Sing ('NZ p)
sing = SingP p -> SingP₀ ('NZ p)
forall (p :: P). SingP p -> SingP₀ ('NZ p)
SingNZ Sing p
SingP 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 P₀ where
    type TZero P₀ = 'Z
    sZero :: Sing (TZero P₀)
sZero = Sing (TZero P₀)
SingP₀ 'Z
SingZ

type family PlusPoly (x :: P) (y :: P) :: P 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 P where
    type x + y = PlusPoly x y

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

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

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

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


instance SOne P where
    type TOne P = 'U
    sOne :: Sing (TOne P)
sOne = Sing (TOne P)
SingP 'U
SingU

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

type family TimesPoly x y :: P 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 :: P₀ where
    TimesPoly₀ Z _ = Z
    TimesPoly₀ (NZ _) Z = Z
    TimesPoly₀ (NZ x) (NZ y) = NZ (TimesPoly x y)

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

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

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

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

type family ComposePoly (x :: P) (y :: P) 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 :: P) where
    ConstantPart' U = S U
    ConstantPart' (S x) = S (ConstantPart' x)
    ConstantPart' (T _) = U

type family ComposePoly₀ (x :: P₀) (y :: P₀) 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 P where
    type x << y = ComposePoly x y
    Sing x
SingP x
SingU %<< :: forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x << y)
%<< Sing y
_ = Sing (x << y)
SingP 'U
SingU
    SingS SingP p
x %<< Sing y
y = SingP (ComposePoly p y) -> SingP ('S (ComposePoly p y))
forall (p :: P). SingP p -> SingP ('S p)
SingS (Sing p
SingP 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 :: P) (y :: P). Sing x -> Sing y -> Sing (x << y)
%<< Sing y
y)
    SingT SingP 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 :: P) (y :: P). Sing x -> Sing y -> Sing (x * y)
%* (Sing p
SingP 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 :: P) (y :: P). Sing x -> Sing y -> Sing (x << y)
%<< Sing y
y)

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

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

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

type family EvalPoly (x :: P) 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) => SingP x -> Sing arg -> Sing (EvalPoly x k arg)
sEvalPoly :: forall k (x :: P) (arg :: k).
(SOne k, SPlus k, STimes k) =>
SingP x -> Sing arg -> Sing (EvalPoly x k arg)
sEvalPoly SingP x
SingU Sing arg
_ = Sing (EvalPoly x k arg)
Sing (TOne k)
forall k. SOne k => Sing (TOne k)
sOne
sEvalPoly (SingS SingP 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)
%+ SingP p -> Sing arg -> Sing (EvalPoly p k arg)
forall k (x :: P) (arg :: k).
(SOne k, SPlus k, STimes k) =>
SingP x -> Sing arg -> Sing (EvalPoly x k arg)
sEvalPoly SingP p
p Sing arg
arg
sEvalPoly (SingT SingP 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)
%* SingP p -> Sing arg -> Sing (EvalPoly p k arg)
forall k (x :: P) (arg :: k).
(SOne k, SPlus k, STimes k) =>
SingP x -> Sing arg -> Sing (EvalPoly x k arg)
sEvalPoly SingP p
p Sing arg
arg

type family EvalPoly₀ (x :: P₀) 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) => SingP₀ x -> Sing arg -> Sing (EvalPoly₀ x k arg)
sEvalPoly₀ :: forall k (x :: P₀) (arg :: k).
(SZero k, SOne k, SPlus k, STimes k) =>
SingP₀ x -> Sing arg -> Sing (EvalPoly₀ x k arg)
sEvalPoly₀ SingP₀ x
SingZ Sing arg
_ = Sing (EvalPoly₀ x k arg)
Sing (TZero k)
forall k. SZero k => Sing (TZero k)
sZero
sEvalPoly₀ (SingNZ SingP p
p) Sing arg
arg = SingP p -> Sing arg -> Sing (EvalPoly p k arg)
forall k (x :: P) (arg :: k).
(SOne k, SPlus k, STimes k) =>
SingP x -> Sing arg -> Sing (EvalPoly x k arg)
sEvalPoly SingP p
p Sing arg
arg