Integers bounded by a closed interval
stack build
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.
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
For most uses of closed, you'll only need DataKinds and maybe TypeFamilies. The other extensions below just make some of the tests concise.
{-# 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 $ doThe safe constructor closed uses Maybe to indicate failure. There is also an unsafe constructor unsafeClosed as well as a Num instance that implements fromInteger.
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` anyErrorCallUse getClosed to extract the Integer from a Closed value.
describe "elimination" $ do
it "should allow the integer value to be extracted" $ do
let result = 1 :: Bounds (Inclusive 0) (Exclusive 10)
getClosed result `shouldBe` 1The upper and lower bounds can be queried, strengthened, and weakened.
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 gets stuck at the upper and lower bounds instead of wrapping. This is called Saturation Arithmetic.
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` resultParsing of closed values is strict.
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"Closed values can be generated with QuickCheck
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)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.
This library was inspired by finite-typelits and finite-typelits-bounded. The differences are summarized below:
finite-typelits- A value ofFinite (n :: Nat)is in the half-open interval[0, n). Uses modular arithmetic.finite-typelits-bounded- A value ofFinite (n :: Nat)is in the half-open interval[0, n). Uses saturation arithmetic.closed- A value ofClosed (n :: Nat) (m :: Nat)is in the closed interval[n, m]. Uses saturation arithmetic.