refined-0.4.4: src/Refined/Internal.hs
--------------------------------------------------------------------------------
-- Copyright © 2015 Nikita Volkov
-- Copyright © 2018 Remy Goldschmidt
-- Copyright © 2019 chessai
--
-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:
--
-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.
--
-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.
--------------------------------------------------------------------------------
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -funbox-strict-fields #-}
--------------------------------------------------------------------------------
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
--------------------------------------------------------------------------------
-- | In type theory, a refinement type is a type endowed
-- with a predicate which is assumed to hold for any element
-- of the refined type.
--
-- This library allows one to capture the idea of a refinement type
-- using the 'Refined' type. A 'Refined' @p@ @x@ wraps a value
-- of type @x@, ensuring that it satisfies a type-level predicate @p@.
--
-- A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/
--
module Refined.Internal
( -- * 'Refined'
Refined(Refined)
-- ** Creation
, refine
, refine_
, refineThrow
, refineFail
, refineError
, refineTH
, refineTH_
-- ** Consumption
, unrefine
-- * 'Predicate'
, Predicate (validate)
, reifyPredicate
-- * Logical predicates
, Not(..)
, And(..)
, type (&&)
, Or(..)
, type (||)
-- * Identity predicate
, IdPred(..)
-- * Numeric predicates
, LessThan(..)
, GreaterThan(..)
, From(..)
, To(..)
, FromTo(..)
, NegativeFromTo(..)
, EqualTo(..)
, NotEqualTo(..)
, Odd(..)
, Even(..)
, DivisibleBy(..)
, Positive
, NonPositive
, Negative
, NonNegative
, ZeroToOne
, NonZero
-- * Foldable predicates
, SizeLessThan(..)
, SizeGreaterThan(..)
, SizeEqualTo(..)
, NonEmpty
-- * IsList predicates
, Ascending(..)
, Descending(..)
-- * Weakening
, Weaken (weaken)
, andLeft
, andRight
, leftOr
, rightOr
-- * Strengthening
, strengthen
, strengthenM
-- * Error handling
-- ** 'RefineException'
, RefineException
( RefineNotException
, RefineAndException
, RefineOrException
, RefineOtherException
)
, displayRefineException
-- ** 'RefineT' and 'RefineM'
, RefineT, runRefineT, exceptRefine, mapRefineT
, RefineM, refineM, runRefineM
, throwRefine, catchRefine
, throwRefineOtherException
, (|>)
, (.>)
-- * Re-Exports
, PP.pretty
) where
--------------------------------------------------------------------------------
import Prelude
(Num, fromIntegral, negate, undefined)
import Control.Applicative (Applicative (pure))
import Control.Exception (Exception (displayException))
import Control.Monad (Monad, unless, when)
import Data.Bool (Bool(True,False),(&&), otherwise)
import Data.Coerce (coerce)
import Data.Either
(Either (Left, Right), either, isRight)
import Data.Eq (Eq, (==), (/=))
import Data.Foldable (Foldable(length, foldl'))
import Data.Function (const, flip, ($), (.))
import Data.Functor (Functor, fmap)
import Data.Functor.Identity (Identity (runIdentity))
import Data.Monoid (mconcat)
import Data.Ord (Ord, (<), (<=), (>), (>=))
import Data.Proxy (Proxy (Proxy))
import Data.Semigroup (Semigroup((<>)))
import Data.Typeable (TypeRep, Typeable, typeOf)
import Data.Void (Void)
import Text.Read (Read (readsPrec), lex, readParen)
import Text.Show (Show (show))
import Control.Monad.Catch (MonadThrow)
import qualified Control.Monad.Catch as MonadThrow
import Control.Monad.Error.Class (MonadError)
import qualified Control.Monad.Error.Class as MonadError
import Control.Monad.Fail (MonadFail, fail)
import Control.Monad.Fix (MonadFix, fix)
import Control.Monad.Trans.Class (MonadTrans (lift))
import Control.Monad.Trans.Except (ExceptT)
import qualified Control.Monad.Trans.Except as ExceptT
import GHC.Generics (Generic, Generic1)
import GHC.TypeLits (type (<=), KnownNat, Nat, natVal)
import GHC.Real (Integral(mod), even, odd)
import Refined.These (These(This,That,These))
import qualified Data.Text.Prettyprint.Doc as PP
import qualified Language.Haskell.TH.Syntax as TH
--------------------------------------------------------------------------------
-- $setup
--
-- Doctest imports
--
-- >>> :set -XDataKinds
-- >>> :set -XTypeApplications
-- >>> import Data.Int
-- >>> import Data.Either (isLeft)
--
--------------------------------------------------------------------------------
infixl 0 |>
infixl 9 .>
-- | Helper function, stolen from the 'flow' package.
(|>) :: a -> (a -> b) -> b
(|>) = flip ($)
{-# INLINE (|>) #-}
-- | Helper function, stolen from the 'flow' package.
(.>) :: (a -> b) -> (b -> c) -> a -> c
f .> g = \x -> g (f x)
{-# INLINE (.>) #-}
-- | FIXME: doc
data Ordered a = Empty | Decreasing a | Increasing a
-- | FIXME: doc
inc :: Ordered a -> Bool
inc (Decreasing _) = False
inc _ = True
{-# INLINE inc #-}
-- | FIXME: doc
dec :: Ordered a -> Bool
dec (Increasing _) = False
dec _ = True
{-# INLINE dec #-}
increasing :: (Foldable t, Ord a) => t a -> Bool
increasing = inc . foldl' go Empty where
go Empty y = Increasing y
go (Decreasing x) _ = Decreasing x
go (Increasing x) y
| x <= y = Increasing y
| otherwise = Decreasing y
{-# INLINABLE increasing #-}
decreasing :: (Foldable t, Ord a) => t a -> Bool
decreasing = dec . foldl' go Empty where
go Empty y = Decreasing y
go (Increasing x) _ = Increasing x
go (Decreasing x) y
| x >= y = Decreasing y
| otherwise = Increasing y
{-# INLINABLE decreasing #-}
--------------------------------------------------------------------------------
-- | A refinement type, which wraps a value of type @x@,
-- ensuring that it satisfies a type-level predicate @p@.
newtype Refined p x = Refined x
deriving (Eq, Foldable , Ord, Show, Typeable)
type role Refined nominal nominal
-- | This instance makes sure to check the refinement.
instance (Read x, Predicate p x) => Read (Refined p x) where
readsPrec d = readParen (d > 10) $ \r1 -> do
("Refined", r2) <- lex r1
(raw, r3) <- readsPrec 11 r2
case refine raw of
Right val -> [(val, r3)]
Left _ -> []
instance (TH.Lift x) => TH.Lift (Refined p x) where
lift (Refined a) = [|Refined a|]
--------------------------------------------------------------------------------
-- | A smart constructor of a 'Refined' value.
-- Checks the input value at runtime.
refine :: (Predicate p x) => x -> Either RefineException (Refined p x)
refine x = do
let predicateByResult :: RefineM (Refined p x) -> p
predicateByResult = const undefined
runRefineM $ fix $ \result -> do
validate (predicateByResult result) x
pure (Refined x)
{-# INLINABLE refine #-}
-- | Like 'refine', but discards the refinement.
-- This _can_ be useful when you only need to validate
-- that some value at runtime satisfies some predicate.
-- See also 'reifyPredicate'.
refine_ :: forall p x. (Predicate p x) => x -> Either RefineException x
refine_ = refine @p @x .> coerce
-- | Constructs a 'Refined' value at run-time,
-- calling 'Control.Monad.Catch.throwM' if the value
-- does not satisfy the predicate.
refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x)
refineThrow = refine .> either MonadThrow.throwM pure
{-# INLINABLE refineThrow #-}
-- | Constructs a 'Refined' value at run-time,
-- calling 'Control.Monad.Fail.fail' if the value
-- does not satisfy the predicate.
refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x)
refineFail = refine .> either (displayException .> fail) pure
{-# INLINABLE refineFail #-}
-- | Constructs a 'Refined' value at run-time,
-- calling 'Control.Monad.Error.throwError' if the value
-- does not satisfy the predicate.
refineError :: (Predicate p x, MonadError RefineException m)
=> x -> m (Refined p x)
refineError = refine .> either MonadError.throwError pure
{-# INLINABLE refineError #-}
--------------------------------------------------------------------------------
-- | Constructs a 'Refined' value at compile-time using @-XTemplateHaskell@.
--
-- For example:
--
-- > $$(refineTH 23) :: Refined Positive Int
-- > Refined 23
--
-- Here's an example of an invalid value:
--
-- > $$(refineTH 0) :: Refined Positive Int
-- > <interactive>:6:4:
-- > Value is not greater than 0
-- > In the Template Haskell splice $$(refineTH 0)
-- > In the expression: $$(refineTH 0) :: Refined Positive Int
-- > In an equation for ‘it’:
-- > it = $$(refineTH 0) :: Refined Positive Int
--
-- If it's not evident, the example above indicates a compile-time failure,
-- which means that the checking was done at compile-time, thus introducing a
-- zero runtime overhead compared to a plain value construction.
--
-- It may be useful to use this function with the `th-lift-instances` package at https://hackage.haskell.org/package/th-lift-instances/
refineTH :: (Predicate p x, TH.Lift x) => x -> TH.Q (TH.TExp (Refined p x))
refineTH =
let refineByResult :: (Predicate p x)
=> TH.Q (TH.TExp (Refined p x))
-> x
-> Either RefineException (Refined p x)
refineByResult = const refine
in fix $ \loop -> refineByResult (loop undefined)
.> either (show .> fail) TH.lift
.> fmap TH.TExp
-- | Like 'refineTH', but immediately unrefines the value.
-- This is useful when some value need only be refined
-- at compile-time.
refineTH_ :: forall p x. (Predicate p x, TH.Lift x)
=> x
-> TH.Q (TH.TExp x)
refineTH_ =
let refineByResult :: (Predicate p x)
=> TH.Q (TH.TExp x)
-> x
-> Either RefineException x
refineByResult = const (refine_ @p @x)
in fix $ \loop -> refineByResult (loop undefined)
.> either (show .> fail) TH.lift
.> fmap TH.TExp
--------------------------------------------------------------------------------
-- | Extracts the refined value.
{-# INLINE unrefine #-}
unrefine :: Refined p x -> x
unrefine = coerce
--------------------------------------------------------------------------------
-- | A typeclass which defines a runtime interpretation of
-- a type-level predicate @p@ for type @x@.
class (Typeable p) => Predicate p x where
{-# MINIMAL validate #-}
-- | Check the value @x@ according to the predicate @p@,
-- producing an error string if the value does not satisfy.
validate :: (Monad m) => p -> x -> RefineT m ()
--------------------------------------------------------------------------------
-- | Reify a 'Predicate' by turning it into a value-level predicate.
reifyPredicate :: forall p a. Predicate p a => a -> Bool
reifyPredicate = refine @p @a .> isRight
--------------------------------------------------------------------------------
-- | A predicate which is satisfied for all types.
-- Arguments passed to @'validate'@ in @'validate' 'IdPred' x@
-- are not evaluated.
--
-- >>> isRight (refine @IdPred @Int undefined)
-- True
--
-- >>> isLeft (refine @IdPred @Int undefined)
-- False
--
data IdPred = IdPred
deriving (Generic)
instance Predicate IdPred x where
validate _ _ = pure ()
{-# INLINE validate #-}
--------------------------------------------------------------------------------
-- | The negation of a predicate.
--
-- >>> isRight (refine @(Not NonEmpty) @[Int] [])
-- True
--
-- >>> isLeft (refine @(Not NonEmpty) @[Int] [1,2])
-- True
data Not p = Not
deriving (Generic, Generic1)
instance (Predicate p x, Typeable p) => Predicate (Not p) x where
validate p x = do
result <- runRefineT (validate @p undefined x)
when (isRight result) $ do
throwRefine (RefineNotException (typeOf p))
--------------------------------------------------------------------------------
-- | The conjunction of two predicates.
--
-- >>> isLeft (refine @(And Positive Negative) @Int 3)
-- True
--
-- >>> isRight (refine @(And Positive Odd) @Int 203)
-- True
data And l r = And
deriving (Generic, Generic1)
infixr 3 &&
-- | The conjunction of two predicates.
type (&&) = And
instance ( Predicate l x, Predicate r x, Typeable l, Typeable r
) => Predicate (And l r) x where
validate p x = do
a <- lift $ runRefineT $ validate @l undefined x
b <- lift $ runRefineT $ validate @r undefined x
let throw err = throwRefine (RefineAndException (typeOf p) err)
case (a, b) of
(Left e, Left e1) -> throw (These e e1)
(Left e, _) -> throw (This e)
(Right _, Left e) -> throw (That e)
(Right _, Right _) -> pure ()
--------------------------------------------------------------------------------
-- | The disjunction of two predicates.
--
-- >>> isRight (refine @(Or Even Odd) @Int 3)
-- True
--
-- >>> isRight (refine @(Or (LessThan 3) (GreaterThan 3)) @Int 2)
-- True
data Or l r = Or
deriving (Generic, Generic1)
infixr 2 ||
-- | The disjunction of two predicates.
type (||) = Or
instance ( Predicate l x, Predicate r x, Typeable l, Typeable r
) => Predicate (Or l r) x where
validate p x = do
left <- lift $ runRefineT $ validate @l undefined x
right <- lift $ runRefineT $ validate @r undefined x
case (left, right) of
(Left l, Left r) -> throwRefine (RefineOrException (typeOf p) l r)
_ -> pure ()
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the 'Foldable' has a length
-- which is less than the specified type-level number.
--
-- >>> isRight (refine @(SizeLessThan 4) @[Int] [1,2,3])
-- True
--
-- >>> isLeft (refine @(SizeLessThan 5) @[Int] [1,2,3,4,5])
-- True
data SizeLessThan (n :: Nat) = SizeLessThan
deriving (Generic)
instance (Foldable t, KnownNat n) => Predicate (SizeLessThan n) (t a) where
validate p x = do
let x' = natVal p
sz = length x
unless (sz < fromIntegral x') $ do
throwRefineOtherException (typeOf p)
( [ "Size of Foldable is not less than "
, PP.pretty x'
, newline
, twoSpaces
, "Size is: "
, PP.pretty sz
] |> mconcat
)
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the 'Foldable' has a length
-- which is greater than the specified type-level number.
--
-- >>> isLeft (refine @(SizeGreaterThan 3) @[Int] [1,2,3])
-- True
--
-- >>> isRight (refine @(SizeGreaterThan 3) @[Int] [1,2,3,4,5])
-- True
data SizeGreaterThan (n :: Nat) = SizeGreaterThan
deriving (Generic)
instance (Foldable t, KnownNat n) => Predicate (SizeGreaterThan n) (t a) where
validate p x = do
let x' = natVal p
sz = length x
unless (sz > fromIntegral x') $ do
throwRefineOtherException (typeOf p)
( [ "Size of Foldable is not greater than "
, PP.pretty x'
, newline
, twoSpaces
, "Size is: "
, PP.pretty sz
] |> mconcat
)
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the 'Foldable' has a length
-- which is equal to the specified type-level number.
--
-- >>> isRight (refine @(SizeEqualTo 4) @[Int] [1,2,3,4])
-- True
--
-- >>> isLeft (refine @(SizeEqualTo 35) @[Int] [1,2,3,4])
-- True
data SizeEqualTo (n :: Nat) = SizeEqualTo
deriving (Generic)
instance (Foldable t, KnownNat n) => Predicate (SizeEqualTo n) (t a) where
validate p x = do
let x' = natVal p
sz = length x
unless (sz == fromIntegral x') $ do
throwRefineOtherException (typeOf p)
( [ "Size of Foldable is not equal to "
, PP.pretty x'
, newline
, twoSpaces
, "Size is: "
, PP.pretty sz
] |> mconcat
)
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the 'Foldable' contains elements
-- in a strictly ascending order.
--
-- >>> isRight (refine @Ascending @[Int] [5, 8, 13, 21, 34])
-- True
--
-- >>> isLeft (refine @Ascending @[Int] [34, 21, 13, 8, 5])
-- True
data Ascending = Ascending
deriving (Generic)
instance (Foldable t, Ord a) => Predicate Ascending (t a) where
validate p x = do
unless (increasing x) $ do
throwRefineOtherException (typeOf p) ( "Foldable is not in ascending order." )
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the 'Foldable' contains elements
-- in a strictly descending order.
--
-- >>> isRight (refine @Descending @[Int] [34, 21, 13, 8, 5])
-- True
--
-- >>> isLeft (refine @Descending @[Int] [5, 8, 13, 21, 34])
-- True
data Descending = Descending
deriving (Generic)
instance (Foldable t, Ord a) => Predicate Descending (t a) where
validate p x = do
unless (decreasing x) $ do
throwRefineOtherException (typeOf p) ( "Foldable is not in descending order." )
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the value is less than the
-- specified type-level number.
--
-- >>> isRight (refine @(LessThan 12) @Int 11)
-- True
--
-- >>> isLeft (refine @(LessThan 12) @Int 12)
-- True
data LessThan (n :: Nat) = LessThan
deriving (Generic)
instance (Ord x, Num x, KnownNat n) => Predicate (LessThan n) x where
validate p x = do
let x' = natVal p
unless (x < fromIntegral x') $ do
throwRefineOtherException (typeOf p) ( "Value is not less than " <> PP.pretty x' )
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the value is greater than the
-- specified type-level number.
--
-- >>> isRight (refine @(GreaterThan 65) @Int 67)
-- True
--
-- >>> isLeft (refine @(GreaterThan 65) @Int 65)
-- True
data GreaterThan (n :: Nat) = GreaterThan
deriving (Generic)
instance (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x where
validate p x = do
let x' = natVal p
unless (x > fromIntegral x') $ do
throwRefineOtherException (typeOf p) ( "Value is not greater than " <> PP.pretty x' )
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the value is greater than or equal to the
-- specified type-level number.
--
-- >>> isRight (refine @(From 9) @Int 10)
-- True
--
-- >>> isRight (refine @(From 10) @Int 10)
-- True
--
-- >>> isLeft (refine @(From 11) @Int 10)
-- True
data From (n :: Nat) = From
deriving (Generic)
instance (Ord x, Num x, KnownNat n) => Predicate (From n) x where
validate p x = do
let x' = natVal p
unless (x >= fromIntegral x') $ do
throwRefineOtherException (typeOf p) ( "Value is less than " <> PP.pretty x' )
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the value is less than or equal to the
-- specified type-level number.
--
-- >>> isRight (refine @(To 23) @Int 17)
-- True
--
-- >>> isLeft (refine @(To 17) @Int 23)
-- True
data To (n :: Nat) = To
deriving (Generic)
instance (Ord x, Num x, KnownNat n) => Predicate (To n) x where
validate p x = do
let x' = natVal p
unless (x <= fromIntegral x') $ do
throwRefineOtherException (typeOf p) ( "Value is greater than " <> PP.pretty x' )
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the value is within an inclusive range.
--
-- >>> isRight (refine @(FromTo 0 16) @Int 13)
-- True
--
-- >>> isRight (refine @(FromTo 13 15) @Int 13)
-- True
--
-- >>> isRight (refine @(FromTo 13 15) @Int 15)
-- True
--
-- >>> isLeft (refine @(FromTo 13 15) @Int 12)
-- True
data FromTo (mn :: Nat) (mx :: Nat) = FromTo
deriving (Generic)
instance ( Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx
) => Predicate (FromTo mn mx) x where
validate p x = do
let mn' = natVal (Proxy @mn)
let mx' = natVal (Proxy @mx)
unless ((x >= fromIntegral mn') && (x <= fromIntegral mx')) $ do
let msg = [ "Value is out of range (minimum: "
, PP.pretty mn'
, ", maximum: "
, PP.pretty mx'
, ")"
] |> mconcat
throwRefineOtherException (typeOf p) msg
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the value is equal to the specified
-- type-level number @n@.
--
-- >>> isRight (refine @(EqualTo 5) @Int 5)
-- True
--
-- >>> isLeft (refine @(EqualTo 6) @Int 5)
-- True
data EqualTo (n :: Nat) = EqualTo
deriving (Generic)
instance (Eq x, Num x, KnownNat n) => Predicate (EqualTo n) x where
validate p x = do
let x' = natVal p
unless (x == fromIntegral x') $ do
throwRefineOtherException (typeOf p) ("Value does not equal " <> PP.pretty x')
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the value is not equal to the specified
-- type-level number @n@.
--
-- >>> isRight (refine @(NotEqualTo 6) @Int 5)
-- True
--
-- >>> isLeft (refine @(NotEqualTo 5) @Int 5)
-- True
data NotEqualTo (n :: Nat) = NotEqualTo
deriving (Generic)
instance (Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n) x where
validate p x = do
let x' = natVal p
unless (x /= fromIntegral x') $ do
throwRefineOtherException (typeOf p) ( "Value does equal " <> PP.pretty x' )
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the value is greater or equal than a negative
-- number specified as a type-level (positive) number @n@ and less than a
-- type-level (positive) number @m@.
--
-- >>> isRight (refine @(NegativeFromTo 5 12) @Int (-3))
-- True
--
-- >>> isLeft (refine @(NegativeFromTo 4 3) @Int (-5))
-- True
data NegativeFromTo (n :: Nat) (m :: Nat) = NegativeFromTo
deriving (Generic)
instance (Ord x, Num x, KnownNat n, KnownNat m) => Predicate (NegativeFromTo n m) x where
validate p x = do
let n' = natVal (Proxy @n)
m' = natVal (Proxy @m)
unless (x >= negate (fromIntegral n') && x <= fromIntegral m') $ do
let msg = [ "Value is out of range (minimum: "
, PP.pretty (negate n')
, ", maximum: "
, PP.pretty m'
, ")"
] |> mconcat
throwRefineOtherException (typeOf p) msg
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the value is divisible by @n@.
--
-- >>> isRight (refine @(DivisibleBy 3) @Int 12)
-- True
--
-- >>> isLeft (refine @(DivisibleBy 2) @Int 37)
-- True
data DivisibleBy (n :: Nat) = DivisibleBy
deriving (Generic)
instance (Integral x, KnownNat n) => Predicate (DivisibleBy n) x where
validate p x = unless (x `mod` (fromIntegral $ natVal p) == 0) $ do
throwRefineOtherException (typeOf p) $ "Value is not divisible by " <> PP.pretty (natVal p)
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the value is odd.
--
-- >>> isRight (refine @Odd @Int 33)
-- True
--
-- >>> isLeft (refine @Odd @Int 32)
-- True
data Odd = Odd
deriving (Generic)
instance (Integral x) => Predicate Odd x where
validate p x = unless (odd x) $ do
throwRefineOtherException (typeOf p) $ "Value is not odd."
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the value is even.
--
-- >>> isRight (refine @Even @Int 32)
-- True
--
-- >>> isLeft (refine @Even @Int 33)
-- True
data Even = Even
deriving (Generic)
instance (Integral x) => Predicate Even x where
validate p x = unless (even x) $ do
throwRefineOtherException (typeOf p) $ "Value is not even."
--------------------------------------------------------------------------------
-- | A 'Predicate' ensuring that the value is greater than zero.
type Positive = GreaterThan 0
-- | A 'Predicate' ensuring that the value is less than or equal to zero.
type NonPositive = To 0
-- | A 'Predicate' ensuring that the value is less than zero.
type Negative = LessThan 0
-- | A 'Predicate' ensuring that the value is greater than or equal to zero.
type NonNegative = From 0
-- | An inclusive range of values from zero to one.
type ZeroToOne = FromTo 0 1
-- | A 'Predicate' ensuring that the value is not equal to zero.
type NonZero = NotEqualTo 0
-- | A 'Predicate' ensuring that the 'Foldable' is non-empty.
type NonEmpty = SizeGreaterThan 0
--------------------------------------------------------------------------------
-- |
-- A typeclass containing "safe" conversions between refined predicates
-- where the target is /weaker/ than the source: that is, all values that
-- satisfy the first predicate will be guarunteed to satisy the second.
--
-- Take care: writing an instance declaration for your custom predicates is
-- the same as an assertion that 'weaken' is safe to use:
--
-- @
-- instance 'Weaken' Pred1 Pred2
-- @
--
-- For most of the instances, explicit type annotations for the result
-- value's type might be required.
class Weaken from to where
weaken :: Refined from x -> Refined to x
weaken = coerce
instance (n <= m) => Weaken (LessThan n) (LessThan m)
instance (n <= m) => Weaken (LessThan n) (To m)
instance (n <= m) => Weaken (To n) (To m)
instance (m <= n) => Weaken (GreaterThan n) (GreaterThan m)
instance (m <= n) => Weaken (GreaterThan n) (From m)
instance (m <= n) => Weaken (From n) (From m)
instance (p <= n, m <= q) => Weaken (FromTo n m) (FromTo p q)
instance (p <= n) => Weaken (FromTo n m) (From p)
instance (m <= q) => Weaken (FromTo n m) (To q)
-- | This function helps type inference.
-- It is equivalent to the following:
--
-- @
-- instance Weaken (And l r) l
-- @
andLeft :: Refined (And l r) x -> Refined l x
andLeft = coerce
-- | This function helps type inference.
-- It is equivalent to the following:
--
-- @
-- instance Weaken (And l r) r
-- @
andRight :: Refined (And l r) x -> Refined r x
andRight = coerce
-- | This function helps type inference.
-- It is equivalent to the following:
--
-- @
-- instance Weaken l (Or l r)
-- @
leftOr :: Refined l x -> Refined (Or l r) x
leftOr = coerce
-- | This function helps type inference.
-- It is equivalent to the following:
--
-- @
-- instance Weaken r (Or l r)
-- @
rightOr :: Refined r x -> Refined (Or l r) x
rightOr = coerce
-- | Strengthen a refinement by composing it with another.
strengthen :: forall p p' x. (Predicate p x, Predicate p' x)
=> Refined p x
-> Either RefineException (Refined (p && p') x)
strengthen r = refine @(p && p') (unrefine r)
{-# inlineable strengthen #-}
-- | Strengthen a refinement by composing it with another
-- inside of the 'RefineT' monad.
strengthenM :: forall p p' x m. (Predicate p x, Predicate p' x, Monad m)
=> Refined p x
-> RefineT m (Refined (p && p') x)
strengthenM r = exceptRefine (strengthen r)
--------------------------------------------------------------------------------
-- | An exception encoding the way in which a 'Predicate' failed.
data RefineException
= -- | A 'RefineException' for failures involving the 'Not' predicate.
RefineNotException
{ _RefineException_typeRep :: !TypeRep
-- ^ The 'TypeRep' of the @'Not' p@ type.
}
| -- | A 'RefineException' for failures involving the 'And' predicate.
RefineAndException
{ _RefineException_typeRep :: !TypeRep
-- ^ The 'TypeRep' of the @'And' l r@ type.
, _RefineException_andChild :: !(These RefineException RefineException)
-- ^ A 'These' encoding which branch(es) of the 'And' failed:
-- if the 'RefineException' came from the @l@ predicate, then
-- this will be 'This', if it came from the @r@ predicate, this
-- will be 'That', and if it came from both @l@ and @r@, this
-- will be 'These'.
-- note to self: what am I, Dr. Seuss?
}
| -- | A 'RefineException' for failures involving the 'Or' predicate.
RefineOrException
{ _RefineException_typeRep :: !TypeRep
-- ^ The 'TypeRep' of the @'Or' l r@ type.
, _RefineException_orLChild :: !RefineException
-- ^ The 'RefineException' for the @l@ failure.
, _RefineException_orRChild :: !RefineException
-- ^ The 'RefineException' for the @l@ failure.
}
| -- | A 'RefineException' for failures involving all other predicates.
RefineOtherException
{ _RefineException_typeRep :: !TypeRep
-- ^ The 'TypeRep' of the predicate that failed.
, _RefineException_message :: !(PP.Doc Void)
-- ^ A custom message to display.
}
deriving (Generic)
instance Show RefineException where
show = PP.pretty .> show
twoSpaces, newline :: PP.Doc ann
{-# INLINE twoSpaces #-}
{-# INLINE newline #-}
twoSpaces = " "
newline = "\n"
-- | Display a 'RefineException' as a @'PP.Doc' ann@
displayRefineException :: RefineException -> PP.Doc ann
displayRefineException = \case
RefineOtherException tr msg ->
[ "The predicate ("
, PP.pretty (show tr)
, ") does not hold: "
, newline
, twoSpaces
, PP.pretty (show msg)
] |> mconcat
RefineNotException tr ->
[ "The negation of the predicate ("
, PP.pretty (show tr)
, ") does not hold:"
, newline
, twoSpaces
] |> mconcat
RefineOrException tr orLChild orRChild ->
[ "Both subpredicates failed in: ("
, PP.pretty (show tr)
, "):"
, newline
, twoSpaces
, displayRefineException orLChild
, newline
, twoSpaces
, displayRefineException orRChild
, newline
, twoSpaces
] |> mconcat
RefineAndException tr andChild ->
(
[ "The predicate ("
, PP.pretty (show tr)
, ") does not hold:"
, newline
, twoSpaces
] |> mconcat
)
<> case andChild of
This a -> mconcat [ "The left subpredicate does not hold:", newline, twoSpaces, displayRefineException a, newline ]
That b -> mconcat [ "The right subpredicate does not hold:", newline, twoSpaces, displayRefineException b, newline ]
These a b -> mconcat [ twoSpaces, "Neither subpredicate holds: ", newline
, twoSpaces, displayRefineException a, newline
, twoSpaces, displayRefineException b, newline
]
-- | Pretty-print a 'RefineException'.
instance PP.Pretty RefineException where
pretty = displayRefineException
-- | Encode a 'RefineException' for use with \Control.Exception\.
instance Exception RefineException where
displayException = show
--------------------------------------------------------------------------------
-- | A monad transformer that adds @'RefineException'@s to other monads.
--
-- The @'pure'@ and @'Control.Monad.return'@ functions yield computations that produce
-- the given value, while @'>>='@ sequences two subcomputations, exiting
-- on the first @'RefineException'@.
newtype RefineT m a
= RefineT (ExceptT RefineException m a)
deriving ( Functor, Applicative, Monad, MonadFix
, MonadError RefineException, MonadTrans
, Generic, Generic1
)
-- | The inverse of @'RefineT'@.
runRefineT
:: RefineT m a
-> m (Either RefineException a)
runRefineT = coerce .> ExceptT.runExceptT
-- | Map the unwrapped computation using the given function.
--
-- @'runRefineT' ('mapRefineT' f m) = f ('runRefineT' m)@
mapRefineT
:: (m (Either RefineException a) -> n (Either RefineException b))
-> RefineT m a
-> RefineT n b
mapRefineT f = coerce .> ExceptT.mapExceptT f .> coerce
--------------------------------------------------------------------------------
-- | @'RefineM' a@ is equivalent to @'RefineT' 'Identity' a@ for any type @a@.
type RefineM a = RefineT Identity a
-- | Constructs a computation in the 'RefineM' monad. (The inverse of @'runRefineM'@).
refineM
:: Either RefineException a
-> RefineM a
refineM = ExceptT.except .> (coerce :: ExceptT RefineException Identity a -> RefineM a)
-- | Run a monadic action of type @'RefineM' a@,
-- yielding an @'Either' 'RefineException' a@.
--
-- This is just defined as @'runIdentity' '.' 'runRefineT'@.
runRefineM
:: RefineM a
-> Either RefineException a
runRefineM = runRefineT .> runIdentity
--------------------------------------------------------------------------------
-- | Constructor for computations in the @'RefineT'@ movie.
-- (The inverse of 'runRefineT').
exceptRefine
:: (Monad m)
=> Either RefineException a
-> RefineT m a
exceptRefine = MonadError.liftEither
-- | One can use @'throwRefine'@ inside of a monadic
-- context to begin processing a @'RefineException'@.
throwRefine
:: (Monad m)
=> RefineException
-> RefineT m a
throwRefine = MonadError.throwError
-- | A handler function to handle previous @'RefineException'@s
-- and return to normal execution. A common idiom is:
--
-- @ do { action1; action2; action3 } `'catchRefine'` handler @
--
-- where the action functions can call @'throwRefine'@. Note that
-- handler and the do-block must have the same return type.
catchRefine
:: (Monad m)
=> RefineT m a
-> (RefineException -> RefineT m a)
-> RefineT m a
catchRefine = MonadError.catchError
-- | A handler for a @'RefineException'@.
--
-- 'throwRefineOtherException' is useful for defining what
-- behaviour 'validate' should have in the event of a predicate failure.
throwRefineOtherException
:: (Monad m)
=> TypeRep
-- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeOf'.
-> PP.Doc Void
-- ^ A 'PP.Doc' 'Void' encoding a custom error message to be pretty-printed.
-> RefineT m a
throwRefineOtherException rep
= RefineOtherException rep .> throwRefine
--------------------------------------------------------------------------------