GHC.TypeLits.Normalise.SOP

SOP: Sum-of-Products, sorta

The arithmetic operation for Nat are, addition (+), subtraction (-), multiplication (*), and exponentiation (^). This means we cannot write expressions in a canonical SOP normal form. We can get rid of subtraction by working with integers, and translating a - b to a + (-1)*b. Exponentation cannot be getten rid of that way. So we define the following grammar for our canonical SOP-like normal form of arithmetic expressions:

SOP      ::= Product '+' SOP | Product
Product  ::= Symbol '*' Product | Symbol
Symbol   ::= Integer
          |  Var
          |  Var '^' Product
          |  SOP '^' ProductE

ProductE ::= SymbolE '*' ProductE | SymbolE
SymbolE  ::= Var
          |  Var '^' Product
          |  SOP '^' ProductE

So a valid SOP terms are:

x*y + y^2
(x+y)^(k*z)

, but,

(x*y)^2

is not, and should be:

x^2 * y^2

Exponents are thus not allowed to have products, so for example, the expression:

(x + 2)^(y + 2)

in valid SOP form is:

4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2

Also, exponents can only be integer values when the base is a variable. Although not enforced by the grammar, the exponentials are flatted as far as possible in SOP form. So:

(x^y)^z

is flattened to:

x^(y*z)