closed

KO | EN

gitlite — search

#javascript #python #react #typescript #golang #go #rust #docker #macos #java #cli #security #ios #open-source

(★ 14)

Integers bounded by a closed interval

closed Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

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

closed

closed Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

closed

closed Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README