type-level-numbers (empty) → 0.1
raw patch · 13 files changed
+996/−0 lines, 13 filesdep +basedep +template-haskellsetup-changed
Dependencies added: base, template-haskell
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- TypeLevel/Boolean.hs +75/−0
- TypeLevel/Number/Classes.hs +169/−0
- TypeLevel/Number/Int.hs +253/−0
- TypeLevel/Number/Int/Types.hs +11/−0
- TypeLevel/Number/Nat.hs +313/−0
- TypeLevel/Number/Nat/Num.hs +26/−0
- TypeLevel/Number/Nat/TH.hs +28/−0
- TypeLevel/Number/Nat/Types.hs +12/−0
- TypeLevel/Reify.hs +23/−0
- TypeLevel/Util.hs +5/−0
- type-level-numbers.cabal +49/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) Alexey Khudyakov++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of his contributors+ may be used to endorse or promote products derived from this software+ without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE CONTRIBUTORS ``AS IS'' AND ANY EXPRESS+OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ TypeLevel/Boolean.hs view
@@ -0,0 +1,75 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE MultiParamTypeClasses #-}+module TypeLevel.Boolean ( True+ , False+ -- * Boolean operations+ , Not+ , notT+ , And+ , andT+ , Or+ , orT+ , Xor+ , xorT+ ) where++import TypeLevel.Reify++-- | Data type for truth+data True+-- | Data type for false.+data False++instance Show False where show _ = "False"+instance Show True where show _ = "True"++instance Reify True Bool where witness = Witness True+instance Reify False Bool where witness = Witness False++----------------------------------------------------------------+-- | Negation++type family Not a :: *++notT :: a -> Not a+notT _ = undefined++type instance Not False = True+type instance Not True = False++----------------------------------------------------------------+-- | And for boolean types+type family And a b :: *++andT :: a -> b -> And a b+andT _ _ = undefined++type instance And False False = False+type instance And False True = False+type instance And True False = False+type instance And True True = True++----------------------------------------------------------------+-- | Or for boolean types+type family Or a b :: *++orT :: a -> b -> Or a b+orT _ _ = undefined++type instance Or False False = True+type instance Or False True = True+type instance Or True False = True+type instance Or True True = False++----------------------------------------------------------------+-- | Exlusive or for boolean types+type family Xor a b :: *++xorT :: a -> b -> Xor a b+xorT _ _ = undefined++type instance Xor False False = False+type instance Xor False True = True+type instance Xor True False = True+type instance Xor True True = False
+ TypeLevel/Number/Classes.hs view
@@ -0,0 +1,169 @@+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# 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 _ _ = undefined++data IsLesser+data IsEqual+data IsGreater++instance Show IsLesser where show _ = "IsLesser"+instance Show IsEqual where show _ = "IsEqual"+instance Show IsGreater where show _ = "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 _ = undefined++-- | Previous number+type family Prev n :: *++prevN :: n -> Prev n+prevN _ = undefined++-- | Negate number.+type family Negate n :: *++negateN :: n -> Negate n+negateN _ = undefined++----------------------------------------------------------------++-- | Sum of two numbers.+type family Add n m :: *++addN :: n -> m -> Add n m+addN _ _ = undefined++-- | Difference of two numbers.+type family Sub n m :: *++subN :: n -> m -> Sub n m+subN _ _ = undefined++-- | Product of two numbers.+type family Mul n m :: *+ +mulN :: n -> m -> Mul n m+mulN _ _ = 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 _ _ = undefined++----------------------------------------------------------------++-- | Usually numbers have non-unique representation. This type family+-- is canonical representation of number.+type family Normalized n :: *
+ TypeLevel/Number/Int.hs view
@@ -0,0 +1,253 @@+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- |+-- Module : TypeLevel.Number.Int+-- Copyright : Alexey Khudyakov+-- License : BSD3-style (see LICENSE)+--+-- Maintainer : Alexey Khudyakov <alexey.skladnoy@gmail.com>+-- Stability : unstable+-- Portability : unportable (GHC only)+--+-- Type level signed integer numbers are implemented using balanced+-- ternary encoding much in the same way as natural numbers.+--+-- Currently following operations are supported: Next, Prev, Add, Sub,+-- Mul.+module TypeLevel.Number.Int ( -- * Integer numbers+ ZZ+ , Dn+ , D0+ , D1+ , IntT+ -- * Template haskell utilities+ , intT+ , module TypeLevel.Number.Classes+ ) where++import Language.Haskell.TH++import TypeLevel.Number.Classes+import TypeLevel.Number.Int.Types+import TypeLevel.Util+++splitToTrits :: Integer -> [Int]+splitToTrits 0 = []+splitToTrits x | n == 0 = 0 : splitToTrits rest+ | n == 1 = 1 : splitToTrits rest+ | n == 2 = -1 : splitToTrits (rest + 1)+ where+ (rest,n) = divMod x 3++-- | Generate type for integer number.+intT :: Integer -> TypeQ+intT = foldr appT [t| ZZ |] . map con . splitToTrits+ where+ con (-1) = [t| Dn |]+ con 0 = [t| D0 |]+ con 1 = [t| D1 |]+ con x = error $ "Strange trit: " ++ show x++----------------------------------------------------------------+--++-- | Type class for type level integers. Only numbers without leading+-- zeroes are members of the class.+class IntT n where+ -- | Convert natural number to integral value. It's not checked+ -- whether value could be represented.+ toInt :: Integral i => n -> i++instance IntT ZZ where toInt _ = 0+instance IntT (D1 ZZ) where toInt _ = 1+instance IntT (Dn ZZ) where toInt _ = -1++instance IntT (Dn n) => IntT (Dn (Dn n)) where toInt n = -1 + 3 * toInt' n+instance IntT (Dn n) => IntT (D0 (Dn n)) where toInt n = 0 + 3 * toInt' n+instance IntT (Dn n) => IntT (D1 (Dn n)) where toInt n = 1 + 3 * toInt' n+instance IntT (D0 n) => IntT (Dn (D0 n)) where toInt n = -1 + 3 * toInt' n+instance IntT (D0 n) => IntT (D0 (D0 n)) where toInt n = 0 + 3 * toInt' n+instance IntT (D0 n) => IntT (D1 (D0 n)) where toInt n = 1 + 3 * toInt' n+instance IntT (D1 n) => IntT (Dn (D1 n)) where toInt n = -1 + 3 * toInt' n+instance IntT (D1 n) => IntT (D0 (D1 n)) where toInt n = 0 + 3 * toInt' n+instance IntT (D1 n) => IntT (D1 (D1 n)) where toInt n = 1 + 3 * toInt' n++toInt' :: (IntT n, Integral i) => t n -> i+toInt' = toInt . cdr+++instance Show ZZ where show _ = "[0:Z]"+instance IntT (Dn n) => Show (Dn n) where show n = "["++show (toInt n)++":Z]"+instance IntT (D0 n) => Show (D0 n) where show n = "["++show (toInt n)++":Z]"+instance IntT (D1 n) => Show (D1 n) where show n = "["++show (toInt n)++":Z]"++----------------------------------------------------------------+-- Number normalization++type family AddBit n :: *+type instance AddBit ZZ = ZZ+type instance AddBit (a b) = D0 (a b)++type instance Normalized ZZ = ZZ+type instance Normalized (Dn n) = Dn (Normalized n)+type instance Normalized (D0 n) = AddBit (Normalized n)+type instance Normalized (D1 n) = D1 (Normalized n)++----------------------------------------------------------------+-- Next Number+type instance Next ZZ = D1 ZZ+type instance Next (Dn n) = Normalized (D0 n)+type instance Next (D0 n) = D1 n+type instance Next (D1 n) = Normalized (Dn (Next n))++----------------------------------------------------------------+-- Previous number+type instance Prev ZZ = Dn ZZ+type instance Prev (Dn n) = Normalized (D1 (Prev n))+type instance Prev (D0 n) = Dn n+type instance Prev (D1 n) = Normalized (D0 n)++----------------------------------------------------------------+-- Negate number+type instance Negate ZZ = ZZ+type instance Negate (Dn n) = D1 (Negate n)+type instance Negate (D0 n) = D0 (Negate n)+type instance Negate (D1 n) = Dn (Negate n)+++----------------------------------------------------------------+-- Addition++-- Type class which actually implement addtition of natural numbers+type family Add' n m carry :: *++data CarryN+data Carry0+data Carry1++-- Special cases with ZZ+type instance Add' ZZ ZZ Carry0 = ZZ+type instance Add' ZZ (Dn n) Carry0 = (Dn n)+type instance Add' ZZ (D0 n) Carry0 = (D0 n)+type instance Add' ZZ (D1 n) Carry0 = (D1 n)+type instance Add' (Dn n) ZZ Carry0 = (Dn n)+type instance Add' (D0 n) ZZ Carry0 = (D0 n)+type instance Add' (D1 n) ZZ Carry0 = (D1 n)+--+type instance Add' ZZ ZZ CarryN = Dn ZZ+type instance Add' ZZ (Dn n) CarryN = Prev (Dn n)+type instance Add' ZZ (D0 n) CarryN = (Dn n)+type instance Add' ZZ (D1 n) CarryN = (D0 n)+type instance Add' (Dn n) ZZ CarryN = Prev (Dn n)+type instance Add' (D0 n) ZZ CarryN = (Dn n)+type instance Add' (D1 n) ZZ CarryN = (D0 n)+--+type instance Add' ZZ ZZ Carry1 = D1 ZZ+type instance Add' ZZ (Dn n) Carry1 = (D0 n)+type instance Add' ZZ (D0 n) Carry1 = (D1 n)+type instance Add' ZZ (D1 n) Carry1 = Next (D1 n)+type instance Add' (Dn n) ZZ Carry1 = (D0 n)+type instance Add' (D0 n) ZZ Carry1 = (D1 n)+type instance Add' (D1 n) ZZ Carry1 = Next (D1 n)++-- == General recursion ==+-- No carry+type instance Add' (Dn n) (Dn m) Carry0 = D1 (Add' n m CarryN)+type instance Add' (D0 n) (Dn m) Carry0 = Dn (Add' n m Carry0)+type instance Add' (D1 n) (Dn m) Carry0 = D0 (Add' n m Carry0)+--+type instance Add' (Dn n) (D0 m) Carry0 = Dn (Add' n m Carry0)+type instance Add' (D0 n) (D0 m) Carry0 = D0 (Add' n m Carry0)+type instance Add' (D1 n) (D0 m) Carry0 = D1 (Add' n m Carry0)+--+type instance Add' (Dn n) (D1 m) Carry0 = D0 (Add' n m Carry0)+type instance Add' (D0 n) (D1 m) Carry0 = D1 (Add' n m Carry0)+type instance Add' (D1 n) (D1 m) Carry0 = Dn (Add' n m Carry1)+-- Carry '-'+type instance Add' (Dn n) (Dn m) CarryN = D0 (Add' n m CarryN)+type instance Add' (D0 n) (Dn m) CarryN = D1 (Add' n m CarryN)+type instance Add' (D1 n) (Dn m) CarryN = Dn (Add' n m Carry0)+--+type instance Add' (Dn n) (D0 m) CarryN = D1 (Add' n m CarryN)+type instance Add' (D0 n) (D0 m) CarryN = Dn (Add' n m Carry0)+type instance Add' (D1 n) (D0 m) CarryN = D0 (Add' n m Carry0)+--+type instance Add' (Dn n) (D1 m) CarryN = Dn (Add' n m Carry0)+type instance Add' (D0 n) (D1 m) CarryN = D0 (Add' n m Carry0)+type instance Add' (D1 n) (D1 m) CarryN = D1 (Add' n m Carry0)+-- Carry '+'+type instance Add' (Dn n) (Dn m) Carry1 = Dn (Add' n m Carry0)+type instance Add' (D0 n) (Dn m) Carry1 = D0 (Add' n m Carry0)+type instance Add' (D1 n) (Dn m) Carry1 = D1 (Add' n m Carry0)+--+type instance Add' (Dn n) (D0 m) Carry1 = D0 (Add' n m Carry0)+type instance Add' (D0 n) (D0 m) Carry1 = D1 (Add' n m Carry0)+type instance Add' (D1 n) (D0 m) Carry1 = Dn (Add' n m Carry1)+--+type instance Add' (Dn n) (D1 m) Carry1 = D1 (Add' n m Carry0)+type instance Add' (D0 n) (D1 m) Carry1 = Dn (Add' n m Carry1)+type instance Add' (D1 n) (D1 m) Carry1 = D0 (Add' n m Carry1)++-- Instances for AddN+type instance Add ZZ ZZ = ZZ+type instance Add ZZ (Dn n) = Normalized (Dn n)+type instance Add ZZ (D0 n) = Normalized (D0 n)+type instance Add ZZ (D1 n) = Normalized (D1 n)+type instance Add (Dn n) ZZ = Normalized (Dn n)+type instance Add (D0 n) ZZ = Normalized (D0 n)+type instance Add (D1 n) ZZ = Normalized (D1 n)+--+type instance Add (Dn n) (Dn m) = Normalized (Add' (Dn n) (Dn m) Carry0)+type instance Add (D0 n) (Dn m) = Normalized (Add' (D0 n) (Dn m) Carry0)+type instance Add (D1 n) (Dn m) = Normalized (Add' (D1 n) (Dn m) Carry0)+--+type instance Add (Dn n) (D0 m) = Normalized (Add' (Dn n) (D0 m) Carry0)+type instance Add (D0 n) (D0 m) = Normalized (Add' (D0 n) (D0 m) Carry0)+type instance Add (D1 n) (D0 m) = Normalized (Add' (D1 n) (D0 m) Carry0)+--+type instance Add (Dn n) (D1 m) = Normalized (Add' (Dn n) (D1 m) Carry0)+type instance Add (D0 n) (D1 m) = Normalized (Add' (D0 n) (D1 m) Carry0)+type instance Add (D1 n) (D1 m) = Normalized (Add' (D1 n) (D1 m) Carry0)+++----------------------------------------------------------------+-- Subtraction.+--+-- Subtraction is much easier since is ise defined using+-- addition and negation++type instance Sub ZZ ZZ = ZZ+type instance Sub ZZ (Dn n) = Negate (Dn n)+type instance Sub ZZ (D0 n) = Negate (D0 n)+type instance Sub ZZ (D1 n) = Negate (D1 n)+type instance Sub (Dn n) ZZ = (Dn n)+type instance Sub (D0 n) ZZ = (D0 n)+type instance Sub (D1 n) ZZ = (D1 n)++type instance Sub (Dn n) (Dn m) = Add (Dn n) (Negate (Dn m))+type instance Sub (D0 n) (Dn m) = Add (D0 n) (Negate (Dn m))+type instance Sub (D1 n) (Dn m) = Add (D1 n) (Negate (Dn m))+--+type instance Sub (Dn n) (D0 m) = Add (Dn n) (Negate (D0 m))+type instance Sub (D0 n) (D0 m) = Add (D0 n) (Negate (D0 m))+type instance Sub (D1 n) (D0 m) = Add (D1 n) (Negate (D0 m))+--+type instance Sub (Dn n) (D1 m) = Add (Dn n) (Negate (D1 m))+type instance Sub (D0 n) (D1 m) = Add (D0 n) (Negate (D1 m))+type instance Sub (D1 n) (D1 m) = Add (D1 n) (Negate (D1 m))+++----------------------------------------------------------------+-- Multiplication++type instance Mul n ZZ = ZZ+type instance Mul n (Dn m) = Normalized (Add' (Negate n) (D0 (Mul n m)) Carry0)+type instance Mul n (D0 m) = Normalized (D0 (Mul n m))+type instance Mul n (D1 m) = Normalized (Add' n (D0 (Mul n m)) Carry0)
+ TypeLevel/Number/Int/Types.hs view
@@ -0,0 +1,11 @@+{-# LANGUAGE EmptyDataDecls #-}+module TypeLevel.Number.Int.Types where+ +-- | Digit -1+data Dn n+-- | Digit 0+data D0 n+-- | Digit 1+data D1 n+-- | Digit stream terminator+data ZZ
+ TypeLevel/Number/Nat.hs view
@@ -0,0 +1,313 @@+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- |+-- Module : TypeLevel.Number.Nat+-- Copyright : Alexey Khudyakov+-- License : BSD3-style (see LICENSE)+--+-- Maintainer : Alexey Khudyakov <alexey.skladnoy@gmail.com>+-- Stability : unstable+-- Portability : unportable (GHC only)+--+--+-- This is type level natural numbers. They are represented using+-- binary encoding which means that reasonable large numbers could be+-- represented. With default context stack depth (20) maximal number+-- is 2^18-1 (262143).+--+-- > Z = 0+-- > I Z = 1+-- > O (I Z) = 2+-- > I (I Z) = 3+-- > O (O (I Z)) = 4+-- > ...+--+-- It's easy to see that representation for each number is not+-- unique. One could add any numbers of leading zeroes:+--+-- > I Z = I (O Z) = I (O (O Z)) = 1+--+-- In order to enforce uniqueness of representation only numbers+-- without leading zeroes are members of Nat type class. This means+-- than types are equal if and only if numbers are equal.+--+-- Natural numbers support comparison and following operations: Next,+-- Prev, Add, Sub, Mul. All operations on numbers return normalized+-- numbers.+--+-- Interface type classes are reexported from TypeLevel.Number.Classes+module TypeLevel.Number.Nat ( -- * Natural numbers+ I+ , O+ , Z+ , Nat(..)+ -- * Template haskell utilities+ -- $TH+ , natT+ , nat+ , module TypeLevel.Number.Classes+ ) where++import Data.Word (Word8,Word16,Word32,Word64)+import Data.Int (Int8, Int16, Int32, Int64 )+++import Language.Haskell.TH++import TypeLevel.Number.Classes+import TypeLevel.Number.Nat.Types+import TypeLevel.Number.Nat.TH+import TypeLevel.Reify++-- $TH+-- Here is usage example for natT:+--+-- > n123 :: $(natT 123)+-- > n123 = undefined++----------------------------------------------------------------++-- | Type class for natural numbers. Only numbers without leading+-- zeroes are members of this type class.+class Nat n where+ -- | Convert natural number to integral value. It's not checked+ -- whether value could be represented.+ toInt :: Integral i => n -> i++-- | Type class for positive natural numbers. It's synonym for+-- Positive and Nat.+class Pos n++instance Nat Z where toInt _ = 0+instance Nat (I Z) where toInt _ = 1+instance Nat (O n) => Nat (O (O n)) where toInt n = 0 + 2 * toInt (undefined :: (O n))+instance Nat (O n) => Nat (I (O n)) where toInt n = 1 + 2 * toInt (undefined :: (O n))+instance Nat (I n) => Nat (O (I n)) where toInt n = 0 + 2 * toInt (undefined :: (I n))+instance Nat (I n) => Nat (I (I n)) where toInt n = 1 + 2 * toInt (undefined :: (I n))+-- Error reporting. Stop for denormalized numbers+class Number_Is_Denormalized a+instance (Number_Is_Denormalized Z) => Nat (O Z) where+ toInt = error "quench warning"++-- Synonym for positive+instance (Nat n, Positive n) => Pos n+++----------------------------------------------------------------+-- Data conversion++-- To Integer+instance Reify Z Integer where witness = Witness 0+instance (Nat (O n)) => Reify (O n) Integer where witness = Witness $ toInt (undefined :: O n)+instance (Nat (I n)) => Reify (I n) Integer where witness = Witness $ toInt (undefined :: I n)++-- To Int+instance Reify Z Int where witness = Witness 0+instance (Nat (O n)) => Reify (O n) Int where witness = Witness $ toInt (undefined :: O n)+instance (Nat (I n)) => Reify (I n) Int where witness = Witness $ toInt (undefined :: I n)++-- To Word8+instance Reify Z Word8 where witness = Witness 0+instance (Nat (O n), (O n) `Lesser` $(natT 0x100)) => Reify (O n) Word8 where witness = Witness $ toInt (undefined :: O n)+instance (Nat (I n), (I n) `Lesser` $(natT 0x100)) => Reify (I n) Word8 where witness = Witness $ toInt (undefined :: I n)++-- To Word16+instance Reify Z Word16 where witness = Witness 0+instance (Nat (O n), (O n) `Lesser` $(natT 0x10000)) => Reify (O n) Word16 where witness = Witness $ toInt (undefined :: O n)+instance (Nat (I n), (I n) `Lesser` $(natT 0x10000)) => Reify (I n) Word16 where witness = Witness $ toInt (undefined :: I n)++-- To Word32 (No checks. Won't to default centext stack length)+instance Reify Z Word32 where witness = Witness 0+instance (Nat (O n)) => Reify (O n) Word32 where witness = Witness $ toInt (undefined :: O n)+instance (Nat (I n)) => Reify (I n) Word32 where witness = Witness $ toInt (undefined :: I n)++-- To Word64 (No checks. Won't to default centext stack length)+instance Reify Z Word64 where witness = Witness 0+instance (Nat (O n)) => Reify (O n) Word64 where witness = Witness $ toInt (undefined :: O n)+instance (Nat (I n)) => Reify (I n) Word64 where witness = Witness $ toInt (undefined :: I n)++-- To Int8+instance Reify Z Int8 where witness = Witness 0+instance (Nat (O n), (O n) `Lesser` $(natT 0x80)) => Reify (O n) Int8 where witness = Witness $ toInt (undefined :: O n)+instance (Nat (I n), (I n) `Lesser` $(natT 0x80)) => Reify (I n) Int8 where witness = Witness $ toInt (undefined :: I n)++-- To Int16+instance Reify Z Int16 where witness = Witness 0+instance (Nat (O n), (O n) `Lesser` $(natT 0x8000)) => Reify (O n) Int16 where witness = Witness $ toInt (undefined :: O n)+instance (Nat (I n), (I n) `Lesser` $(natT 0x8000)) => Reify (I n) Int16 where witness = Witness $ toInt (undefined :: I n)++-- To Int32 (No checks. Won't to default centext stack length)+instance Reify Z Int32 where witness = Witness 0+instance (Nat (O n)) => Reify (O n) Int32 where witness = Witness $ toInt (undefined :: O n)+instance (Nat (I n)) => Reify (I n) Int32 where witness = Witness $ toInt (undefined :: I n)++-- To Int64 (No checks. Won't to default centext stack length)+instance Reify Z Int64 where witness = Witness 0+instance (Nat (O n)) => Reify (O n) Int64 where witness = Witness $ toInt (undefined :: O n)+instance (Nat (I n)) => Reify (I n) Int64 where witness = Witness $ toInt (undefined :: I n)++----------------------------------------------------------------+-- Number normalization++-- Add trailing zero bit to number. It's added only if number is not+-- equal to zero. Actual normalization is done here.+type family Add0Bit n :: *+type instance Add0Bit Z = Z+type instance Add0Bit (a b) = (O (a b))++type instance Normalized Z = Z+type instance Normalized (I n) = I (Normalized n)+type instance Normalized (O n) = Add0Bit (Normalized n)++----------------------------------------------------------------+-- Show instances.+-- Nat contexts are used to ensure correctness of numbers.+instance Show Z where show _ = "[0:N]"+instance Nat (O n) => Show (O n) where show n = "["++show (toInt n)++":N]"+instance Nat (I n) => Show (I n) where show n = "["++show (toInt n)++":N]"++----------------------------------------------------------------+-- Next number.+-- Number normalization is not required.+type instance Next Z = I Z+type instance Next (I n) = O (Next n)+type instance Next (O n) = I n++----------------------------------------------------------------+-- Previous number.+-- Normalization isn't requred too. It's done manually in (I Z) case.+type instance Prev (I Z) = Z+type instance Prev (O (O n)) = I (Prev (O n))+type instance Prev (I (O n)) = O (O n)+type instance Prev (O (I n)) = I (Prev (I n))+type instance Prev (I (I n)) = O (I n)+++----------------------------------------------------------------+-- Comparison++-- Join compare results. a is result of comparison of low digits b is+-- result of comparion of higher digits.+type family Join a b :: *++type instance Join IsLesser IsEqual = IsLesser+type instance Join IsEqual IsEqual = IsEqual+type instance Join IsGreater IsEqual = IsGreater+type instance Join a IsLesser = IsLesser+type instance Join a IsGreater = IsGreater++-- Instances for comparison+type instance Compare Z Z = IsEqual+type instance Compare (O n) Z = IsGreater+type instance Compare (I n) Z = IsGreater+type instance Compare Z (O n) = IsLesser+type instance Compare Z (I n) = IsLesser++type instance Compare (O n) (O m) = Compare n m+type instance Compare (O n) (I m) = Join IsLesser (Compare n m)+type instance Compare (I n) (O m) = Join IsGreater (Compare n m)+type instance Compare (I n) (I m) = Compare n m++----------------------------------------------------------------+-- Positive and Non-zero numbers++instance Nat (I n) => Positive (I n)+instance Nat (O n) => Positive (O n)++instance Nat (I n) => NonZero (I n)+instance Nat (O n) => NonZero (O n)++----------------------------------------------------------------+-- Addition+data Carry -- Designate carry bit+data NoCarry -- No carry bit in addition++-- Type family which actually implement addtition of natural numbers+type family Add' n m c :: *++-- Recursion termination without carry bit. Full enumeration is+-- required to avoid overlapping instances+type instance Add' Z Z NoCarry = Z+type instance Add' (O n) Z NoCarry = O n+type instance Add' (I n) Z NoCarry = I n+type instance Add' Z (O n) NoCarry = O n+type instance Add' Z (I n) NoCarry = I n+-- Recursion termination with carry bit+type instance Add' Z Z Carry = I Z+type instance Add' (O n) Z Carry = I n+type instance Add' (I n) Z Carry = Add' (I n) (I Z) NoCarry+type instance Add' Z (O n) Carry = I n+type instance Add' Z (I n) Carry = Add' (I n) (I Z) NoCarry+-- Generic recursion (No carry)+type instance Add' (O n) (O m) NoCarry = O (Add' n m NoCarry)+type instance Add' (I n) (O m) NoCarry = I (Add' n m NoCarry)+type instance Add' (O n) (I m) NoCarry = I (Add' n m NoCarry)+type instance Add' (I n) (I m) NoCarry = O (Add' n m Carry)+-- Generic recursion (with carry)+type instance Add' (O n) (O m) Carry = I (Add' n m NoCarry)+type instance Add' (I n) (O m) Carry = O (Add' n m Carry)+type instance Add' (O n) (I m) Carry = O (Add' n m Carry)+type instance Add' (I n) (I m) Carry = I (Add' n m Carry)++-- Enumeration of all possible instances heads is required to avoid+-- overlapping.+type instance Add (O n) (O m) = Normalized (Add' (O n) (O m) NoCarry)+type instance Add (I n) (O m) = Normalized (Add' (I n) (O m) NoCarry)+type instance Add (O n) (I m) = Normalized (Add' (O n) (I m) NoCarry)+type instance Add (I n) (I m) = Normalized (Add' (I n) (I m) NoCarry)+type instance Add (O n) Z = Normalized (Add' (O n) Z NoCarry)+type instance Add (I n) Z = Normalized (Add' (I n) Z NoCarry)+type instance Add Z (O n) = Normalized (Add' Z (O n) NoCarry)+type instance Add Z (I n) = Normalized (Add' Z (I n) NoCarry)+type instance Add Z Z = Normalized (Add' Z Z NoCarry)++----------------------------------------------------------------+-- Subtraction+data Borrow -- Borrow bit+data NoBorrow -- Do not borrow bit++-- Type class which actually implement addtition of natural numbers+type family Sub' n m c :: *++-- Recursion termination without carry bit. Full enumeration is+-- required to avoid overlapping instances+type instance Sub' Z Z NoBorrow = Z+type instance Sub' (O n) Z NoBorrow = O n+type instance Sub' (I n) Z NoBorrow = I n+-- Recursion termination with carry bit+type instance Sub' (O n) Z Borrow = I (Sub' n Z Borrow)+type instance Sub' (I n) Z Borrow = O n+-- Generic recursion (No carry)+type instance Sub' (O n) (O m) NoBorrow = O (Sub' n m NoBorrow)+type instance Sub' (I n) (O m) NoBorrow = I (Sub' n m NoBorrow)+type instance Sub' (O n) (I m) NoBorrow = I (Sub' n m Borrow)+type instance Sub' (I n) (I m) NoBorrow = O (Sub' n m NoBorrow)+-- -- Generic recursion (with carry)+type instance Sub' (O n) (O m) Borrow = I (Sub' n m Borrow)+type instance Sub' (I n) (O m) Borrow = O (Sub' n m NoBorrow)+type instance Sub' (O n) (I m) Borrow = O (Sub' n m Borrow)+type instance Sub' (I n) (I m) Borrow = I (Sub' n m Borrow)++-- Enumeration of all possible instances heads is required to avoid+-- overlapping.+type instance Sub (O n) (O m) = Normalized (Sub' (O n) (O m) NoBorrow)+type instance Sub (I n) (O m) = Normalized (Sub' (I n) (O m) NoBorrow)+type instance Sub (O n) (I m) = Normalized (Sub' (O n) (I m) NoBorrow)+type instance Sub (I n) (I m) = Normalized (Sub' (I n) (I m) NoBorrow)+type instance Sub (O n) Z = Normalized (Sub' (O n) Z NoBorrow)+type instance Sub (I n) Z = Normalized (Sub' (I n) Z NoBorrow)+type instance Sub Z Z = Normalized (Sub' Z Z NoBorrow)++----------------------------------------------------------------+-- Multiplication+----------------------------------------------------------------++type instance Mul n Z = Z+type instance Mul n (O m) = Normalized (O (Mul n m))+type instance Mul n (I m) = Normalized (Add' n (O (Mul n m)) NoCarry)
+ TypeLevel/Number/Nat/Num.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE TemplateHaskell #-}+module TypeLevel.Number.Nat.Num where++import TypeLevel.Number.Nat++type N0 = $(natT 0)+type N1 = $(natT 1)+type N2 = $(natT 2)+type N3 = $(natT 3)+type N4 = $(natT 4)+type N5 = $(natT 5)+type N6 = $(natT 6)+type N7 = $(natT 7)+type N8 = $(natT 8)+type N9 = $(natT 9)++n0 :: N0; n0 = undefined+n1 :: N1; n1 = undefined+n2 :: N2; n2 = undefined+n3 :: N3; n3 = undefined+n4 :: N4; n4 = undefined+n5 :: N5; n5 = undefined+n6 :: N6; n6 = undefined+n7 :: N7; n7 = undefined+n8 :: N8; n8 = undefined+n9 :: N9; n9 = undefined
+ TypeLevel/Number/Nat/TH.hs view
@@ -0,0 +1,28 @@+{-# LANGUAGE TemplateHaskell #-}+module TypeLevel.Number.Nat.TH ( nat+ , natT+ ) where+++import Language.Haskell.TH+import TypeLevel.Number.Nat.Types++splitToBits :: Integer -> [Int]+splitToBits 0 = []+splitToBits x | odd x = 1 : splitToBits rest+ | otherwise = 0 : splitToBits rest+ where rest = x `div` 2+++-- | Create type for natural number.+natT :: Integer -> TypeQ+natT n | n >= 0 = foldr appT [t| Z |] . map con . splitToBits $ n+ | otherwise = error "natT: negative number is supplied"+ where+ con 0 = [t| O |]+ con 1 = [t| I |]+ con _ = error "natT: Strange bit nor 0 nor 1"++-- | Create value for type level natural. Value itself is undefined.+nat :: Integer -> ExpQ+nat n = sigE [|undefined|] (natT n)
+ TypeLevel/Number/Nat/Types.hs view
@@ -0,0 +1,12 @@+{-# LANGUAGE EmptyDataDecls #-}+module TypeLevel.Number.Nat.Types ( I+ , O+ , Z+ ) where++-- | One bit.+data I n+-- | Zero bit.+data O n+-- | Bit stream terminator.+data Z
+ TypeLevel/Reify.hs view
@@ -0,0 +1,23 @@+{-# LANGUAGE MultiParamTypeClasses #-}+-- |+-- Module : TypeLevel.Reify+-- Copyright : Alexey Khudyakov+-- License : BSD3-style (see LICENSE)+--+-- Maintainer : Alexey Khudyakov <alexey.skladnoy@gmail.com>+-- Stability : unstable+-- Portability : unportable (GHC only)+module TypeLevel.Reify ( Witness(..)+ , Reify(..)+ ) where+++data Witness t a = Witness { getValue :: a }+ deriving Show++-- | Convert type level into value level using +class Reify t a where+ witness :: Witness t a++ +
+ TypeLevel/Util.hs view
@@ -0,0 +1,5 @@+module TypeLevel.Util ( cdr + ) where++cdr :: t a -> a+cdr _ = undefined
+ type-level-numbers.cabal view
@@ -0,0 +1,49 @@+Name: type-level-numbers+Version: 0.1+Cabal-Version: >= 1.6+License: BSD3+License-File: LICENSE+Author: Alexey Khudyakov <alexey.skladnoy@gmail.com>+Maintainer: Alexey Khudyakov <alexey.skladnoy@gmail.com>+Homepage: +Category: Type System+Build-Type: Simple+Synopsis: + Type level numbers implemented using type families.+Description:+ This is type level numbers implemented using type families. Natural+ numbers use binary encoding. With default context stack numbers up+ to 2^18-1 coudl be represented. Signed integer numbers use balanced ternary+ encoding.+ .+ Package is structured as folows:+ .+ * [@TypeLevel.Number.Classes@] contain generic type families such as Add+ .+ * [@TypeLevel.Number.Nat@] natural numbers implemented using binary encoding+ .+ * [@TypeLevel.Number.Int@] signed integers implemented using balanced+ ternary encoding+ .+ * [@TypeLevel.Boolean@] type level booleans+ .+ So far comparison of numbers, subtraction and multiplication of+ numbers are supported.++source-repository head+ type: hg+ location: http://bitbucket.org/Shimuuar/type-numbers++Library+ Build-Depends: base >=3 && <5,+ template-haskell > 2.0+ Exposed-modules: TypeLevel.Number.Classes+ TypeLevel.Number.Nat+ TypeLevel.Number.Nat.Num+ TypeLevel.Number.Int+ TypeLevel.Boolean+ TypeLevel.Reify+ Other-modules: TypeLevel.Number.Nat.Types+ TypeLevel.Number.Nat.TH+ TypeLevel.Number.Int.Types+ TypeLevel.Util