Numeric.Limp.Program.ResultKind

Type-level functions on result types.

Linear functions are classified as either int-valued or real-valued, so we define KZ and KR as data kinds to denote this in the type.

Documentation

data K

Classify the result type of a linear function to either integral or real:

Constructors

KZ

Integral Z

KR

Real or mixed R

data Linear z r c k where

Representation of either integral of real linear functions: a list of variables with coefficients, plus a constant summand.

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

Instances

(Show z, Show r, Show (Z c), Show (R c)) => Show (Linear z r c k)

type family KMerge a b :: K

Find the result type of merging, or adding, two linear functions: adding two integers produces an integer, while adding a real on either side produces a real.

Equations

KMerge KZ KZ = KZ

KMerge KR b = KR

KMerge a KR = KR

type family KRep a :: * -> *

Convert a K to its actual representation (Z or R).

Equations

KRep KZ = Z

KRep KR = R