{-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -- | -- Module : TypeLevel.Number.Classes -- Copyright : Alexey Khudyakov -- License : BSD3-style (see LICENSE) -- -- Maintainer : Alexey Khudyakov <alexey.skladnoy@gmail.com> -- Stability : unstable -- Portability : unportable (GHC only) -- -- This module contain interface type classes for operations with type -- level numbers. module TypeLevel.Number.Classes ( -- * Comparison of numbers Compare , compareN -- ** Data labels for types comparison , IsLesser , IsEqual , IsGreater -- ** Specialized type classes -- $comparing , Lesser , LesserEq , Greater , GreaterEq -- ** Special traits , Positive , NonZero -- * Arithmetic operations on numbers , Next , nextN , Prev , prevN , Negate , negateN , Add , addN , Sub , subN , Mul , mulN , Div , divN -- * Special classes , Normalized ) where ---------------------------------------------------------------- -- Comparison ---------------------------------------------------------------- -- | Type family for comparing two numbers. It's expected that for any -- two valid 'n' and 'm' 'Compare n m' is equal to IsLess when 'n<m', IsEqual -- when 'n=m' and IsGreater when 'n>m'. type family Compare n m :: * compareN :: n -> m -> Compare n m compareN :: n -> m -> Compare n m compareN n _ m _ = Compare n m forall a. HasCallStack => a undefined data IsLesser data IsEqual data IsGreater instance Show IsLesser where show :: IsLesser -> String show IsLesser _ = String "IsLesser" instance Show IsEqual where show :: IsEqual -> String show IsEqual _ = String "IsEqual" instance Show IsGreater where show :: IsGreater -> String show IsGreater _ = String "IsGreater" ---------------------------------------------------------------- -- $comparing -- These type classes are meant to be used in contexts to ensure -- relations between numbers. For example: -- -- > someFunction :: Lesser n m => Data n -> Data m -> Data n -- > someFunction = ... -- -- They have generic instances and every number which is instance of -- Compare type family is instance of these type classes. -- -- These instance could have problems. They weren't exensively tested. -- Also error messages are really unhelpful. -- | Numbers n and m are instances of this class if and only is n < m. class Lesser n m -- | Numbers n and m are instances of this class if and only is n > m. class Greater n m -- | Numbers n and m are instances of this class if and only is n <= m. class LesserEq n m -- | Numbers n and m are instances of this class if and only is n >= m. class GreaterEq n m -- a b c are instance of class only when a ~ b or a ~ c. Require ovelapping. class OneOfTwo a b c instance OneOfTwo a a b instance OneOfTwo a b a instance OneOfTwo a a a instance (Compare n m ~ IsLesser ) => Lesser n m instance (Compare n m ~ IsGreater) => Greater n m -- Instances for LessEq and GreaterEq are trickier. instance (OneOfTwo (Compare n m) IsLesser IsEqual) => LesserEq n m instance (OneOfTwo (Compare n m) IsGreater IsEqual) => GreaterEq n m -- | Non-zero number. For naturals it's same as positive class NonZero n -- | Positive number. class Positive n ---------------------------------------------------------------- -- | Next number. type family Next n :: * nextN :: n -> Next n nextN :: n -> Next n nextN n _ = Next n forall a. HasCallStack => a undefined -- | Previous number type family Prev n :: * prevN :: n -> Prev n prevN :: n -> Prev n prevN n _ = Prev n forall a. HasCallStack => a undefined -- | Negate number. type family Negate n :: * negateN :: n -> Negate n negateN :: n -> Negate n negateN n _ = Negate n forall a. HasCallStack => a undefined ---------------------------------------------------------------- -- | Sum of two numbers. type family Add n m :: * addN :: n -> m -> Add n m addN :: n -> m -> Add n m addN n _ m _ = Add n m forall a. HasCallStack => a undefined -- | Difference of two numbers. type family Sub n m :: * subN :: n -> m -> Sub n m subN :: n -> m -> Sub n m subN n _ m _ = Sub n m forall a. HasCallStack => a undefined -- | Product of two numbers. type family Mul n m :: * mulN :: n -> m -> Mul n m mulN :: n -> m -> Mul n m mulN n _ m _ = Mul n m forall a. HasCallStack => a undefined -- | Division of two numbers. 'n' and 'm' should be instances of this -- class only if remainder of 'n/m' is zero. type family Div n m :: * divN :: n -> m -> Div n m divN :: n -> m -> Div n m divN n _ m _ = Div n m forall a. HasCallStack => a undefined ---------------------------------------------------------------- -- | Usually numbers have non-unique representation. This type family -- is canonical representation of number. type family Normalized n :: *