closed 0.2.0.3 → 0.2.1.0

raw patch · 4 files changed

+119/−56 lines, 4 filesdep +randomPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: random

API changes (from Hackage documentation)

Files

• README.lhs +11/−0
• closed.cabal +2/−1
• library/Closed.hs +1/−1
• library/Closed/Internal.hs +105/−54

@@ -49,6 +49,7 @@ import qualified Data.Csv as CSV import Test.Hspec import Test.Hspec.QuickCheck+import Text.Read (readEither)  main :: IO () main = hspec $ do@@ -167,6 +168,16 @@ 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

@@ -1,6 +1,6 @@ cabal-version:      1.12 name:               closed-version:            0.2.0.3+version:            0.2.1.0 license:            MIT license-file:       LICENSE maintainer:         Freckle Education <engineering@freckle.com>@@ -35,6 +35,7 @@         deepseq >=1.4.3.0,         hashable >=1.2.7.0,         persistent >=2.8.2,+        random >=1.1,         text >=1.2.3.1  test-suite readme

@@ -1,5 +1,5 @@ module Closed-  ( Endpoint(..)+  ( Endpoint (..)   , Closed   , Bounds   , Single

@@ -32,27 +32,30 @@ import GHC.Generics import GHC.Stack import GHC.TypeLits+import System.Random (Random (..)) import Test.QuickCheck+import Text.ParserCombinators.ReadP (pfail, readP_to_S, readS_to_P) -newtype Closed (n :: Nat) (m :: Nat)-  = Closed { getClosed :: Integer }+newtype Closed (a :: Nat) (b :: Nat) = Closed+  { getClosed :: Integer+  }   deriving (Generic)  -- | Describe whether the endpoint of a 'Bounds' includes -- or excludes its argument data Endpoint-  -- | Endpoint includes its argument-  = Inclusive Nat-  -- | Endpoint excludes its argument-  | Exclusive Nat+  = -- | Endpoint includes its argument+    Inclusive Nat+  | -- | Endpoint excludes its argument+    Exclusive Nat  -- | Syntactic sugar to express open and half-open intervals using -- the 'Closed' type type family Bounds (lhs :: Endpoint) (rhs :: Endpoint) :: Type where-  Bounds (Inclusive n) (Inclusive m) = Closed  n       m-  Bounds (Inclusive n) (Exclusive m) = Closed  n      (m - 1)-  Bounds (Exclusive n) (Inclusive m) = Closed (n + 1)  m-  Bounds (Exclusive n) (Exclusive m) = Closed (n + 1) (m - 1)+  Bounds (Inclusive a) (Inclusive b) = Closed a b+  Bounds (Inclusive a) (Exclusive b) = Closed a (b - 1)+  Bounds (Exclusive a) (Inclusive b) = Closed (a + 1) b+  Bounds (Exclusive a) (Exclusive b) = Closed (a + 1) (b - 1)  -- | Syntactic sugar to express a value that has only one non-bottom -- inhabitant using the 'Closed' type@@ -62,15 +65,19 @@ type FiniteNat (rhs :: Endpoint) = Bounds ('Inclusive 0) rhs  -- | Proxy for the lower bound of a 'Closed' value-lowerBound :: Closed n m -> Proxy n+lowerBound :: Closed a b -> Proxy a lowerBound _ = Proxy  -- | Proxy for the upper bound of a 'Closed' value-upperBound :: Closed n m -> Proxy m+upperBound :: Closed a b -> Proxy b upperBound _ = Proxy  -- | Safely create a 'Closed' value using the specified argument-closed :: forall n m. (n <= m, KnownNat n, KnownNat m) => Integer -> Maybe (Closed n m)+closed+  :: forall a b+   . (KnownNat a, KnownNat b, a <= b)+  => Integer+  -> Maybe (Closed a b) closed x = result  where   extracted = fromJust result@@ -79,7 +86,11 @@     pure $ Closed x  -- | Create a 'Closed' value throwing an error if the argument is not in range-unsafeClosed :: forall n m. (HasCallStack, n <= m, KnownNat n, KnownNat m) => Integer -> Closed n m+unsafeClosed+  :: forall a b+   . (HasCallStack, KnownNat a, KnownNat b, a <= b)+  => Integer+  -> Closed a b unsafeClosed x = result  where   result =@@ -88,22 +99,26 @@       else error $ unrepresentable x result "unsafeClosed"  -- | Clamp an @'Integral'@ in the range constrained by a @'Closed'@ interval-clamp :: forall n m a. (KnownNat n, KnownNat m, n <= m, Integral a) => a -> Closed n m+clamp+  :: forall a b i+   . (Integral i, KnownNat a, KnownNat b, a <= b)+  => i+  -> Closed a b clamp x-  | fromIntegral x < getClosed (minBound @(Closed n m)) = minBound-  | fromIntegral x > getClosed (maxBound @(Closed n m)) = maxBound+  | fromIntegral x < getClosed (minBound @(Closed a b)) = minBound+  | fromIntegral x > getClosed (maxBound @(Closed a b)) = maxBound   | otherwise = Closed (fromIntegral x)  -- | Test equality on 'Closed' values in the same range-instance Eq (Closed n m) where+instance Eq (Closed a b) where   Closed x == Closed y = x == y  -- | Compare 'Closed' values in the same range-instance Ord (Closed n m) where+instance Ord (Closed a b) where   Closed x `compare` Closed y = x `compare` y  -- | Generate the lowest and highest inhabitant of a given 'Closed' type-instance (n <= m, KnownNat n, KnownNat m) => Bounded (Closed n m) where+instance (KnownNat a, KnownNat b, a <= b) => Bounded (Closed a b) where   maxBound = result    where     result = Closed (natVal (upperBound result))@@ -113,20 +128,25 @@     result = Closed (natVal (lowerBound result))  -- | Enumerate values in the range of a given 'Closed' type-instance (n <= m, KnownNat n, KnownNat m) => Enum (Closed n m) where+instance (KnownNat a, KnownNat b, a <= b) => Enum (Closed a b) where   fromEnum = fromEnum . getClosed   toEnum = unsafeClosed . toEnum   enumFrom x = enumFromTo x maxBound   enumFromThen x y = enumFromThenTo x y (if x >= y then minBound else maxBound) -instance Show (Closed n m) where+instance Show (Closed a b) where   showsPrec d (Closed x) = showParen (d > 9) $ showString "unsafeClosed " . showsPrec 10 x +instance (KnownNat a, KnownNat b, a <= b) => Read (Closed a b) where+  readsPrec n = readP_to_S $ do+    i <- readS_to_P $ readsPrec @Integer n+    maybe pfail pure $ closed @a @b i+ -- | Bounded arithmetic, e.g. maxBound + 1 == maxBound-instance (n <= m, KnownNat n, KnownNat m) => Num (Closed n m) where-  Closed x + Closed y = Closed $ min (x + y) (fromIntegral (maxBound :: Closed n m))-  Closed x - Closed y = Closed $ max (x - y) (fromIntegral (minBound :: Closed n m))-  Closed x * Closed y = Closed $ min (x * y) (fromIntegral (maxBound :: Closed n m))+instance (KnownNat a, KnownNat b, a <= b) => Num (Closed a b) where+  Closed x + Closed y = Closed $ min (x + y) (fromIntegral (maxBound :: Closed a b))+  Closed x - Closed y = Closed $ max (x - y) (fromIntegral (minBound :: Closed a b))+  Closed x * Closed y = Closed $ min (x * y) (fromIntegral (maxBound :: Closed a b))   abs = id   signum = const 1   fromInteger x = result@@ -136,73 +156,96 @@         then Closed x         else error $ unrepresentable x result "fromInteger" -instance (n <= m, KnownNat n, KnownNat m) => Real (Closed n m) where+instance (KnownNat a, KnownNat b, a <= b) => Real (Closed a b) where   toRational (Closed x) = x % 1 -instance (n <= m, KnownNat n, KnownNat m) => Integral (Closed n m) where+instance (KnownNat a, KnownNat b, a <= b) => Integral (Closed a b) where   quotRem (Closed x) (Closed y) = (Closed $ x `quot` y, Closed $ x `rem` y)   toInteger (Closed x) = x -instance NFData (Closed n m)+instance NFData (Closed a b) -instance Hashable (Closed n m)+instance (KnownNat a, KnownNat b, a <= b) => Random (Closed a b) where+  randomR (a, b) g =+    let (x, g') = randomR (getClosed a, getClosed b) g+    in  (unsafeClosed x, g')+  random = randomR (minBound, maxBound) -instance ToJSON (Closed n m) where+instance Hashable (Closed a b)++instance ToJSON (Closed a b) where   toEncoding = toEncoding . getClosed   toJSON = toJSON . getClosed -instance (n <= m, KnownNat n, KnownNat m) => FromJSON (Closed n m) where+instance (KnownNat a, KnownNat b, a <= b) => FromJSON (Closed a b) where   parseJSON v = do     x <- parseJSON v     case closed x of       Just cx -> pure cx       n -> fail $ unrepresentable x (fromJust n) "parseJSON" -instance CSV.ToField (Closed n m) where+instance CSV.ToField (Closed a b) where   toField = CSV.toField . getClosed -instance (n <= m, KnownNat n, KnownNat m) => CSV.FromField (Closed n m) where+instance (KnownNat a, KnownNat b, a <= b) => CSV.FromField (Closed a b) where   parseField s = do     x <- CSV.parseField s     case closed x of       Just cx -> pure cx       n -> fail $ unrepresentable x (fromJust n) "parseField" -instance (n <= m, KnownNat n, KnownNat m) => Arbitrary (Closed n m) where+instance (KnownNat a, KnownNat b, a <= b) => Arbitrary (Closed a b) where   arbitrary =-    Closed <$> choose (natVal @n Proxy, natVal @m Proxy)+    Closed <$> choose (natVal @a Proxy, natVal @b Proxy) -instance (n <= m, KnownNat n, KnownNat m) => PersistField (Closed n m) where+instance (KnownNat a, KnownNat b, a <= b) => PersistField (Closed a b) where   toPersistValue = toPersistValue . fromIntegral @Integer @Int . getClosed   fromPersistValue value = do     x <- fromIntegral @Int @Integer <$> fromPersistValue value-    case closed @n @m x of+    case closed @a @b x of       Just cx -> pure cx       n -> Left $ pack $ unrepresentable x (fromJust n) "fromPersistValue" -instance (n <= m, KnownNat n, KnownNat m) => PersistFieldSql (Closed n m) where+instance (KnownNat a, KnownNat b, a <= b) => PersistFieldSql (Closed a b) where   sqlType _ = sqlType (Proxy @Int) -unrepresentable :: (KnownNat n, KnownNat m) => Integer -> Closed n m -> String -> String+unrepresentable+  :: (KnownNat a, KnownNat b)+  => Integer+  -> Closed a b+  -> String+  -> String unrepresentable x cx prefix =-  prefix ++ ": Integer " ++ show x ++-  " is not representable in Closed " ++ show (natVal $ lowerBound cx) ++-  " " ++ show (natVal $ upperBound cx)+  prefix+    <> ": Integer "+    <> show x+    <> " is not representable in Closed "+    <> show (natVal $ lowerBound cx)+    <> " "+    <> show (natVal $ upperBound cx)  -- | Convert a type-level literal into a 'Closed' value-natToClosed :: forall n m x proxy. (n <= x, x <= m, KnownNat x, KnownNat n, KnownNat m) => proxy x -> Closed n m+natToClosed+  :: forall a b x proxy+   . (KnownNat a, KnownNat b, KnownNat x, a <= x, x <= b)+  => proxy x+  -> Closed a b natToClosed p = Closed $ natVal p  -- | Add inhabitants at the end-weakenUpper :: forall k n m. (n <= m, m <= k) => Closed n m -> Closed n k+weakenUpper :: forall k a b. (a <= b, b <= k) => Closed a b -> Closed a k weakenUpper (Closed x) = Closed x  -- | Add inhabitants at the beginning-weakenLower :: forall k n m. (n <= m, k <= n) => Closed n m -> Closed k m+weakenLower :: forall k a b. (a <= b, k <= a) => Closed a b -> Closed k b weakenLower (Closed x) = Closed x  -- | Remove inhabitants from the end. Returns 'Nothing' if the input was removed-strengthenUpper :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed n k)+strengthenUpper+  :: forall k a b+   . (KnownNat a, KnownNat b, KnownNat k, a <= b, a <= k, k <= b)+  => Closed a b+  -> Maybe (Closed a k) strengthenUpper (Closed x) = result  where   result = do@@ -210,7 +253,11 @@     pure $ Closed x  -- | Remove inhabitants from the beginning. Returns 'Nothing' if the input was removed-strengthenLower :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed k m)+strengthenLower+  :: forall k a b+   . (KnownNat a, KnownNat b, KnownNat k, a <= b, a <= k, k <= b)+  => Closed a b+  -> Maybe (Closed k b) strengthenLower (Closed x) = result  where   result = do@@ -218,32 +265,36 @@     pure $ Closed x  -- | Test two different types of 'Closed' values for equality.-equals :: Closed n m -> Closed o p -> Bool+equals :: Closed a b -> Closed o p -> Bool equals (Closed x) (Closed y) = x == y+ infix 4 `equals`  -- | Compare two different types of 'Closed' values-cmp :: Closed n m -> Closed o p -> Ordering+cmp :: Closed a b -> Closed o p -> Ordering cmp (Closed x) (Closed y) = x `compare` y  -- | Add two different types of 'Closed' values-add :: Closed n m -> Closed o p -> Closed (n + o) (m + p)+add :: Closed a b -> Closed o p -> Closed (n + o) (m + p) add (Closed x) (Closed y) = Closed $ x + y  -- | Subtract two different types of 'Closed' values -- Returns 'Left' for negative results, and 'Right' for positive results.-sub :: Closed n m -> Closed o p -> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))+sub+  :: Closed a b+  -> Closed o p+  -> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p)) sub (Closed x) (Closed y)   | x >= y = Right $ Closed $ x - y   | otherwise = Left $ Closed $ y - x  -- | Multiply two different types of 'Closed' values-multiply :: Closed n m -> Closed o p -> Closed (n * o) (m * p)+multiply :: Closed a b -> Closed o p -> Closed (a * o) (b * p) multiply (Closed x) (Closed y) = Closed $ x * y  -- | Verifies that a given 'Closed' value is valid. -- Should always return 'True' unles you bring the @Closed.Internal.Closed@ constructor into scope, -- or use 'Unsafe.Coerce.unsafeCoerce' or other nasty hacks-isValidClosed :: (KnownNat n, KnownNat m) => Closed n m -> Bool+isValidClosed :: (KnownNat a, KnownNat b) => Closed a b -> Bool isValidClosed cx@(Closed x) =   natVal (lowerBound cx) <= x && x <= natVal (upperBound cx)