ResultKind.hs

-- | 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.
--
module Numeric.Limp.Program.ResultKind where
import Numeric.Limp.Rep


-- | Classify the result type of a linear function to either integral or real:
data K
 -- | Integral @Z@
 = KZ
 -- | Real or mixed @R@
 | KR


-- | Representation of either integral of real linear functions:
-- a list of variables with coefficients, plus a constant summand.
data Linear z r c k where
 LZ :: [(z, Z c)]          -> (Z c) -> Linear z r c KZ
 LR :: [(Either z r, R c)] -> (R c) -> Linear z r c KR


-- | 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.
type family KMerge (a :: K) (b :: K) :: K where
 KMerge KZ KZ = KZ
 KMerge KR b  = KR
 KMerge a  KR = KR

-- | Convert a @K@ to its actual representation (@Z@ or @R@).
type family KRep (a :: K) :: * -> * where
 KRep KZ = Z
 KRep KR = R