-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Type-level numeric types and classes
--   
--   This provides numeric types meant for use at the type level with
--   -XDataKinds, along with type families that act like type-level
--   typeclasses providing various operations.
--   
--   Currently, this primarily exists in support of <a>snumber</a> and
--   <a>dependent-literals-plugin</a>, and the only type-level numeric type
--   in the current version is <tt>Integer</tt>.
@package numeric-kinds
@version 0.2.0


-- | Type-level equivalent of a subset of <a>Num</a>.
--   
--   This provides "kindclasses" (actually open type families) with
--   functionality analogous to that provided by the <a>Num</a> typeclass.
--   Since type-level typeclasses don't exist, instead we translate each
--   would-be method to its own open type family; then "instances" are
--   implemented by providing clauses for each type family "method".
--   Unfortunately this means we can't group methods into classes that must
--   be implemented all-or-none, but in practice this seems to be okay.
module Kinds.Num

-- | Type-level numeric conversion from <a>Nat</a>. Like <a>fromInteger</a>
--   in <a>Num</a>.
type family FromNat (n :: Nat) :: k

-- | Type-level conversion to <a>Integer</a>. Like <a>toInteger</a> in
--   <a>Integral</a>.
type family ToInteger (n :: k) :: Integer

-- | Type-level addition "kindclass".
type family (x :: k) + (y :: k) :: k

-- | Type-level subtraction "kindclass".
type family (x :: k) - (y :: k) :: k

-- | Type-level multiplication "kindclass".
type family (x :: k) * (y :: k) :: k


-- | Type-level <a>Integer</a>.
--   
--   Import Integer qualified as K and refer to it as K.Integer.
--   
--   It turns out this is approximately identical to an in-progress GHC
--   change <a>https://github.com/ghc-proposals/ghc-proposals/pull/154</a>,
--   right down to the particulars of how to encode kind-classes.
--   Apparently I was on the right track! TODO(awpr): when that thing is
--   merged and readily available, remove this or turn it into a compat
--   package.
--   
--   Once that proposal is complete, we can migrate by replacing K.Integer
--   with just Integer.
module Kinds.Integer

-- | Type-level signed numbers
data Integer
Pos :: Nat -> Integer
Neg :: Nat -> Integer

-- | Type-level conversion to <a>Integer</a>. Like <a>toInteger</a> in
--   <a>Integral</a>.
type family ToInteger (n :: k) :: Integer

-- | Mostly internal; the "snumber" package provides more useful
--   functionality.
class KnownInteger (n :: Integer)
integerVal :: KnownInteger n => Integer

-- | Addition of type-level integers.
type family AddInteger m n

-- | Subtraction of type-level integers.
type family SubInteger m n

-- | Comparison of type-level integers.
type family CmpInteger m n

-- | Multiplication of type-level integers.
type family MulInteger m n

-- | Given two <a>Nat</a>s <tt>m</tt> and <tt>n</tt>, computes <tt>m -
--   n</tt> as an <a>Integer</a>.
type family (m :: Nat) -# (n :: Nat)

-- | Subtracting the left summand gives back the right summand.
plusMinusInverseL :: ((m + n) -# m) :~: 'Pos n

-- | Subtracting the right summand gives back the left summand.
plusMinusInverseR :: ((m + n) -# n) :~: 'Pos m

-- | Multiplication of integers is commutative.
mulCommutes :: MulInteger m n :~: MulInteger n m
instance GHC.TypeNats.KnownNat n => Kinds.Integer.KnownInteger ('Kinds.Integer.Pos n)
instance GHC.TypeNats.KnownNat n => Kinds.Integer.KnownInteger ('Kinds.Integer.Neg n)