diff --git a/LICENSE.md b/LICENSE.md new file mode 100644 --- /dev/null +++ b/LICENSE.md @@ -0,0 +1,201 @@ +Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "{}" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright 2014 Janos Tapolczai + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/Numeric/Peano.hs b/Numeric/Peano.hs new file mode 100644 --- /dev/null +++ b/Numeric/Peano.hs @@ -0,0 +1,193 @@ +-- Value-level Peano arithmetic. +module Numeric.Peano where + +import Data.Ratio ((%)) + +-- |Lazy Peano numbers. Allow calculation with infinite values. +data Nat = Z | S Nat deriving (Show) + +-- |Sign for whole numbers. +data Sign = Pos | Neg deriving (Show, Eq, Ord, Enum, Read, Bounded) + +-- |Whole numbers (Z). +data Whole = Whole Nat Sign + +-- |The class of Peano-like constructions (i.e. Nat and Whole). +class Enum a => Peano a where + -- |Test for zero. + isZero :: a -> Bool + -- |An unobservable infinity. + infinity :: a + -- |Converts the number to an Integer. + fromPeano :: a -> Integer + -- |Reduces the absolute value of the number by 1. If @isZero n@, then + -- @decr n = n@. + decr :: a -> a + +-- |Negation of 'isZero'. +isSucc :: Peano n => n -> Bool +isSucc = not . isZero + +instance Peano Nat where + isZero Z = True + isZero _ = False + infinity = S infinity + fromPeano Z = 0 + fromPeano (S n) = succ $ fromPeano n + decr = pred + +instance Peano Whole where + isZero (Whole n _) = isZero n + infinity = Whole infinity Pos + fromPeano (Whole n Pos) = fromPeano n + fromPeano (Whole n Neg) = negate $ fromPeano n + decr (Whole n s) = Whole (pred n) s + +-- |Removes at most 'S' constructors from a Peano number. +-- Outputs the number of removed constructors and the remaining number. +takeNat :: (Num a, Enum a, Ord a, Peano n) => a -> n -> (a, n) +takeNat = takeNat' 0 + where + takeNat' c i n | i <= 0 = (c, n) + | isZero n = (c, n) + | otherwise = takeNat' (succ c) (pred i) (decr n) + + +-- |Bounded-instance for 'Nat'. The lower bound is zero, the upper bound +-- is infinity. +instance Bounded Nat where + minBound = Z + maxBound = infinity + +-- |Bounded-instance for 'Nat'. The bounds are negative and positive infinity. +instance Bounded Whole where + minBound = Whole infinity Neg + maxBound = infinity + +-- |Enum-instance for 'Nat'. The 'pred' function is bounded at Zero. +instance Enum Nat where + toEnum = fromInteger . fromIntegral + fromEnum = fromInteger . fromPeano + succ = S + pred Z = Z + pred (S n) = n + +-- |Enum-instance for 'Whole'. 'succ' and 'pred' work according to the total +-- order on the whole numbers, i.e. @succ n = n+1@ and @pred n = n-1@. +instance Enum Whole where + toEnum i | i < 0 = Whole (toEnum i) Neg + | otherwise = Whole (toEnum i) Pos + fromEnum = fromInteger . fromPeano + succ (Whole (S n) Neg) = Whole n Neg + succ (Whole n Pos) = Whole (S n) Pos + succ (Whole Z _) = Whole (S Z) Pos + pred (Whole (S n) Pos) = Whole n Pos + pred (Whole n Neg) = Whole (S n) Neg + pred (Whole Z _) = Whole (S Z) Neg + +-- |Num-instance for 'Nat'. Addition, multiplication, and subtraction are +-- lazy in both arguments, meaning that, in the case of infinite values, +-- they can produce an infinite stream of S-constructors. As long as +-- the callers of these functions only consume a finite amount of these, +-- the program will not hang. +-- +-- @fromInteger@ is not injective in case of 'Nat', since negative integers +-- are all converted to Z. +instance Num Nat where + (+) Z n = n + (+) n Z = n + (+) (S n) (S m) = S $ S $ (+) n m + + (*) Z n = Z + (*) n Z = Z + (*) (S n) (S m) = S Z + n + m + (n * m) + + abs = id + + signum _ = S Z + + fromInteger i | i <= 0 = Z + | otherwise = S $ fromInteger $ i - 1 + + (-) Z n = Z + (-) n Z = n + (-) (S n) (S m) = n - m + +instance Num Whole where + (+) (Whole n Pos) (Whole m Pos) = Whole (n+m) Pos + (+) (Whole n Neg) (Whole m Neg) = Whole (n+m) Neg + (+) (Whole n Pos) (Whole m Neg) | n >= m = Whole (n-m) Pos + | otherwise = Whole (m-n) Neg + (+) (Whole n Neg) (Whole m Pos) = Whole m Pos + Whole n Neg + + (*) (Whole n s) (Whole m t) | s == t = Whole (n*m) Pos + | otherwise = Whole (n*m) Neg + + (-) n (Whole m Neg) = n + (Whole m Pos) + (-) n (Whole m Pos) = n + (Whole m Neg) + + abs (Whole n s) = Whole n Pos + + signum (Whole Z _) = Whole Z Pos + signum (Whole _ Pos) = Whole (S Z) Pos + signum (Whole _ Neg) = Whole (S Z) Neg + + fromInteger i | i < 0 = Whole (fromInteger $ negate i) Neg + | otherwise = Whole (fromInteger i) Pos + + +-- |Eq-instance for 'Nat'. '==' and '/=' work as long as at least one operand +-- is finite. +instance Eq Nat where + (==) Z Z = True + (==) Z (S _) = False + (==) (S _) Z = False + (==) (S n) (S m) = n == m + +-- |Eq-instance for 'Whole'. Positive and negative zero are considered equal. +instance Eq Whole where + (==) (Whole Z _) (Whole Z _) = True + (==) (Whole n s) (Whole m t) = s == t && n == m + +-- |Ord-instance for 'Nat'. All methods work as long as at least one operand +-- is finite. +instance Ord Nat where + compare Z Z = EQ + compare Z (S _) = LT + compare (S _) Z = GT + compare (S n) (S m) = compare n m + +instance Ord Whole where + compare (Whole Z _) (Whole Z _) = EQ + compare (Whole _ Neg) (Whole _ Pos) = LT + compare (Whole _ Pos) (Whole _ Neg) = GT + compare (Whole n Pos) (Whole m Pos) = compare n m + compare (Whole n Neg) (Whole m Neg) = compare m n + +-- |Returns the length of a list as Nat. Can handle infinite lists, provided +-- that a finite lower bound is checked. +natLength :: [a] -> Nat +natLength [] = Z +natLength (_:xs) = S $ natLength xs + +-- |Real-instance for 'Nat'. Since 'toRational' returns a @Ratio Integer@, +-- it WILL NOT terminate on infinities. +instance Real Nat where + toRational = flip (%) 1 . fromPeano + +-- |Integral-instance for 'Nat'. Since negative numbers are not allowed, +-- @quot = div@ and @rem = mod@. The methods @quot@, @rem@, @div@, @mod@, +-- @quotRem@ and @divMod@ will return as long as their first argument is +-- finite. Infinities are handled as follows: +-- @ +-- n `quot` infinity = n `div` infinity = 0 +-- n `rem` infinity = n `mod` infinity = n@ +instance Integral Nat where + quotRem _ Z = error "divide by zero" + quotRem n (S m) = quotRem' Z n (S m) + where + quotRem' q n m | n >= m = quotRem' (S q) (n-m) m + | otherwise = (q,n) + + divMod = quotRem + toInteger = fromPeano diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,9 @@ +numericpeano +============ + +Peano numbers with the expected bells and whistles. The implementation is naive (the memory footprint of a number n is O(n) bytes). + +Features: +* lazy evaluation, i.e. compatibility with infinity, +* positive as well as negative numbers (N and Z), +* instances for the usual typeclasses: Enum, Bounded, Num, Integral, etc. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/numericpeano.cabal b/numericpeano.cabal new file mode 100644 --- /dev/null +++ b/numericpeano.cabal @@ -0,0 +1,35 @@ +-- Initial numericpeano.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +name: numericpeano +version: 0.1.0.0 +synopsis: Peano numbers with attendant bells and whistles. +description: Value-level lazy Peano numbers for all your proof-theoretic + and infinity-related needs. The features are: + + 1) natural and integral numbers (N and Z); + 2) lazy infinities; and + 3) instances for all relevant typeclasses, meaning that + Peano arithmetic can be used in generic functions without + extra hassle. + + The implementation is naive, meaning that a number of + magnitude n may consume O(n) bytes of memory. +homepage: https://github.com/ombocomp/numericpeano/ +license: Apache-2.0 +license-file: LICENSE.md +author: Janos Tapolczai +maintainer: janos.tapolczai@gmail.com +-- copyright: +category: Math +build-type: Simple +extra-source-files: README.md +cabal-version: >=1.10 + +library + exposed-modules: Numeric.Peano + -- other-modules: + -- other-extensions: + build-depends: base >=4.7 && <4.8 + -- hs-source-dirs: + default-language: Haskell2010