# 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 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 import Text.Read (readEither) 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 -- 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 @2 @4 1 evaluate (getClosed result) `shouldThrow` anyErrorCall describe "construction with clamp" $ do it "should round up to lower bound" $ do let result = clamp @2 @4 @Int 0 getClosed result `shouldBe` 2 it "should round down to upper bound" $ do let result = clamp @2 @4 @Int 6 getClosed result `shouldBe` 4 it "should accept internal value as-is" $ do let result = clamp @2 @4 @Int 3 getClosed result `shouldBe` 3 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 @9) lowerBound cx `shouldBe` (Proxy @2) 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 @20) lowerBound (weakenLower cx) `shouldBe` (Proxy @0) 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 @7) lowerBound <$> strengthenLower cx `shouldBe` Just (Proxy @4) ``` ### Arithmetic 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 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 "Read" $ do it "should successfully read values in the specified bounds" $ do let result = readEither "1" :: Either String (Bounds (Inclusive 1) (Exclusive 10)) result `shouldBe` Right 1 it "should fail to read values outside the specified bounds" $ do let result = readEither "0" :: Either String (Bounds (Inclusive 1) (Exclusive 10)) result `shouldBe` Left "Prelude.read: no parse" 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 \"\"" 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 ```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) ``` ## Release To release a new version of this library, push a commit to `main` using a conventionally-formatted commit message. - Prefix with `fix:` to release a new patch version, - Prefix with `feat:` to release a new minor version, or - Prefix with `feat!:` to release a new major version To change the "epoch" version, edit it in `package.yaml` and change the `.releaserc.yaml` tag prefix to match. ## 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 saturation arithmetic. * `closed` - A value of `Closed (n :: Nat) (m :: Nat)` is in the closed interval `[n, m]`. Uses saturation arithmetic.