closed (empty) → 0.1.0
raw patch · 5 files changed
+525/−0 lines, 5 filesdep +QuickCheckdep +aesondep +base
Dependencies added: QuickCheck, aeson, base, cassava, closed, deepseq, hashable, hspec, markdown-unlit, vector
Files
- LICENSE +21/−0
- README.lhs +201/−0
- closed.cabal +57/−0
- library/Closed.hs +25/−0
- library/Closed/Internal.hs +221/−0
+ LICENSE view
@@ -0,0 +1,21 @@+The MIT License++Copyright (c) 2013-2017 Front Row Education, Inc. www.frontrowed.com++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in+all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN+THE SOFTWARE.
+ README.lhs view
@@ -0,0 +1,201 @@+# closed: Integers bounded by a closed interval++## Build++ ```plaintext+ stack build+ ```++## Tutorial++### Overview++This package exports one core data type `Closed (n :: Nat) (m :: Nat)`+for describing integers bounded by a closed interval. That is, given+`cx :: Closed n m`, `getClosed cx` is an integer `x` where `n <= x <= m`.++We also export a type family `Bounds` for describing open and half-open+intervals in terms of closed intervals.++ ```plaintext+ Bounds (Inclusive 0) (Inclusive 10) => Closed 0 10+ Bounds (Inclusive 0) (Exclusive 10) => Closed 0 9+ Bounds (Exclusive 0) (Inclusive 10) => Closed 1 10+ Bounds (Exclusive 0) (Exclusive 10) => Closed 1 9+ ```++### Preamble++ For most uses of `closed`, you'll only need `DataKinds` and maybe+ `TypeFamilies`. The other extensions below just make some of the+ tests concise.++ ```haskell+ {-# LANGUAGE TypeFamilies #-}+ {-# LANGUAGE DataKinds #-}+ {-# LANGUAGE OverloadedStrings #-}+ {-# LANGUAGE OverloadedLists #-}+ {-# LANGUAGE TypeApplications #-}+ {-# LANGUAGE ScopedTypeVariables #-}+ {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}++ module Main where++ import Closed+ import Control.Exception+ import Data.Aeson+ import qualified Data.Csv as CSV+ import Data.Vector+ import Data.Proxy+ import GHC.TypeLits+ import Test.Hspec+ import Test.Hspec.QuickCheck++ main :: IO ()+ main = hspec $ do+ ```++### Construction++ The safe constructor `closed` uses `Maybe` to indicate failure. There is+ also an unsafe constructor `unsafeClosed` as well as a `Num` instance that implements+ `fromInteger`.++ ```haskell+ describe "safe construction" $ do++ it "should successfully construct values in the specified bounds" $ do+ let result = closed 2 :: Maybe (Bounds (Inclusive 2) (Exclusive 5))+ getClosed <$> result `shouldBe` Just 2++ it "should fail to construct values outside the specified bounds" $ do+ let result = closed 1 :: Maybe (Bounds (Inclusive 2) (Exclusive 5))+ getClosed <$> result `shouldBe` Nothing++ describe "unsafe construction" $ do++ it "should successfully construct values in the specified bounds" $ do+ let result = unsafeClosed 2 :: Bounds (Inclusive 2) (Exclusive 5)+ getClosed result `shouldBe` 2++ it "should fail to construct values outside the specified bounds" $ do+ let result = unsafeClosed 1 :: Bounds (Inclusive 2) (Exclusive 5)+ evaluate (getClosed result) `shouldThrow` anyErrorCall++ describe "unsafe literal construction" $ do++ it "should successfully construct values in the specified bounds" $ do+ let result = 2 :: Bounds (Inclusive 2) (Exclusive 5)+ getClosed result `shouldBe` 2++ it "should fail to construct values outside the specified bounds" $ do+ let result = 1 :: Bounds (Inclusive 2) (Exclusive 5)+ evaluate (getClosed result) `shouldThrow` anyErrorCall+ ```++### Elimination++ Use `getClosed` to extract the `Integer` from a `Closed` value.++ ```haskell+ describe "elimination" $ do++ it "should allow the integer value to be extracted" $ do+ let result = 1 :: Bounds (Inclusive 0) (Exclusive 10)+ getClosed result `shouldBe` 1+ ```++### Bounds Manipulation++ The upper and lower bounds can be queried, strengthened, and weakened.++ ```haskell+ describe "bounds manipulation" $ do++ let cx = 4 :: Bounds (Inclusive 2) (Exclusive 10)++ it "should allow querying the bounds" $ do+ upperBound cx `shouldBe` (Proxy :: Proxy 9)+ lowerBound cx `shouldBe` (Proxy :: Proxy 2)++ it "should allow weakening the bounds" $ do+ upperBound (weakenUpper cx) `shouldBe` (Proxy :: Proxy 10)+ lowerBound (weakenLower cx) `shouldBe` (Proxy :: Proxy 1)++ it "should allow weakening the bounds by more than one" $ do+ upperBound (weakenUpper cx) `shouldBe` (Proxy :: Proxy 20)+ lowerBound (weakenLower cx) `shouldBe` (Proxy :: Proxy 0)++ it "should allow strengthening the bounds" $ do+ upperBound <$> strengthenUpper cx `shouldBe` Just (Proxy :: Proxy 8)+ lowerBound <$> strengthenLower cx `shouldBe` Just (Proxy :: Proxy 3)++ it "should allow strengthening the bounds by more than one" $ do+ upperBound <$> strengthenUpper cx `shouldBe` Just (Proxy :: Proxy 7)+ lowerBound <$> strengthenLower cx `shouldBe` Just (Proxy :: Proxy 4)+ ```++### Arithmetic++ Arithmetic gets stuck at the upper and lower bounds instead of wrapping.++ ```haskell+ describe "arithmetic" $ do++ it "addition to the maxBound should have no effect" $ do+ let result = maxBound :: Bounds (Inclusive 1) (Exclusive 10)+ result + 1 `shouldBe` result++ it "subtraction from the minBound should have no effect" $ do+ let result = minBound :: Bounds (Inclusive 1) (Exclusive 10)+ result - 1 `shouldBe` result+ ```++### Serialization++ Parsing of closed values is strict.++ ```haskell+ describe "json" $ do++ it "should successfully parse values in the specified bounds" $ do+ let result = eitherDecode "1" :: Either String (Bounds (Inclusive 1) (Exclusive 10))+ result `shouldBe` Right 1++ it "should fail to parse values outside the specified bounds" $ do+ let result = eitherDecode "0" :: Either String (Bounds (Inclusive 1) (Exclusive 10))+ result `shouldBe` Left "Error in $: parseJSON: Integer 0 is not representable in Closed 1 9"++ describe "csv" $ do++ it "should successfully parse values in the specified bounds" $ do+ let result = CSV.decode CSV.NoHeader "1" :: Either String (Vector (CSV.Only (Bounds (Inclusive 1) (Exclusive 10))))+ result `shouldBe` Right [CSV.Only 1]++ it "should fail to parse values outside the specified bounds" $ do+ let result = CSV.decode CSV.NoHeader "0" :: Either String (Vector (CSV.Only (Bounds (Inclusive 1) (Exclusive 10))))+ result `shouldBe` Left "parse error (Failed reading: conversion error: parseField: Integer 0 is not representable in Closed 1 9) at \"\""+ ```++### Testing++ Closed values can be generated with QuickCheck++ ```haskell+ describe "quickcheck" $ do++ prop "should always generate values in the specified bounds" $+ \(cx :: Closed 0 1000) ->+ natVal (lowerBound cx) <= getClosed cx &&+ getClosed cx <= natVal (upperBound cx)+ ```++## Remarks++This library was inspired by [finite-typelits](https://hackage.haskell.org/package/finite-typelits)+and [finite-typelits-bounded](https://github.com/pseudonom/finite-typelits-bounded). The differences+are summarized below:++* `finite-typelits` - A value of `Finite (n :: Nat)` is in the half-open interval `[0, n)`. Uses modular arithmetic.+* `finite-typelits-bounded` - A value of `Finite (n :: Nat)` is in the half-open interval `[0, n)`. Uses bounded arithmetic.+* `closed` - A value of `Closed (n :: Nat) (m :: Nat)` is in the closed interval `[n, m]`. Uses bounded arithmetic.
+ closed.cabal view
@@ -0,0 +1,57 @@+-- This file has been generated from package.yaml by hpack version 0.17.1.+--+-- see: https://github.com/sol/hpack++name: closed+version: 0.1.0+synopsis: Integers bounded by a closed interval+description: Integers bounded by a closed interval+category: Data+homepage: https://github.com/frontrowed/closed#readme+bug-reports: https://github.com/frontrowed/closed/issues+author: Chris Parks <chris@frontrowed.com>+maintainer: Front Row Education <engineering@frontrowed.com>+license: MIT+license-file: LICENSE+build-type: Simple+cabal-version: >= 1.10++extra-source-files:+ README.lhs++source-repository head+ type: git+ location: https://github.com/frontrowed/closed++library+ hs-source-dirs:+ library+ build-depends:+ base >= 4.9 && < 5+ , deepseq+ , aeson+ , cassava+ , hashable+ , QuickCheck+ exposed-modules:+ Closed+ Closed.Internal+ default-language: Haskell2010++test-suite readme+ type: exitcode-stdio-1.0+ main-is: README.lhs+ ghc-options: -Wall -pgmL markdown-unlit+ build-depends:+ base >= 4.9 && < 5+ , deepseq+ , aeson+ , cassava+ , hashable+ , QuickCheck+ , base+ , closed+ , hspec+ , markdown-unlit+ , vector+ default-language: Haskell2010
+ library/Closed.hs view
@@ -0,0 +1,25 @@+module Closed+ ( Endpoint(..)+ , Closed+ , Bounds+ , Single+ , FiniteNat+ , closed+ , unsafeClosed+ , getClosed+ , lowerBound+ , upperBound+ , equals+ , cmp+ , natToClosed+ , weakenUpper+ , weakenLower+ , strengthenUpper+ , strengthenLower+ , add+ , sub+ , multiply+ , isValidClosed+ ) where++import Closed.Internal
+ library/Closed/Internal.hs view
@@ -0,0 +1,221 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExplicitForAll #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}+module Closed.Internal where++import Data.Aeson+import qualified Data.Csv as CSV+import Data.Hashable+import Data.Maybe+import Data.Proxy+import Data.Ratio+import Control.DeepSeq+import Control.Monad+import GHC.Generics+import GHC.Stack+import GHC.TypeLits+import Test.QuickCheck++newtype Closed (n :: Nat) (m :: Nat)+ = Closed { getClosed :: Integer }+ deriving (Generic)++-- | Describe whether the endpoint of a 'Bounds' includes+-- or excludes its argument+data Endpoint+ -- | Endpoint includes its argument+ = Inclusive Nat+ -- | Endpoint excludes its argument+ | Exclusive Nat++-- | Syntactic sugar to express open and half-open intervals using+-- the 'Closed' type+type family Bounds (lhs :: Endpoint) (rhs :: Endpoint) :: * where+ Bounds (Inclusive n) (Inclusive m) = Closed n m+ Bounds (Inclusive n) (Exclusive m) = Closed n (m - 1)+ Bounds (Exclusive n) (Inclusive m) = Closed (n + 1) m+ Bounds (Exclusive n) (Exclusive m) = Closed (n + 1) (m - 1)++-- | Syntactic sugar to express a value that has only one non-bottom+-- inhabitant using the 'Closed' type+type Single (n :: Nat) = Bounds ('Inclusive n) ('Inclusive n)++-- | Syntactic sugar to express a value whose lower bound is zero+type FiniteNat (rhs :: Endpoint) = Bounds ('Inclusive 0) rhs++-- | Proxy for the lower bound of a 'Closed' value+lowerBound :: Closed n m -> Proxy n+lowerBound _ = Proxy++-- | Proxy for the upper bound of a 'Closed' value+upperBound :: Closed n m -> Proxy m+upperBound _ = Proxy++-- | Safely create a 'Closed' value using the specified argument+closed :: forall n m. (n <= m, KnownNat n, KnownNat m) => Integer -> Maybe (Closed n m)+closed x = result+ where+ extracted = fromJust result+ result = do+ guard $ x >= natVal (lowerBound extracted) && x <= natVal (upperBound extracted)+ pure $ Closed x++-- | Create a 'Closed' value throwing an error if the argument is not in range+unsafeClosed :: forall n m. (HasCallStack, n <= m, KnownNat n, KnownNat m) => Integer -> Closed n m+unsafeClosed x = result+ where+ result =+ if x >= natVal (lowerBound result) && x <= natVal (upperBound result)+ then Closed x+ else error $ unrepresentable x result "unsafeClosed"++-- | Test equality on 'Closed' values in the same range+instance Eq (Closed n m) where+ Closed x == Closed y = x == y++-- | Compare 'Closed' values in the same range+instance Ord (Closed n m) where+ Closed x `compare` Closed y = x `compare` y++-- | Generate the lowest and highest inhabitant of a given 'Closed' type+instance (n <= m, KnownNat n, KnownNat m) => Bounded (Closed n m) where+ maxBound = result+ where+ result = Closed (natVal (upperBound result))++ minBound = result+ where+ result = Closed (natVal (lowerBound result))++-- | Enumerate values in the range of a given 'Closed' type+instance (n <= m, KnownNat n, KnownNat m) => Enum (Closed n m) where+ fromEnum = fromEnum . getClosed+ toEnum = unsafeClosed . toEnum+ enumFrom x = enumFromTo x maxBound+ enumFromThen x y = enumFromThenTo x y (if x >= y then minBound else maxBound)++instance Show (Closed n m) where+ showsPrec d (Closed x) = showParen (d > 9) $ showString "unsafeClosed " . showsPrec 10 x++-- | Bounded arithmetic, e.g. maxBound + 1 == maxBound+instance (n <= m, KnownNat n, KnownNat m) => Num (Closed n m) where+ Closed x + Closed y = Closed $ min (x + y) (fromIntegral (maxBound :: Closed n m))+ Closed x - Closed y = Closed $ max (x - y) (fromIntegral (minBound :: Closed n m))+ Closed x * Closed y = Closed $ min (x * y) (fromIntegral (maxBound :: Closed n m))+ abs = id+ signum = const 1+ fromInteger x = result+ where+ result =+ if x >= natVal (lowerBound result) && x <= natVal (upperBound result)+ then Closed x+ else error $ unrepresentable x result "fromInteger"++instance (n <= m, KnownNat n, KnownNat m) => Real (Closed n m) where+ toRational (Closed x) = x % 1++instance (n <= m, KnownNat n, KnownNat m) => Integral (Closed n m) where+ quotRem (Closed x) (Closed y) = (Closed $ x `quot` y, Closed $ x `rem` y)+ toInteger (Closed x) = x++instance NFData (Closed n m)++instance Hashable (Closed n m)++instance ToJSON (Closed n m) where+ toEncoding = toEncoding . getClosed+ toJSON = toJSON . getClosed++instance (n <= m, KnownNat n, KnownNat m) => FromJSON (Closed n m) where+ parseJSON v = do+ x <- parseJSON v+ case closed x of+ Just cx -> pure cx+ n -> fail $ unrepresentable x (fromJust n) "parseJSON"++instance CSV.ToField (Closed n m) where+ toField = CSV.toField . getClosed++instance (n <= m, KnownNat n, KnownNat m) => CSV.FromField (Closed n m) where+ parseField s = do+ x <- CSV.parseField s+ case closed x of+ Just cx -> pure cx+ n -> fail $ unrepresentable x (fromJust n) "parseField"++instance (n <= m, KnownNat n, KnownNat m) => Arbitrary (Closed n m) where+ arbitrary =+ Closed <$> choose (natVal @n Proxy, natVal @m Proxy)++unrepresentable :: (KnownNat n, KnownNat m) => Integer -> Closed n m -> String -> String+unrepresentable x cx prefix =+ prefix ++ ": Integer " ++ show x +++ " is not representable in Closed " ++ show (natVal $ lowerBound cx) +++ " " ++ show (natVal $ upperBound cx)++-- | Convert a type-level literal into a 'Closed' value+natToClosed :: forall n m x proxy. (n <= x, x <= m, KnownNat x, KnownNat n, KnownNat m) => proxy x -> Closed n m+natToClosed p = Closed $ natVal p++-- | Add inhabitants at the end+weakenUpper :: forall k n m. (n <= m, m <= k) => Closed n m -> Closed n k+weakenUpper (Closed x) = Closed x++-- | Add inhabitants at the beginning+weakenLower :: forall k n m. (n <= m, k <= n) => Closed n m -> Closed k m+weakenLower (Closed x) = Closed x++-- | Remove inhabitants from the end. Returns 'Nothing' if the input was removed+strengthenUpper :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed n k)+strengthenUpper (Closed x) = result+ where+ result = do+ guard $ x <= natVal (upperBound $ fromJust result)+ pure $ Closed x++-- | Remove inhabitants from the beginning. Returns 'Nothing' if the input was removed+strengthenLower :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed k m)+strengthenLower (Closed x) = result+ where+ result = do+ guard $ x >= natVal (lowerBound $ fromJust result)+ pure $ Closed x++-- | Test two different types of 'Closed' values for equality.+equals :: Closed n m -> Closed o p -> Bool+equals (Closed x) (Closed y) = x == y+infix 4 `equals`++-- | Compare two different types of 'Closed' values+cmp :: Closed n m -> Closed o p -> Ordering+cmp (Closed x) (Closed y) = x `compare` y++-- | Add two different types of 'Closed' values+add :: Closed n m -> Closed o p -> Closed (n + o) (m + p)+add (Closed x) (Closed y) = Closed $ x + y++-- | Subtract two different types of 'Closed' values+-- Returns 'Left' for negative results, and 'Right' for positive results.+sub :: Closed n m -> Closed o p -> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))+sub (Closed x) (Closed y)+ | x >= y = Right $ Closed $ x - y+ | otherwise = Left $ Closed $ y - x++-- | Multiply two different types of 'Closed' values+multiply :: Closed n m -> Closed o p -> Closed (n * o) (m * p)+multiply (Closed x) (Closed y) = Closed $ x * y++-- | Verifies that a given 'Closed' value is valid.+-- Should always return 'True' unles you bring the @Closed.Internal.Closed@ constructor into scope,+-- or use 'Unsafe.Coerce.unsafeCoerce' or other nasty hacks+isValidClosed :: (KnownNat n, KnownNat m) => Closed n m -> Bool+isValidClosed cx@(Closed x) =+ natVal (lowerBound cx) <= x && x <= natVal (upperBound cx)