Numeric.Limp.Program.Linear

Documentation

data K

The kind of a linear function: it can be integral (Z) or real (R).

Constructors

KZ

KR

data Linear z r c k where

Constructors

LZ :: [(z, Z c)] -> Z c -> Linear z r c KZ

LR :: [(Either z r, R c)] -> R c -> Linear z r c KR

type family KMerge a b :: K

The upper bound of two kinds is real, unless both are integral

Equations

KMerge KZ KZ = KZ

KMerge KR b = KR

KMerge a KR = KR

type family KRep a :: * -> *

The upper bound of two kinds is real, unless both are integral

Equations

KRep KZ = Z

KRep KR = R

toR :: Rep c => Linear z r c k -> Linear z r c KR

Any linear function can be made into a real, as it is the upper bound / top

z :: Rep c => z -> Z c -> Linear z r c KZ

Integral variable

z1 :: Rep c => z -> Linear z r c KZ

Integral variable with coefficient 1

r :: Rep c => r -> R c -> Linear z r c KR

Real variable

r1 :: Rep c => r -> Linear z r c KR

Real variable with coefficient 1

con :: Rep c => Z c -> Linear z r c KZ

An integral constant

c0 :: Rep c => Linear z r c KZ

c1 :: Rep c => Linear z r c KZ

on2 :: (b -> c) -> (a, b) -> (a, c)

neg :: Rep c => Linear z r c k -> Linear z r c k

Negate a linear function. Negation does not change the kind.

(.*) :: Rep c => Linear z r c k -> KRep k c -> Linear z r c k infix 7

(*.) :: Rep c => KRep k c -> Linear z r c k -> Linear z r c k infix 7

(.+.) :: Rep c => Linear z r c k1 -> Linear z r c k2 -> Linear z r c (KMerge k1 k2) infixl 6

(.-.) :: Rep c => Linear z r c k1 -> Linear z r c k2 -> Linear z r c (KMerge k1 k2) infixl 6

eval :: (Rep c, Ord z, Ord r) => Assignment z r c -> Linear z r c k -> KRep k c

evalR :: (Rep c, Ord z, Ord r) => Assignment z r c -> Linear z r c k -> R c