Safe Haskell	None
Language	Haskell2010

Data.Polynomial

Contents

Formal polynomials with natural-number (ℕ) coefficients
Type-level formal polynomials

Synopsis

data P
- = U
- | S P
- | T P
data P₀
- = Z
- | NZ P
class Zero a where
- zero :: a
class Plus a where
- plus :: a -> a -> a
class One a where
- one :: a
class Times a where
- times :: a -> a -> a
evalPoly :: (Plus a, One a, Times a) => P -> a -> a
evalPoly₀ :: (Zero a, Plus a, One a, Times a) => P₀ -> a -> a
countSummands :: P₀ -> Int
polynomialOrder :: P -> Int
class SZero k where
- type TZero k :: k
- sZero :: Sing (TZero k)
class SPlus k where
- type (x :: k) + (y :: k) :: k
- (%+) :: forall (x :: k) (y :: k). Sing x -> Sing y -> Sing (x + y)
class SOne k where
- type TOne k :: k
- sOne :: Sing (TOne k)
class STimes k where
- type (x :: k) * (y :: k) :: k
- (%*) :: forall (x :: k) (y :: k). Sing x -> Sing y -> Sing (x * y)
class SId k where
- type TId k :: k
- sId :: Sing (TId k)
class SCompose k where
- type (x :: k) << (y :: k) :: k
- (%<<) :: forall (x :: k) (y :: k). Sing x -> Sing y -> Sing (x << y)
data SingP (a :: P) where
- SingU :: SingP 'U
- SingS :: forall (p :: P). SingP p -> SingP ('S p)
- SingT :: forall (p :: P). SingP p -> SingP ('T p)
data SingP₀ (a :: P₀) where
- SingZ :: SingP₀ 'Z
- SingNZ :: forall (p :: P). SingP p -> SingP₀ ('NZ p)
type family EvalPoly (x :: P) k (arg :: k) :: k where ...
sEvalPoly :: forall k (x :: P) (arg :: k). (SOne k, SPlus k, STimes k) => SingP x -> Sing arg -> Sing (EvalPoly x k arg)
type family EvalPoly₀ (x :: P₀) k (arg :: k) :: k where ...
sEvalPoly₀ :: forall k (x :: P₀) (arg :: k). (SZero k, SOne k, SPlus k, STimes k) => SingP₀ x -> Sing arg -> Sing (EvalPoly₀ x k arg)

Formal polynomials with natural-number (ℕ) coefficients

data P Source #

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

Constructors

U
S P
T P

Instances

Instances details

One P Source #

Instance details

Defined in Data.Polynomial

Methods

one :: P Source #

Plus P Source #

Instance details

Defined in Data.Polynomial

Methods

plus :: P -> P -> P Source #

SCompose P Source #

Instance details

Defined in Data.Polynomial

Associated Types

type (x :: P) << (y :: P)
Instance details Defined in Data.Polynomial type (x :: P) << (y :: P)

Methods

(%<<) :: forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x << y) Source #

SId P Source #

Instance details

Defined in Data.Polynomial

Associated Types

type TId P
Instance details Defined in Data.Polynomial type TId P = 'S 'U

Methods

sId :: Sing (TId P) Source #

SOne P Source #

Instance details

Defined in Data.Polynomial

Associated Types

type TOne P
Instance details Defined in Data.Polynomial type TOne P = 'U

Methods

sOne :: Sing (TOne P) Source #

SPlus P Source #

Instance details

Defined in Data.Polynomial

Associated Types

type (x :: P) + (y :: P)
Instance details Defined in Data.Polynomial type (x :: P) + (y :: P)

Methods

(%+) :: forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x + y) Source #

STimes P Source #

Instance details

Defined in Data.Polynomial

Associated Types

type (x :: P) * (y :: P)
Instance details Defined in Data.Polynomial type (x :: P) * (y :: P)

Methods

(%*) :: forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x * y) Source #

Times P Source #

Instance details

Defined in Data.Polynomial

Methods

times :: P -> P -> P Source #

Show P Source #

Instance details

Defined in Data.Polynomial

Methods

showsPrec :: Int -> P -> ShowS #

show :: P -> String #

showList :: [P] -> ShowS #

Eq P Source #

Instance details

Defined in Data.Polynomial

Methods

(==) :: P -> P -> Bool #

(/=) :: P -> P -> Bool #

Ord P Source #

Instance details

Defined in Data.Polynomial

Methods

compare :: P -> P -> Ordering #

(<) :: P -> P -> Bool #

(<=) :: P -> P -> Bool #

(>) :: P -> P -> Bool #

(>=) :: P -> P -> Bool #

max :: P -> P -> P #

min :: P -> P -> P #

SingKind P Source #

Instance details

Defined in Data.Polynomial

Associated Types

type Demote P
Instance details Defined in Data.Polynomial type Demote P = P

Methods

fromSing :: forall (a :: P). Sing a -> Demote P #

toSing :: Demote P -> SomeSing P #

SingI 'U Source #

Instance details

Defined in Data.Polynomial

Methods

sing :: Sing 'U #

SingI p => SingI ('S p :: P) Source #

Instance details

Defined in Data.Polynomial

Methods

sing :: Sing ('S p) #

SingI p => SingI ('T p :: P) Source #

Instance details

Defined in Data.Polynomial

Methods

sing :: Sing ('T p) #

type TId P Source #

Instance details

Defined in Data.Polynomial

type TId P = 'S 'U

type TOne P Source #

Instance details

Defined in Data.Polynomial

type TOne P = 'U

type Demote P Source #

Instance details

Defined in Data.Polynomial

type Demote P = P

type Sing Source #

Instance details

Defined in Data.Polynomial

type Sing = SingP

type (x :: P) * (y :: P) Source #

Instance details

Defined in Data.Polynomial

type (x :: P) * (y :: P)

type (x :: P) + (y :: P) Source #

Instance details

Defined in Data.Polynomial

type (x :: P) + (y :: P)

type (x :: P) << (y :: P) Source #

Instance details

Defined in Data.Polynomial

type (x :: P) << (y :: P)

data P₀ Source #

P₀ is either zero or a P.

{Z}(x) = 0
{NZ p}(x) = {p}(x)

Constructors

Z
NZ P

Instances

Instances details

One P₀ Source #

Instance details

Defined in Data.Polynomial

Methods

one :: P₀ Source #

Plus P₀ Source #

Instance details

Defined in Data.Polynomial

Methods

plus :: P₀ -> P₀ -> P₀ Source #

SCompose P₀ Source #

Instance details

Defined in Data.Polynomial

Associated Types

type (x :: P₀) << (y :: P₀)
Instance details Defined in Data.Polynomial type (x :: P₀) << (y :: P₀)

Methods

(%<<) :: forall (x :: P₀) (y :: P₀). Sing x -> Sing y -> Sing (x << y) Source #

SId P₀ Source #

Instance details

Defined in Data.Polynomial

Associated Types

type TId P₀
Instance details Defined in Data.Polynomial type TId P₀ = 'NZ ('S 'U)

Methods

sId :: Sing (TId P₀) Source #

SOne P₀ Source #

Instance details

Defined in Data.Polynomial

Associated Types

type TOne P₀
Instance details Defined in Data.Polynomial type TOne P₀ = 'NZ 'U

Methods

sOne :: Sing (TOne P₀) Source #

SPlus P₀ Source #

Instance details

Defined in Data.Polynomial

Associated Types

type (x :: P₀) + (y :: P₀)
Instance details Defined in Data.Polynomial type (x :: P₀) + (y :: P₀)

Methods

(%+) :: forall (x :: P₀) (y :: P₀). Sing x -> Sing y -> Sing (x + y) Source #

STimes P₀ Source #

Instance details

Defined in Data.Polynomial

Associated Types

type (x :: P₀) * (y :: P₀)
Instance details Defined in Data.Polynomial type (x :: P₀) * (y :: P₀)

Methods

(%*) :: forall (x :: P₀) (y :: P₀). Sing x -> Sing y -> Sing (x * y) Source #

SZero P₀ Source #

Instance details

Defined in Data.Polynomial

Associated Types

type TZero P₀
Instance details Defined in Data.Polynomial type TZero P₀ = 'Z

Methods

sZero :: Sing (TZero P₀) Source #

Times P₀ Source #

Instance details

Defined in Data.Polynomial

Methods

times :: P₀ -> P₀ -> P₀ Source #

Zero P₀ Source #

Instance details

Defined in Data.Polynomial

Methods

zero :: P₀ Source #

Show P₀ Source #

Instance details

Defined in Data.Polynomial

Methods

showsPrec :: Int -> P₀ -> ShowS #

show :: P₀ -> String #

showList :: [P₀] -> ShowS #

Eq P₀ Source #

Instance details

Defined in Data.Polynomial

Methods

(==) :: P₀ -> P₀ -> Bool #

(/=) :: P₀ -> P₀ -> Bool #

Ord P₀ Source #

Instance details

Defined in Data.Polynomial

Methods

compare :: P₀ -> P₀ -> Ordering #

(<) :: P₀ -> P₀ -> Bool #

(<=) :: P₀ -> P₀ -> Bool #

(>) :: P₀ -> P₀ -> Bool #

(>=) :: P₀ -> P₀ -> Bool #

max :: P₀ -> P₀ -> P₀ #

min :: P₀ -> P₀ -> P₀ #

SingKind P₀ Source #

Instance details

Defined in Data.Polynomial

Associated Types

type Demote P₀
Instance details Defined in Data.Polynomial type Demote P₀ = P₀

Methods

fromSing :: forall (a :: P₀). Sing a -> Demote P₀ #

toSing :: Demote P₀ -> SomeSing P₀ #

SingI 'Z Source #

Instance details

Defined in Data.Polynomial

Methods

sing :: Sing 'Z #

SingI p => SingI ('NZ p :: P₀) Source #

Instance details

Defined in Data.Polynomial

Methods

sing :: Sing ('NZ p) #

type TId P₀ Source #

Instance details

Defined in Data.Polynomial

type TId P₀ = 'NZ ('S 'U)

type TOne P₀ Source #

Instance details

Defined in Data.Polynomial

type TOne P₀ = 'NZ 'U

type TZero P₀ Source #

Instance details

Defined in Data.Polynomial

type TZero P₀ = 'Z

type Demote P₀ Source #

Instance details

Defined in Data.Polynomial

type Demote P₀ = P₀

type Sing Source #

Instance details

Defined in Data.Polynomial

type Sing = SingP₀

type (x :: P₀) * (y :: P₀) Source #

Instance details

Defined in Data.Polynomial

type (x :: P₀) * (y :: P₀)

type (x :: P₀) + (y :: P₀) Source #

Instance details

Defined in Data.Polynomial

type (x :: P₀) + (y :: P₀)

type (x :: P₀) << (y :: P₀) Source #

Instance details

Defined in Data.Polynomial

type (x :: P₀) << (y :: P₀)

class Zero a where Source #

Minimal complete definition

Nothing

Methods

zero :: a Source #

default zero :: Num a => a Source #

Instances

Instances details

Zero P₀ Source #
Instance details Defined in Data.Polynomial Methods zero :: P₀ Source #
Zero Natural Source #
Instance details Defined in Data.Polynomial Methods zero :: Natural Source #
Zero Int Source #
Instance details Defined in Data.Polynomial Methods zero :: Int Source #
(Bounded a, Ord a) => Zero (Max a) Source #
Instance details Defined in Data.Polynomial Methods zero :: Max a Source #

class Plus a where Source #

Minimal complete definition

Nothing

Methods

plus :: a -> a -> a Source #

default plus :: Num a => a -> a -> a Source #

Instances

Instances details

Plus P Source #
Instance details Defined in Data.Polynomial Methods plus :: P -> P -> P Source #
Plus P₀ Source #
Instance details Defined in Data.Polynomial Methods plus :: P₀ -> P₀ -> P₀ Source #
Plus Natural Source #
Instance details Defined in Data.Polynomial Methods plus :: Natural -> Natural -> Natural Source #
Plus Int Source #
Instance details Defined in Data.Polynomial Methods plus :: Int -> Int -> Int Source #
Ord a => Plus (Max a) Source #	max-plus algebra (assuming addition in `Num` preserves order)
Instance details Defined in Data.Polynomial Methods plus :: Max a -> Max a -> Max a Source #

class One a where Source #

Minimal complete definition

Nothing

Methods

one :: a Source #

default one :: Num a => a Source #

Instances

Instances details

One P Source #
Instance details Defined in Data.Polynomial Methods one :: P Source #
One P₀ Source #
Instance details Defined in Data.Polynomial Methods one :: P₀ Source #
One Natural Source #
Instance details Defined in Data.Polynomial Methods one :: Natural Source #
One Int Source #
Instance details Defined in Data.Polynomial Methods one :: Int Source #
(Ord a, Num a) => One (Max a) Source #	max-plus algebra (assuming addition in `Num` preserves order)
Instance details Defined in Data.Polynomial Methods one :: Max a Source #

class Times a where Source #

Minimal complete definition

Nothing

Methods

times :: a -> a -> a Source #

default times :: Num a => a -> a -> a Source #

Instances

Instances details

Times P Source #
Instance details Defined in Data.Polynomial Methods times :: P -> P -> P Source #
Times P₀ Source #
Instance details Defined in Data.Polynomial Methods times :: P₀ -> P₀ -> P₀ Source #
Times Natural Source #
Instance details Defined in Data.Polynomial Methods times :: Natural -> Natural -> Natural Source #
Times Int Source #
Instance details Defined in Data.Polynomial Methods times :: Int -> Int -> Int Source #
(Ord a, Num a) => Times (Max a) Source #	max-plus algebra
Instance details Defined in Data.Polynomial Methods times :: Max a -> Max a -> Max a Source #

evalPoly :: (Plus a, One a, Times a) => P -> a -> a Source #

evalPoly₀ :: (Zero a, Plus a, One a, Times a) => P₀ -> a -> a Source #

countSummands :: P₀ -> Int Source #

polynomialOrder :: P -> Int Source #

Type-level formal polynomials

class SZero k where Source #

Associated Types

type TZero k :: k Source #

Methods

sZero :: Sing (TZero k) Source #

Instances

Instances details

SZero P₀ Source #

Instance details

Defined in Data.Polynomial

Associated Types

type TZero P₀
Instance details Defined in Data.Polynomial type TZero P₀ = 'Z

Methods

sZero :: Sing (TZero P₀) Source #

class SPlus k where Source #

Associated Types

type (x :: k) + (y :: k) :: k infixl 6 Source #

Methods

(%+) :: forall (x :: k) (y :: k). Sing x -> Sing y -> Sing (x + y) infixl 6 Source #

Instances

Instances details

SPlus P Source #

Instance details

Defined in Data.Polynomial

Associated Types

type (x :: P) + (y :: P)
Instance details Defined in Data.Polynomial type (x :: P) + (y :: P)

Methods

(%+) :: forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x + y) Source #

SPlus P₀ Source #

Instance details

Defined in Data.Polynomial

Associated Types

type (x :: P₀) + (y :: P₀)
Instance details Defined in Data.Polynomial type (x :: P₀) + (y :: P₀)

Methods

(%+) :: forall (x :: P₀) (y :: P₀). Sing x -> Sing y -> Sing (x + y) Source #

class SOne k where Source #

Associated Types

type TOne k :: k Source #

Methods

sOne :: Sing (TOne k) Source #

Instances

Instances details

SOne P Source #

Instance details

Defined in Data.Polynomial

Associated Types

type TOne P
Instance details Defined in Data.Polynomial type TOne P = 'U

Methods

sOne :: Sing (TOne P) Source #

SOne P₀ Source #

Instance details

Defined in Data.Polynomial

Associated Types

type TOne P₀
Instance details Defined in Data.Polynomial type TOne P₀ = 'NZ 'U

Methods

sOne :: Sing (TOne P₀) Source #

class STimes k where Source #

Associated Types

type (x :: k) * (y :: k) :: k infixl 7 Source #

Methods

(%*) :: forall (x :: k) (y :: k). Sing x -> Sing y -> Sing (x * y) infixl 7 Source #

Instances

Instances details

STimes P Source #

Instance details

Defined in Data.Polynomial

Associated Types

type (x :: P) * (y :: P)
Instance details Defined in Data.Polynomial type (x :: P) * (y :: P)

Methods

(%*) :: forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x * y) Source #

STimes P₀ Source #

Instance details

Defined in Data.Polynomial

Associated Types

type (x :: P₀) * (y :: P₀)
Instance details Defined in Data.Polynomial type (x :: P₀) * (y :: P₀)

Methods

(%*) :: forall (x :: P₀) (y :: P₀). Sing x -> Sing y -> Sing (x * y) Source #

class SId k where Source #

Associated Types

type TId k :: k Source #

Methods

sId :: Sing (TId k) Source #

Instances

Instances details

SId P Source #

Instance details

Defined in Data.Polynomial

Associated Types

type TId P
Instance details Defined in Data.Polynomial type TId P = 'S 'U

Methods

sId :: Sing (TId P) Source #

SId P₀ Source #

Instance details

Defined in Data.Polynomial

Associated Types

type TId P₀
Instance details Defined in Data.Polynomial type TId P₀ = 'NZ ('S 'U)

Methods

sId :: Sing (TId P₀) Source #

class SCompose k where Source #

Associated Types

type (x :: k) << (y :: k) :: k infixl 8 Source #

Methods

(%<<) :: forall (x :: k) (y :: k). Sing x -> Sing y -> Sing (x << y) infixl 8 Source #

Instances

Instances details

SCompose P Source #

Instance details

Defined in Data.Polynomial

Associated Types

type (x :: P) << (y :: P)
Instance details Defined in Data.Polynomial type (x :: P) << (y :: P)

Methods

(%<<) :: forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x << y) Source #

SCompose P₀ Source #

Instance details

Defined in Data.Polynomial

Associated Types

type (x :: P₀) << (y :: P₀)
Instance details Defined in Data.Polynomial type (x :: P₀) << (y :: P₀)

Methods

(%<<) :: forall (x :: P₀) (y :: P₀). Sing x -> Sing y -> Sing (x << y) Source #

data SingP (a :: P) where Source #

Constructors

SingU :: SingP 'U
SingS :: forall (p :: P). SingP p -> SingP ('S p)
SingT :: forall (p :: P). SingP p -> SingP ('T p)

Instances

Instances details

Show (SingP p) Source #
Instance details Defined in Data.Polynomial Methods showsPrec :: Int -> SingP p -> ShowS # show :: SingP p -> String # showList :: [SingP p] -> ShowS #

data SingP₀ (a :: P₀) where Source #

Constructors

SingZ :: SingP₀ 'Z
SingNZ :: forall (p :: P). SingP p -> SingP₀ ('NZ p)

Instances

Instances details

Show (SingP₀ p) Source #
Instance details Defined in Data.Polynomial Methods showsPrec :: Int -> SingP₀ p -> ShowS # show :: SingP₀ p -> String # showList :: [SingP₀ p] -> ShowS #

type family EvalPoly (x :: P) k (arg :: k) :: k where ... Source #

Equations

EvalPoly 'U k (_1 :: k) = TOne k
EvalPoly ('S p) k (arg :: k) = TOne k + EvalPoly p k arg
EvalPoly ('T p) k (arg :: k) = arg * EvalPoly p k arg

sEvalPoly :: forall k (x :: P) (arg :: k). (SOne k, SPlus k, STimes k) => SingP x -> Sing arg -> Sing (EvalPoly x k arg) Source #

type family EvalPoly₀ (x :: P₀) k (arg :: k) :: k where ... Source #

Equations

EvalPoly₀ 'Z k (_1 :: k) = TZero k
EvalPoly₀ ('NZ p) k (arg :: k) = EvalPoly p 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) Source #