closed 0.1.0 → 0.2.0

raw patch · 3 files changed

+173/−145 lines, 3 filesdep +persistentdep +textdep ~QuickCheckdep ~aesondep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: persistent, text

Dependency ranges changed: QuickCheck, aeson, base, cassava, deepseq, hashable

API changes (from Hackage documentation)

Files

• README.lhs +138/−132
• closed.cabal +19/−10
• library/Closed/Internal.hs +16/−3

@@ -1,201 +1,207 @@-# closed: Integers bounded by a closed interval+# closed +Integers bounded by a closed interval+ ## Build -  ```plaintext-  stack 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`.+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.+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-  ```+```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.+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 #-}+```haskell+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE OverloadedLists #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} -  module Main where+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+import Closed+import Control.Exception+import Data.Aeson+import Database.Persist+import Data.Proxy+import Data.Text+import Data.Vector+import GHC.TypeLits+import qualified Data.Csv as CSV+import Test.Hspec+import Test.Hspec.QuickCheck -  main :: IO ()-  main = hspec $ do-  ```+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`.+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+```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 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+    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+  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 successfully construct values in the specified bounds" $ do+      -- Note that you can use -XTypeApplications instead of type annotations+      let result = unsafeClosed @2 @4 2+      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+    it "should fail to construct values outside the specified bounds" $ do+      let result = unsafeClosed @2 @4 1+      evaluate (getClosed result) `shouldThrow` anyErrorCall -    describe "unsafe literal construction" $ do+  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 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-  ```+    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.+Use `getClosed` to extract the `Integer` from a `Closed` value. -  ```haskell-    describe "elimination" $ do+```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-  ```+    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.+The upper and lower bounds can be queried, strengthened, and weakened. -  ```haskell-    describe "bounds manipulation" $ do+```haskell+  describe "bounds manipulation" $ do -      let cx = 4 :: Bounds (Inclusive 2) (Exclusive 10)+    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 querying the bounds" $ do+      upperBound cx `shouldBe` (Proxy @9)+      lowerBound cx `shouldBe` (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" $ do+      upperBound (weakenUpper cx) `shouldBe` (Proxy @10)+      lowerBound (weakenLower cx) `shouldBe` (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 weakening the bounds by more than one" $ do+      upperBound (weakenUpper cx) `shouldBe` (Proxy @20)+      lowerBound (weakenLower cx) `shouldBe` (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" $ do+      upperBound <$> strengthenUpper cx `shouldBe` Just (Proxy @8)+      lowerBound <$> strengthenLower cx `shouldBe` Just (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)-  ```+    it "should allow strengthening the bounds by more than one" $ do+      upperBound <$> strengthenUpper cx `shouldBe` Just (Proxy @7)+      lowerBound <$> strengthenLower cx `shouldBe` Just (Proxy @4)+```  ### Arithmetic -  Arithmetic gets stuck at the upper and lower bounds instead of wrapping.+Arithmetic gets stuck at the upper and lower bounds instead of wrapping. This is called [Saturation Arithmetic](https://en.wikipedia.org/wiki/Saturation_arithmetic). -  ```haskell-    describe "arithmetic" $ do+```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 "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-  ```+    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.+Parsing of closed values is strict. -  ```haskell-    describe "json" $ do+```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 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"+    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+  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 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 \"\""-  ```+    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 \"\"" +  describe "persistent" $ do++    it "should successfully parse values in the specified bounds" $ do+      let result = fromPersistValue (PersistInt64 1) :: Either Text (Bounds (Inclusive 1) (Exclusive 10))+      result `shouldBe` Right 1++    it "should fail to parse values outside the specified bounds" $ do+      let result = fromPersistValue (PersistInt64 0) :: Either Text (Bounds (Inclusive 1) (Exclusive 10))+      result `shouldBe` Left "fromPersistValue: Integer 0 is not representable in Closed 1 9"+```+ ### Testing -  Closed values can be generated with QuickCheck+Closed values can be generated with QuickCheck -  ```haskell-    describe "quickcheck" $ do+```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)-  ```+    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:+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.+* `finite-typelits-bounded` - A value of `Finite (n :: Nat)` is in the half-open interval `[0, n)`. Uses saturation arithmetic.+* `closed` - A value of `Closed (n :: Nat) (m :: Nat)` is in the closed interval `[n, m]`. Uses saturation arithmetic.

@@ -1,9 +1,11 @@--- This file has been generated from package.yaml by hpack version 0.17.1.+-- This file has been generated from package.yaml by hpack version 0.20.0. -- -- see: https://github.com/sol/hpack+--+-- hash: e5fbf1e0d45f270ab3829a93b28d76aac53b63b7dc3ff9d76dc0c69309541594  name:           closed-version:        0.1.0+version:        0.2.0 synopsis:       Integers bounded by a closed interval description:    Integers bounded by a closed interval category:       Data@@ -27,15 +29,19 @@   hs-source-dirs:       library   build-depends:-      base >= 4.9 && < 5-    , deepseq+      QuickCheck     , aeson+    , base >=4.9 && <5     , cassava+    , deepseq     , hashable-    , QuickCheck+    , persistent+    , text   exposed-modules:       Closed       Closed.Internal+  other-modules:+      Paths_closed   default-language: Haskell2010  test-suite readme@@ -43,15 +49,18 @@   main-is: README.lhs   ghc-options: -Wall -pgmL markdown-unlit   build-depends:-      base >= 4.9 && < 5-    , deepseq+      QuickCheck     , aeson-    , cassava-    , hashable-    , QuickCheck     , base+    , cassava     , closed+    , deepseq+    , hashable     , hspec     , markdown-unlit+    , persistent+    , text     , vector+  other-modules:+      Paths_closed   default-language: Haskell2010

@@ -11,17 +11,19 @@ {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} module Closed.Internal where +import Control.DeepSeq+import Control.Monad import Data.Aeson-import qualified Data.Csv as CSV+import Database.Persist.Sql import Data.Hashable import Data.Maybe import Data.Proxy import Data.Ratio-import Control.DeepSeq-import Control.Monad+import Data.Text (pack) import GHC.Generics import GHC.Stack import GHC.TypeLits+import qualified Data.Csv as CSV import Test.QuickCheck  newtype Closed (n :: Nat) (m :: Nat)@@ -154,6 +156,17 @@ instance (n <= m, KnownNat n, KnownNat m) => Arbitrary (Closed n m) where   arbitrary =     Closed <$> choose (natVal @n Proxy, natVal @m Proxy)++instance (n <= m, KnownNat n, KnownNat m) => PersistField (Closed n m) where+  toPersistValue = toPersistValue . (fromIntegral @Integer @Int) . getClosed+  fromPersistValue value = do+    x <- fromIntegral @Int @Integer <$> fromPersistValue value+    case closed @n @m x of+      Just cx -> pure cx+      n -> Left $ pack $ unrepresentable x (fromJust n) "fromPersistValue"++instance (n <= m, KnownNat n, KnownNat m) => PersistFieldSql (Closed n m) where+  sqlType _ = sqlType (Proxy @Int)  unrepresentable :: (KnownNat n, KnownNat m) => Integer -> Closed n m -> String -> String unrepresentable x cx prefix =