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
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 "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)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.