diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,1 @@ +# Changelog for modular diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright Preetham Gujjula (c) 2018 + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * 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. + + * Neither the name of Preetham Gujjula nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND 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 COPYRIGHT +OWNER 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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,3 @@ +To build the project, first install stack (https://docs.haskellstack.org/en/stable/install_and_upgrade/). Then from the project directory, run `stack build`. + +To build and view documentation, run `stack haddock --open`. diff --git a/modular.cabal b/modular.cabal new file mode 100644 --- /dev/null +++ b/modular.cabal @@ -0,0 +1,41 @@ +cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.31.0. +-- +-- see: https://github.com/sol/hpack +-- +-- hash: 8d000ad547476a8f5e3417684a4fdec07bc61d4fe40ed52bd6c63bc764dd8aec + +name: modular +version: 0.1.0.0 +synopsis: Type-safe modular arithmetic +description: Please the documentation on GitHub at +category: Math +homepage: https://github.com/pgujjula/modular#readme +bug-reports: https://github.com/pgujjula/modular/issues +author: Preetham Gujjula +maintainer: preetham.gujjula@gmail.com +copyright: 2018 Preetham Gujjula +license: BSD3 +license-file: LICENSE +build-type: Simple +extra-source-files: + README.md + ChangeLog.md + +source-repository head + type: git + location: https://github.com/pgujjula/modular + +library + exposed-modules: + Numeric.Modular + other-modules: + Paths_modular + hs-source-dirs: + src + ghc-options: -Wall + build-depends: + base >=4.7 && <5 + , ghc-typelits-knownnat >=0.5 && <1 + default-language: Haskell2010 diff --git a/src/Numeric/Modular.hs b/src/Numeric/Modular.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Modular.hs @@ -0,0 +1,114 @@ +{-| + Module : Numeric.Modular + Copyright : (c) Preetham Gujjula, 2018 + License : BSD3 + Maintainer : preetham.gujjula@gmail.com + Stability : experimental + + The @'Mod' m@ type represents a Integer modulo m, i.e., a value in ℤ/mℤ, which enables type-safe modular arithmetic. + + This library, especially the 'withMod' function, uses ideas from + /Functional Pearl: Implicit Configurations -- or, Type Classes Reflect the Values of Types/ by Oleg Kiselyov and Chung-chieh Shan, + available here: + + For example, to perform basic modular computations, + + >>> 10 :: Mod 3 + 1 + >>> 15 + 3 :: Mod 7 + 4 + + Modular reductions are performed implicitly, so modular exponentiation can be performed efficiently. + + >>> 60803790666453028877 ^ 88100461154844882932 :: Mod 39127526509442054532 + 33479467020524411041 + + Compare this to running @(60803790666453028877 ^ 88100461154844882932) \``mod`\` 39127526509442054532@, which is + much less efficient. + + The modulus can also be specified at runtime without losing any type safety or efficiency. + + >>> x = mkMod 10 + >>> y = mkMod 17 + >>> withMod 3 (x + y) + 0 + >>> withMod 10 (x + y) + 7 + >>> a = mkMod 60803790666453028877 + >>> b = 88100461154844882932 :: Integer + >>> m = 39127526509442054532 :: Integer + >>> withMod m $ a^b + 33479467020524411041 +-} + +{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, GADTs, Rank2Types, ScopedTypeVariables #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} + +module Numeric.Modular + ( Mod + , mkMod + , withMod + ) where + +import Data.Proxy (Proxy(..)) +import GHC.TypeLits (Nat, KnownNat, type (*), type (+), natVal) + +{-| + Data type to represent an integer modulo `n`. +-} +data Mod (n :: Nat) = Mod Integer + +{-| @mkMod n@ wraps @n@ in type @'Mod' m@. -} +mkMod :: forall m. (KnownNat m) => Integer -> Mod m +mkMod n = Mod (n `mod` (natVal (Proxy :: Proxy m))) + +{-| + In @withMod m a@ + + * @m@ is the modulus. + * @a@ is a polymorphic value that can take on the type @'Mod' m@ for any @a@. + * @withMod m a@ equals @a@ interpreted modulo @m@. + + > x = mkMod 17 + > withMod 5 x == 2 +-} +withMod :: Integer -> (forall m. (KnownNat m) => Mod m) -> Integer +withMod k m = reifyInteger k (withModProxy m) + +{- Given a polymorphic modular value and a proxy for the modulus Nat, resolve the modular value + using the given modulus. +-} +withModProxy :: forall m. KnownNat m => (forall n. (KnownNat n) => Mod n) -> Proxy m -> Integer +withModProxy k modProxy = (getV (k :: Mod m)) `mod` (natVal modProxy) + +{- Get the modulus m as a integer of a value of type Mod m. -} +getM :: forall m. (KnownNat m) => Mod m -> Integer +getM _ = natVal (Proxy :: Proxy m) + +{- Get the Integer inside a value of type Mod m. -} +getV :: forall m. (KnownNat m) => Mod m -> Integer +getV (Mod k) = k + +{- The implementation of "reifyIntegral" from the Implicit Configurations paper adapted + to the current context. +-} +reifyInteger :: Integer -> (forall n. (KnownNat n) => Proxy n -> w) -> w +reifyInteger 0 f = f (Proxy :: Proxy 0) +reifyInteger n f + | even n = reifyInteger (n `div` 2) (\(Proxy :: Proxy n) -> f (Proxy :: Proxy (n * 2))) + | otherwise = reifyInteger (n - 1) (\(Proxy :: Proxy n) -> f (Proxy :: Proxy (n + 1))) + +instance Eq (Mod m) where + (==) (Mod a) (Mod b) = a == b + +instance (KnownNat m) => Show (Mod m) where + show (Mod a) = show a + +instance (KnownNat m) => Num (Mod m) where + (+) k@(Mod a) (Mod b) = Mod $ (a + b) `mod` (getM k) + (*) k@(Mod a) (Mod b) = Mod $ (a * b) `mod` (getM k) + (-) k@(Mod a) (Mod b) = Mod $ (a - b) `mod` (getM k) + negate k@(Mod a) = Mod $ (negate a) `mod` (getM k) + abs = id + signum _ = 1 + fromInteger = mkMod