finite-typelits (empty) → 0.1.0.0
raw patch · 5 files changed
+305/−0 lines, 5 filesdep +basesetup-changed
Dependencies added: base
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- finite-typelits.cabal +18/−0
- src/Data/Finite.hs +232/−0
- src/Data/Finite/Internal.hs +23/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2015, mniip++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 mniip 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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ finite-typelits.cabal view
@@ -0,0 +1,18 @@+name: finite-typelits+version: 0.1.0.0+synopsis: A type inhabited by finitely many values, indexed by type-level naturals.+description: A type inhabited by finitely many values, indexed by type-level naturals.+homepage: https://github.com/mniip/finite-typelits+license: BSD3+license-file: LICENSE+author: mniip+maintainer: mniip@mniip.com+category: Data+build-type: Simple+cabal-version: >=1.10++library+ exposed-modules: Data.Finite, Data.Finite.Internal+ build-depends: base == 4.*+ hs-source-dirs: src+ default-language: Haskell2010
+ src/Data/Finite.hs view
@@ -0,0 +1,232 @@+--------------------------------------------------------------------------------+-- |+-- Module : Data.Finite+-- Copyright : (C) 2015 mniip+-- License : BSD3+-- Maintainer : mniip <mniip@mniip.com>+-- Stability : experimental+-- Portability : portable+--------------------------------------------------------------------------------+{-# LANGUAGE TypeOperators, DataKinds, TypeFamilies, FlexibleContexts #-}+module Data.Finite+ (+ Finite,+ packFinite, packFiniteProxy,+ finite, finiteProxy,+ getFinite,+ equals, cmp,+ natToFinite,+ weaken, strengthen, shift, unshift,+ weakenN, strengthenN, shiftN, unshiftN,+ weakenProxy, strengthenProxy, shiftProxy, unshiftProxy,+ add, sub, multiply,+ combineSum, combineProduct,+ separateSum, separateProduct,+ isValidFinite+ )+ where++import Data.Maybe+import Data.Ratio+import GHC.TypeLits++import Data.Finite.Internal (Finite(Finite))++-- | Convert an 'Integer' into a 'Finite', returning 'Nothing' if the input is out of bounds.+packFinite :: KnownNat n => Integer -> Maybe (Finite n)+packFinite x = result+ where+ result = if x < natVal (fromJust result) && x >= 0+ then Just $ Finite x+ else Nothing++-- | Same as 'packFinite' but with a proxy argument to avoid type signatures.+packFiniteProxy :: KnownNat n => proxy n -> Integer -> Maybe (Finite n)+packFiniteProxy _ = packFinite++-- | Convert an 'Integer' into a 'Finite', throwing an error if the input is out of bounds.+finite :: KnownNat n => Integer -> Finite n+finite x = result+ where+ result = if x < natVal result && x >= 0+ then Finite x+ else error $ "finite: Integer " ++ show x ++ " is not representable in Finite " ++ show (natVal result)++-- | Same as 'finite' but with a proxy argument to avoid type signatures.+finiteProxy :: KnownNat n => proxy n -> Integer -> Finite n+finiteProxy _ = finite++-- | Convert a 'Finite' into the corresponding 'Integer'.+getFinite :: Finite n -> Integer+getFinite (Finite x) = x++instance Eq (Finite n) where+ Finite x == Finite y = x == y++-- | Test two different types of finite numbers for equality.+equals :: Finite n -> Finite m -> Bool+equals (Finite x) (Finite y) = x == y+infix 4 `equals`++instance Ord (Finite n) where+ Finite x `compare` Finite y = x `compare` y++-- | Compare two different types of finite numbers.+cmp :: Finite n -> Finite m -> Ordering+cmp (Finite x) (Finite y) = x `compare` y++-- | Throws an error for @'Finite' 0@+instance KnownNat n => Bounded (Finite n) where+ maxBound = result+ where+ result = if natVal result > 0+ then Finite $ natVal result - 1+ else error "maxBound: Finite 0 is uninhabited"+ minBound = result+ where+ result = if natVal result > 0+ then Finite 0+ else error "minBound: Finite 0 is uninhabited"++instance KnownNat n => Enum (Finite n) where+ fromEnum = fromEnum . getFinite+ toEnum = finite . toEnum+ enumFrom x = enumFromTo x maxBound+ enumFromThen x y = enumFromThenTo x y (if x >= y then minBound else maxBound)++instance Show (Finite n) where+ showsPrec d (Finite x) = showParen (d > 9) $ showString "finite " . showsPrec 10 x++-- | Modulo arithmetic. Only the 'fromInteger' function is supposed to be useful.+instance KnownNat n => Num (Finite n) where+ fx@(Finite x) + Finite y = Finite $ (x + y) `mod` natVal fx+ fx@(Finite x) - Finite y = Finite $ (x - y) `mod` natVal fx+ fx@(Finite x) * Finite y = Finite $ (x * y) `mod` natVal fx+ abs fx = fx+ signum _ = fromInteger 1+ fromInteger x = result+ where+ result = if x < natVal result && x >= 0+ then Finite x+ else error $ "fromInteger: Integer " ++ show x ++ " is not representable in Finite " ++ show (natVal result)++instance KnownNat n => Real (Finite n) where+ toRational (Finite x) = x % 1++instance KnownNat n => Integral (Finite n) where+ quotRem (Finite x) (Finite y) = (Finite $ x `quot` y, Finite $ x `rem` y)+ toInteger (Finite x) = x++-- | Convert a type-level literal into a 'Finite'.+natToFinite :: (KnownNat n, KnownNat m, n + 1 <= m) => proxy n -> Finite m+natToFinite p = Finite $ natVal p++-- | Add one inhabitant in the end.+weaken :: Finite n -> Finite (n + 1)+weaken (Finite x) = Finite x++-- | Remove one inhabitant from the end. Returns 'Nothing' if the input was the removed inhabitant.+strengthen :: KnownNat n => Finite (n + 1) -> Maybe (Finite n)+strengthen (Finite x) = result+ where+ result = if x < natVal (fromJust result)+ then Just $ Finite x+ else Nothing++-- | Add one inhabitant in the beginning, shifting everything up by one.+shift :: Finite n -> Finite (n + 1)+shift (Finite x) = Finite (x + 1)++-- | Remove one inhabitant from the beginning, shifting everything down by one. Returns 'Nothing' if the input was the removed inhabitant.+unshift :: Finite (n + 1) -> Maybe (Finite n)+unshift (Finite x) = if x < 1+ then Nothing+ else Just $ Finite $ x - 1++-- | Add multiple inhabitants in the end.+weakenN :: (n <= m) => Finite n -> Finite m+weakenN (Finite x) = Finite x++-- | Remove multiple inhabitants from the end. Returns 'Nothing' if the input was one of the removed inhabitants.+strengthenN :: (KnownNat n, n <= m) => Finite m -> Maybe (Finite n)+strengthenN (Finite x) = result+ where+ result = if x < natVal (fromJust result)+ then Just $ Finite x+ else Nothing++-- | Add multiple inhabitant in the beginning, shifting everything up by the amount of inhabitants added.+shiftN :: (KnownNat n, KnownNat m, n <= m) => Finite n -> Finite m+shiftN fx@(Finite x) = result+ where+ result = Finite $ x + natVal result - natVal fx++-- | Remove multiple inhabitants from the beginning, shifting everything down by the amount of inhabitants removed. Returns 'Nothing' if the input was one of the removed inhabitants.+unshiftN :: (KnownNat n, KnownNat m, n <= m) => Finite m -> Maybe (Finite n)+unshiftN fx@(Finite x) = result+ where+ result = if x < natVal fx - natVal (fromJust result)+ then Nothing+ else Just $ Finite $ x - natVal fx + natVal (fromJust result)++weakenProxy :: proxy k -> Finite n -> Finite (n + k)+weakenProxy _ (Finite x) = Finite x++strengthenProxy :: KnownNat n => proxy k -> Finite (n + k) -> Maybe (Finite n)+strengthenProxy p (Finite x) = result+ where+ result = if x < natVal (fromJust result)+ then Just $ Finite x+ else Nothing++shiftProxy :: KnownNat k => proxy k -> Finite n -> Finite (n + k)+shiftProxy p (Finite x) = Finite $ x + natVal p++unshiftProxy :: KnownNat k => proxy k -> Finite (n + k) -> Maybe (Finite n)+unshiftProxy p (Finite x) = if x < natVal p+ then Nothing+ else Just $ Finite $ x - natVal p++-- | Add two 'Finite's.+add :: Finite n -> Finite m -> Finite (n + m)+add (Finite x) (Finite y) = Finite $ x + y++-- | Subtract two 'Finite's. Returns 'Left' for negative results, and 'Right' for positive results. Note that this function never returns @'Left' 0@.+sub :: Finite n -> Finite m -> Either (Finite m) (Finite n)+sub (Finite x) (Finite y) = if x >= y+ then Right $ Finite $ x - y+ else Left $ Finite $ y - x++-- | Multiply two 'Finite's.+multiply :: Finite n -> Finite m -> Finite (n * m)+multiply (Finite x) (Finite y) = Finite $ x * y++getLeftType :: Either a b -> a+getLeftType = error "getLeftType"++-- | 'Left'-biased (left values come first) disjoint union of finite sets.+combineSum :: KnownNat n => Either (Finite n) (Finite m) -> Finite (n + m)+combineSum (Left (Finite x)) = Finite x+combineSum efx@(Right (Finite x)) = Finite $ x + natVal (getLeftType efx)++-- | 'fst'-biased (fst is the inner, and snd is the outer iteratee) product of finite sets.+combineProduct :: KnownNat n => (Finite n, Finite m) -> Finite (n * m)+combineProduct (fx@(Finite x), Finite y) = Finite $ x + y * natVal fx++-- | Take a 'Left'-biased disjoint union apart.+separateSum :: KnownNat n => Finite (n + m) -> Either (Finite n) (Finite m)+separateSum (Finite x) = result+ where+ result = if x >= natVal (getLeftType result)+ then Right $ Finite $ x - natVal (getLeftType result)+ else Left $ Finite x++-- | Take a 'fst'-biased product apart.+separateProduct :: KnownNat n => Finite (n * m) -> (Finite n, Finite m)+separateProduct (Finite x) = result+ where+ result = (Finite $ x `mod` natVal (fst result), Finite $ x `div` natVal (fst result))++-- | Verifies that a given 'Finite' is valid. Should always return 'True' unles you bring the @Data.Finite.Internal.Finite@ constructor into the scope, or use 'Unsafe.Coerce.unsafeCoerce' or other nasty hacks+isValidFinite :: KnownNat n => Finite n -> Bool+isValidFinite fx@(Finite x) = x < natVal fx && x >= 0
+ src/Data/Finite/Internal.hs view
@@ -0,0 +1,23 @@+--------------------------------------------------------------------------------+-- |+-- Module : Data.Finite.Internal+-- Copyright : (C) 2015 mniip+-- License : BSD3+-- Maintainer : mniip <mniip@mniip.com>+-- Stability : experimental+-- Portability : portable+--------------------------------------------------------------------------------+{-# LANGUAGE KindSignatures, DataKinds #-}+module Data.Finite.Internal+ (+ Finite(Finite)+ )+ where++import GHC.TypeLits++-- | Finite number type. @'Finite' n@ is inhabited by exactly @n@ values. Invariants:+--+-- prop> getFinite x < natVal x+-- prop> getFinite x >= 0+newtype Finite (n :: Nat) = Finite Integer