diff --git a/README.lhs b/README.lhs --- a/README.lhs +++ b/README.lhs @@ -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. diff --git a/closed.cabal b/closed.cabal --- a/closed.cabal +++ b/closed.cabal @@ -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 diff --git a/library/Closed/Internal.hs b/library/Closed/Internal.hs --- a/library/Closed/Internal.hs +++ b/library/Closed/Internal.hs @@ -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 =