closed

Integers bounded by a closed interval

Monthly Downloads: 21

Programming language: Haskell

License: MIT License

Tags: Data    

Latest version: v0.2.0

README

closed

Integers bounded by a closed interval

Build

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.

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.

{-# 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 $ 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.

  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.

  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.

  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.

  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.

  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

  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)

Remarks

This library was inspired by finite-typelits and 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.