refined 0.2.3.0 → 0.3.0.0
raw patch · 8 files changed
+1290/−728 lines, 8 filesdep +deepseqdep −containersdep −thesedep ~exceptionssetup-changed
Dependencies added: deepseq
Dependencies removed: containers, these
Dependency ranges changed: exceptions
Files
- Setup.hs +0/−2
- library/Refined.hs +16/−679
- library/Refined/Internal.hs +835/−0
- library/Refined/TH.hs +0/−41
- library/Refined/These.hs +264/−0
- library/Refined/Unsafe.hs +122/−0
- library/Refined/Unsafe/Type.hs +45/−0
- refined.cabal +8/−6
− Setup.hs
@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain
library/Refined.hs view
@@ -27,29 +27,12 @@ -------------------------------------------------------------------------------- -{-# OPTIONS_GHC -Wall #-}-{-# OPTIONS_GHC -funbox-strict-fields #-}+{-# OPTIONS_GHC -Wall #-} -{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveFoldable #-}-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE ExplicitNamespaces #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE QuasiQuotes #-}-{-# LANGUAGE RoleAnnotations #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}+-------------------------------------------------------------------------------- +{-# language ExplicitNamespaces #-}+ -------------------------------------------------------------------------------- -- | In type theory, a refinement type is a type endowed@@ -62,6 +45,13 @@ -- -- A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/ --+-- This module only provides /safe/ constructions of 'Refined'+-- values, /safe/ meaning that the refinement predicate holds,+-- and the construction of the 'Refined' value is total.+--+-- If you can manually prove that the refinement predicate holds,+-- or you do not necessarily care about this definition of safety,+-- use the module /Refined.Unsafe/. module Refined ( -- * 'Refined' Refined@@ -71,7 +61,6 @@ , refineThrow , refineFail , refineError- , unsafeRefine , refineTH -- ** Consumption@@ -87,6 +76,9 @@ , Or , type (||) + -- * Identity predicate+ , IdPred+ -- * Numeric predicates , LessThan , GreaterThan@@ -139,661 +131,6 @@ -------------------------------------------------------------------------------- -import Prelude- (Num, error, fromIntegral, undefined)--import Control.Applicative (Applicative (pure))-import Control.Exception (Exception (displayException))-import Control.Monad (Monad, unless, when)-import Data.Bool ((&&))-import Data.Coerce (coerce)-import Data.Either- (Either (Left, Right), either, isRight)-import Data.Eq (Eq, (==), (/=))-import Data.Foldable (Foldable(length))-import Data.Function (const, id, flip, ($))-import Data.Functor (Functor, fmap)-import Data.Functor.Identity (Identity (runIdentity))-import Data.List ((++))-import qualified Data.List as List-import Data.Monoid (mconcat)-import Data.Ord (Ord, (<), (<=), (>), (>=))-import Data.Proxy (Proxy (Proxy))-import Data.Semigroup (Semigroup((<>)))-import Data.These (These(..))-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.Exts (IsList(Item, toList))-import GHC.Generics (Generic, Generic1)-import GHC.TypeLits (type (<=), KnownNat, Nat, natVal)--import qualified Data.Text.Prettyprint.Doc as PP--import qualified Language.Haskell.TH.Syntax as TH-------------------------------------------------------------------------------------- Helper functions,--- from the 'flow' package.-infixl 0 |>-infixl 9 .>--(|>) :: a -> (a -> b) -> b-(|>) = flip ($)-{-# INLINE (|>) #-}--(.>) :: (a -> b) -> (b -> c) -> a -> c-f .> g = \x -> g (f x)-{-# INLINE (.>) #-}-------------------------------------------------------------------------------------- | A refinement type, which wraps a value of type @x@,--- ensuring that it satisfies a type-level predicate @p@.------ The only ways that this library provides to construct--- a value of type 'Refined' are with the 'refine-' family--- of functions, because the use of the newtype constructor--- gets around the checking of the predicate. This restriction--- on the user makes 'unrefine' safe.--- --- If you would /really/ like to--- construct a 'Refined' value without checking the predicate,--- use 'Unsafe.Coerce.unsafeCoerce'.-newtype Refined p x = Refined x- deriving- ( Eq- , Foldable - , Ord- , Show- , Typeable- )--type role Refined phantom representational--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 #-}---- | 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 run-time,--- calling 'Prelude.error' if the value--- does not satisfy the predicate.------ WARNING: this function is not total!-unsafeRefine :: (Predicate p x) => x -> Refined p x-unsafeRefine = refine .> either (displayException .> error) id-{-# INLINABLE unsafeRefine #-}-------------------------------------------------------------------------------------- | 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.-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-------------------------------------------------------------------------------------- | 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 ()-------------------------------------------------------------------------------------- | The negation of a predicate.-data Not p--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.-data And l r--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.-data Or l r--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.-data SizeLessThan (n :: Nat)--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' <> "\n"- <> "\tSize is: " <> PP.pretty sz-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the 'Foldable' has a length--- which is greater than the specified type-level number.-data SizeGreaterThan (n :: Nat)--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' <> "\n"- <> "\tSize is: " <> PP.pretty sz-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the 'Foldable' has a length--- which is equal to the specified type-level number.-data SizeEqualTo (n :: Nat)--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' <> "\n"- <> "\tSize is: " <> PP.pretty sz-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the 'IsList' contains elements--- in a strictly ascending order.-data Ascending--instance (IsList t, Ord (Item t)) => Predicate Ascending t where- validate p x = do- let asList = toList x- unless (List.sort asList == asList) $ do- throwRefineOtherException (typeOf p)- $ "IsList is not in ascending order "-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the 'IsList' contains elements--- in a strictly descending order.-data Descending--instance (IsList t, Ord (Item t)) => Predicate Descending t where- validate p x = do- let asList = toList x- unless (List.reverse (List.sort asList) == asList) $ do- throwRefineOtherException (typeOf p)- $ "IsList is not in ascending order "-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the value is less than the--- specified type-level number.-data LessThan (n :: Nat)--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.-data GreaterThan (n :: Nat)--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.-data From (n :: Nat)--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.-data To (n :: Nat)--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.-data FromTo (mn :: Nat) (mx :: Nat)--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@.-data EqualTo (n :: Nat)--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@.-data NotEqualTo (n :: Nat)--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 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-------------------------------------------------------------------------------------- | 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---- | Display a 'RefineException' as a @'PP.Doc' ann@-displayRefineException :: RefineException -> PP.Doc ann-displayRefineException (RefineOtherException tr msg)- = PP.pretty ("The predicate (" ++ show tr ++ ") does not hold: \n \t" ++ show msg)-displayRefineException (RefineNotException tr)- = PP.pretty ("The negation of the predicate (" ++ show tr ++ ") does not hold.")-displayRefineException (RefineOrException tr orLChild orRChild)- = PP.pretty ("Both subpredicates failed in: (" ++ show tr ++ "). \n")- <> "\t" <> (displayRefineException orLChild) <> "\n"- <> "\t" <> (displayRefineException orRChild) <> "\n"-displayRefineException (RefineAndException tr andChild)- = PP.pretty ("The predicate (" ++ show tr ++ ") does not hold: \n \t")- <> case andChild of- This a -> "The left subpredicate does not hold:\n\t" <> displayRefineException a <> "\n"- That b -> "The right subpredicate does not hold:\n\t" <> displayRefineException b <> "\n"- These a b -> "\t Neither subpredicate holds: \n"- <> "\t" <> displayRefineException a <> "\n"- <> "\t" <> displayRefineException b <> "\n"---- | 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---- | 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-------------------------------------------------------------------------------------- | 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+import Refined.Internal ---------------------------------------------------------------------------------+-------------------------------------------------------------------------------
+ library/Refined/Internal.hs view
@@ -0,0 +1,835 @@+--------------------------------------------------------------------------------++-- Copyright © 2015 Nikita Volkov+-- Copyright © 2018 Remy Goldschmidt+-- Copyright © 2018 Daniel Cartwright+--+-- 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 DataKinds #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE QuasiQuotes #-}+{-# 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+ , refineThrow+ , refineFail+ , refineError+ , refineTH++ -- ** Consumption+ , unrefine++ -- * 'Predicate'+ , Predicate (validate)++ -- * Logical predicates+ , Not+ , And+ , type (&&)+ , Or+ , type (||)++ -- * Identity predicate+ , IdPred++ -- * Numeric predicates+ , LessThan+ , GreaterThan+ , From+ , To+ , FromTo+ , EqualTo+ , NotEqualTo + , Positive+ , NonPositive+ , Negative+ , NonNegative+ , ZeroToOne+ , NonZero++ -- * Foldable predicates+ , SizeLessThan+ , SizeGreaterThan+ , SizeEqualTo+ , NonEmpty++ -- * IsList predicates+ , Ascending+ , Descending++ -- * Weakening+ , Weaken (weaken)+ , andLeft+ , andRight+ , leftOr+ , rightOr++ -- * Error handling++ -- ** 'RefineException'+ , RefineException+ ( RefineNotException+ , RefineAndException+ , RefineOrException+ , RefineOtherException+ )+ , displayRefineException++ -- ** 'RefineT' and 'RefineM'+ , RefineT, runRefineT, mapRefineT+ , RefineM, refineM, runRefineM+ , throwRefine, catchRefine+ , throwRefineOtherException+ + , (|>)+ , (.>)+ ) where++--------------------------------------------------------------------------------++import Prelude+ (Num, fromIntegral, 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.List ((++))+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 Refined.These (These(This,That,These))++import qualified Data.Text.Prettyprint.Doc as PP+import qualified Language.Haskell.TH.Syntax as TH++--------------------------------------------------------------------------------++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 #-}++-- | 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++--------------------------------------------------------------------------------++-- | 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 ()++--------------------------------------------------------------------------------++-- | A predicate which is satisfied for all types.+data IdPred+ deriving (Generic)++instance Predicate IdPred x where+ validate _ _ = pure ()++--------------------------------------------------------------------------------++-- | The negation of a predicate.+data Not p+ 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.+data And l r+ 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.+data Or l r+ 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.+data SizeLessThan (n :: Nat)+ 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' <> "\n"+ <> "\tSize is: " <> PP.pretty sz++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the 'Foldable' has a length+-- which is greater than the specified type-level number.+data SizeGreaterThan (n :: Nat)+ 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' <> "\n"+ <> "\tSize is: " <> PP.pretty sz++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the 'Foldable' has a length+-- which is equal to the specified type-level number.+data SizeEqualTo (n :: Nat)+ 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' <> "\n"+ <> "\tSize is: " <> PP.pretty sz++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the 'Foldable' contains elements+-- in a strictly ascending order.+data 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.+data 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.+data LessThan (n :: Nat)+ 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.+data GreaterThan (n :: Nat)+ 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.+data From (n :: Nat)+ 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.+data To (n :: Nat)+ 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.+data FromTo (mn :: Nat) (mx :: Nat)+ 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@.+data EqualTo (n :: Nat)+ 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@.+data NotEqualTo (n :: Nat)+ 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 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++--------------------------------------------------------------------------------++-- | 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++-- | Display a 'RefineException' as a @'PP.Doc' ann@+displayRefineException :: RefineException -> PP.Doc ann+displayRefineException (RefineOtherException tr msg)+ = PP.pretty ("The predicate (" ++ show tr ++ ") does not hold: \n \t" ++ show msg)+displayRefineException (RefineNotException tr)+ = PP.pretty ("The negation of the predicate (" ++ show tr ++ ") does not hold.")+displayRefineException (RefineOrException tr orLChild orRChild)+ = PP.pretty ("Both subpredicates failed in: (" ++ show tr ++ "). \n")+ <> "\t" <> (displayRefineException orLChild) <> "\n"+ <> "\t" <> (displayRefineException orRChild) <> "\n"+displayRefineException (RefineAndException tr andChild)+ = PP.pretty ("The predicate (" ++ show tr ++ ") does not hold: \n \t")+ <> case andChild of+ This a -> "The left subpredicate does not hold:\n\t" <> displayRefineException a <> "\n"+ That b -> "The right subpredicate does not hold:\n\t" <> displayRefineException b <> "\n"+ These a b -> "\t Neither subpredicate holds: \n"+ <> "\t" <> displayRefineException a <> "\n"+ <> "\t" <> displayRefineException b <> "\n"++-- | 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++-- | 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++--------------------------------------------------------------------------------++-- | 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++--------------------------------------------------------------------------------
− library/Refined/TH.hs
@@ -1,41 +0,0 @@-----------------------------------------------------------------------------------{-# LANGUAGE DeriveLift #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell #-}------------------------------------------------------------------------------------{-| This module contains orphan 'Lift' instances of types in common libraries- such as 'containers', for more available compile-time checking of predicates.---}--module Refined.TH () where------------------------------------------------------------------------------------import Data.IntMap.Internal (IntMap(..))-import Data.Map.Internal (Map(..))-import Data.Sequence.Internal (Digit(..), Elem(..), FingerTree(..), Node(..), Seq(..), ViewL(..), ViewR(..))-import Data.Set.Internal (Set(..))-import Data.Tree (Tree(..))--import Language.Haskell.TH.Syntax (Lift)-------------------------------------------------------------------------------------- [containers]-deriving instance (Lift a) => Lift (IntMap a)-deriving instance (Lift k, Lift v) => Lift (Map k v)-deriving instance (Lift v) => Lift (Set v)-deriving instance (Lift a) => Lift (Elem a)-deriving instance (Lift a) => Lift (Node a)-deriving instance (Lift a) => Lift (Digit a)-deriving instance (Lift a) => Lift (FingerTree a)-deriving instance (Lift a) => Lift (Seq a)-deriving instance (Lift a) => Lift (ViewL a)-deriving instance (Lift a) => Lift (ViewR a)-deriving instance (Lift a) => Lift (Tree a)----------------------------------------------------------------------------------
+ library/Refined/These.hs view
@@ -0,0 +1,264 @@+--------------------------------------------------------------------------------++-- Copyright © 2015 Nikita Volkov+-- Copyright © 2018 Remy Goldschmidt+-- Copyright © 2018 Daniel Cartwright+--+-- 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 #-}++--------------------------------------------------------------------------------++{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE InstanceSigs #-}++--------------------------------------------------------------------------------++-- | This module is defined internally to avoid using the 'these'+-- package, which brings in a lot of very heavy and unnecessary +-- transitive dependencies. We export the type and constructors+-- here, in case a user should need it.+-- We provide a small API for working with the 'These' type here.+-- If one should need a fuller API, see https://hackage.haskell.org/package/these+-- Converting to/from the two types should be trivial, as the+-- data constructors are exported from both.+module Refined.These+ (+ -- * 'These' type + These(This, That, These)+ + -- * Consumption+ , these+ , fromThese+ , mergeThese+ , mergeTheseWith++ -- * Traversals+ , here, there++ -- * Case selections+ , justThis+ , justThat+ , justThese++ , catThis+ , catThat+ , catThese+ + , partitionThese++ -- * Case predicates+ , isThis+ , isThat+ , isThese++ -- * Map operations+ , mapThese+ , mapThis+ , mapThat+ ) where++--------------------------------------------------------------------------------++import Control.DeepSeq (NFData(rnf))+#if MIN_VERSION_base(4,10,0)+import Data.Bifoldable (Bifoldable(bifold, bifoldr, bifoldl))+#endif+#if MIN_VERSION_base(4,8,0)+import Data.Bifunctor (Bifunctor(bimap, first, second))+#endif+import Data.Data (Data)+import Data.Maybe (isJust, mapMaybe)+import Data.Semigroup (Semigroup((<>)))+import Data.Typeable (Typeable)+import GHC.Generics (Generic, Generic1)+ +-- | This is defined internally to avoid using the 'these'+-- package, which brings in a lot of very heavy and unnecessary +-- transitive dependencies. We export the type and constructors+-- here, in case a user should need it.+data These a b = This a | That b | These a b+ deriving (Eq, Ord, Read, Show, Typeable, Data, Generic, Generic1)++-- | Case analysis for the 'These' type.+these :: (a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c+these l _ _ (This a) = l a+these _ r _ (That x) = r x+these _ _ lr (These a x) = lr a x++-- | Takes two default values and produces a tuple.+fromThese :: a -> b -> These a b -> (a, b)+fromThese _ x (This a ) = (a, x)+fromThese a _ (That x ) = (a, x)+fromThese _ _ (These a x) = (a, x)++-- | Coalesce with the provided operation.+mergeThese :: (a -> a -> a) -> These a a -> a+mergeThese = these id id++-- | BiMap and coalesce results with the provided operation.+mergeTheseWith :: (a -> c) -> (b -> c) -> (c -> c -> c) -> These a b -> c+mergeTheseWith f g op t = mergeThese op $ mapThese f g t++-- | A @Traversal@ of the first half of a 'These', suitable for use with @Control.Lens@.+here :: (Applicative f) => (a -> f b) -> These a t -> f (These b t)+here f (This x) = This <$> f x+here f (These x y) = flip These y <$> f x+here _ (That x) = pure (That x)++-- | A @Traversal@ of the second half of a 'These', suitable for use with @Control.Lens@.+there :: (Applicative f) => (a -> f b) -> These t a -> f (These t b)+there _ (This x) = pure (This x)+there f (These x y) = These x <$> f y+there f (That x) = That <$> f x++-- | @'justThis' = 'these' 'Just' (\_ -> 'Nothing') (\_ _ -> 'Nothing')@+justThis :: These a b -> Maybe a+justThis = these Just (\_ -> Nothing) (\_ _ -> Nothing)++-- | @'justThat' = 'these' (\_ -> 'Nothing') 'Just' (\_ _ -> 'Nothing')@+justThat :: These a b -> Maybe b+justThat = these (\_ -> Nothing) Just (\_ _ -> Nothing)++-- | @'justThese' = 'these' (\_ -> 'Nothing') (\_ -> 'Nothing') (\a b -> 'Just' (a, b))@+justThese :: These a b -> Maybe (a, b)+justThese = these (\_ -> Nothing) (\_ -> Nothing) (\a b -> Just (a, b))++isThis, isThat, isThese :: These a b -> Bool+-- | @'isThis' = 'isJust' . 'justThis'@+isThis = isJust . justThis++-- | @'isThat' = 'isJust' . 'justThat'@+isThat = isJust . justThat++-- | @'isThese' = 'isJust' . 'justThese'@+isThese = isJust . justThese++-- | 'Bifunctor' map.+mapThese :: (a -> c) -> (b -> d) -> These a b -> These c d+mapThese f _ (This a ) = This (f a)+mapThese _ g (That x) = That (g x)+mapThese f g (These a x) = These (f a) (g x)++-- | @'mapThis' = over 'here'@+mapThis :: (a -> c) -> These a b -> These c b+mapThis f = mapThese f id++-- | @'mapThat' = over 'there'@+mapThat :: (b -> d) -> These a b -> These a d+mapThat f = mapThese id f++-- | Select all 'This' constructors from a list.+catThis :: [These a b] -> [a]+catThis = mapMaybe justThis++-- | Select all 'That' constructors from a list.+catThat :: [These a b] -> [b]+catThat = mapMaybe justThat++-- | Select all 'These' constructors from a list.+catThese :: [These a b] -> [(a, b)]+catThese = mapMaybe justThese++-- | Select each constructor and partition them into separate lists.+partitionThese :: [These a b] -> ( [(a, b)], ([a], [b]) )+partitionThese [] = ([], ([], []))+partitionThese (These x y:xs) = first ((x, y):) $ partitionThese xs+partitionThese (This x :xs) = second (first (x:)) $ partitionThese xs+partitionThese (That y:xs) = second (second (y:)) $ partitionThese xs++instance (Semigroup a, Semigroup b) => Semigroup (These a b) where+ This a <> This b = This (a <> b)+ This a <> That y = These a y+ This a <> These b y = These (a <> b) y+ That x <> This b = These b x+ That x <> That y = That (x <> y)+ That x <> These b y = These b (x <> y)+ These a x <> This b = These (a <> b) x+ These a x <> That y = These a (x <> y)+ These a x <> These b y = These (a <> b) (x <> y)++#if MIN_VERSION_base(4,8,0)+instance Bifunctor These where+ bimap :: (a -> c) -> (b -> d) -> These a b -> These c d + bimap f _ (This a ) = This (f a)+ bimap _ g (That b) = That (g b)+ bimap f g (These a b) = These (f a) (g b)+ first :: (a -> c) -> These a b -> These c b+ first f = bimap f id+ second :: (b -> d) -> These a b -> These a d+ second f = bimap id f+#endif++instance Functor (These a) where+ fmap _ (This x) = This x+ fmap f (That y) = That (f y)+ fmap f (These x y) = These x (f y)++instance Semigroup a => Applicative (These a) where+ pure = That+ This a <*> _ = This a+ That _ <*> This b = This b+ That f <*> That x = That (f x)+ That f <*> These b x = These b (f x)+ These a _ <*> This b = This (a <> b)+ These a f <*> That x = These a (f x)+ These a f <*> These b x = These (a <> b) (f x)++instance Semigroup a => Monad (These a) where+ return = pure+ This a >>= _ = This a+ That x >>= k = k x+ These a x >>= k = case k x of+ This b -> This (a <> b)+ That y -> These a y+ These b y -> These (a <> b) y++instance (NFData a, NFData b) => NFData (These a b) where+ rnf (This a) = rnf a+ rnf (That b) = rnf b+ rnf (These a b) = rnf a `seq` rnf b++instance Foldable (These a) where+ foldr _ z (This _) = z+ foldr f z (That x) = f x z+ foldr f z (These _ x) = f x z++instance Traversable (These a) where+ traverse _ (This a ) = pure $ This a+ traverse f (That x) = That <$> f x+ traverse f (These a x) = These a <$> f x+ sequenceA (This a ) = pure $ This a+ sequenceA (That x) = That <$> x+ sequenceA (These a x) = These a <$> x++#if MIN_VERSION_base(4,10,0)+instance Bifoldable These where+ bifold = these id id mappend+ bifoldr f g z = these (`f` z) (`g` z) (\x y -> x `f` (y `g` z))+ bifoldl f g z = these (z `f`) (z `g`) (\x y -> (z `f` x) `g` y)+#endif
+ library/Refined/Unsafe.hs view
@@ -0,0 +1,122 @@+--------------------------------------------------------------------------------++-- Copyright © 2015 Nikita Volkov+-- Copyright © 2018 Remy Goldschmidt+-- Copyright © 2018 Daniel Cartwright+--+-- 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.++--------------------------------------------------------------------------------++{-# LANGUAGE CPP #-}+#if __GLASGOW_HASKELL__ >= 805+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+#endif+{-# OPTIONS_GHC -Wall #-}++--------------------------------------------------------------------------------++-- | This module exposes /unsafe/ refinements. An /unsafe/ refinement+-- is one which either does not make the guarantee of totality in construction+-- of the 'Refined' value or does not perform a check of the refinement+-- predicate. It is recommended only to use this when you can manually prove+-- that the refinement predicate holds.+module Refined.Unsafe+ ( -- * 'Refined'+ Refined++ -- ** Creation+ , reallyUnsafeRefine + , unsafeRefine++ -- ** Coercion+ , reallyUnsafeUnderlyingRefined+#if __GLASGOW_HASKELL__ >= 805+ , reallyUnsafeAllUnderlyingRefined+#endif+ , reallyUnsafePredEquiv+ ) where++--------------------------------------------------------------------------------++import Control.Exception (Exception(displayException))+import Data.Coerce (coerce)+import Data.Either (either)+import Data.Function (id)++import GHC.Err (error)++import Refined.Internal (Refined(Refined), Predicate, refine, (.>))+import Data.Type.Coercion (Coercion (..))+#if __GLASGOW_HASKELL__ >= 805+import Data.Coerce (Coercible)+#endif++--------------------------------------------------------------------------------++-- | Constructs a 'Refined' value at run-time,+-- calling 'Prelude.error' if the value+-- does not satisfy the predicate.+--+-- WARNING: this function is not total!+unsafeRefine :: (Predicate p x) => x -> Refined p x+unsafeRefine = refine .> either (displayException .> error) id+{-# INLINABLE unsafeRefine #-}++-- | Constructs a 'Refined' value, completely+-- ignoring any refinements! Use this only+-- when you can manually prove that the refinement+-- holds.+reallyUnsafeRefine :: x -> Refined p x+reallyUnsafeRefine = coerce+{-# INLINE reallyUnsafeRefine #-}++-- | A coercion between a type and any refinement of that type.+-- See "Data.Type.Coercion" for functions manipulating coercions.+reallyUnsafeUnderlyingRefined :: Coercion x (Refined p x)+reallyUnsafeUnderlyingRefined = Coercion++-- | A coercion between two 'Refined' types, magicking up the claim+-- that one predicate is entirely equivalent to another.+reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)+reallyUnsafePredEquiv = Coercion+-- Note: reallyUnsafePredEquiv =+-- sym 'reallyUnsafeUnderlyingRefined' `trans` 'reallyUnsafeUnderlyingRefined'++#if __GLASGOW_HASKELL__ >= 805+-- | Reveal that @x@ and @'Refined' p x@ are 'Coercible' for+-- /all/ @x@ and @p@ simultaneously.+--+-- === Example+--+-- @+-- reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)+-- reallyUnsafePredEquiv = reallyUnsafeAllUnderlyingRefined Coercion+-- @+reallyUnsafeAllUnderlyingRefined+ :: ((forall x y p. (Coercible x y => Coercible y (Refined p x))) => r) -> r+-- Why is this constraint so convoluted? Because otherwise the constraint+-- solver doesn't handle transitivity properly. See "Safe Zero-cost Coercions+-- for Haskell" by Breitner et al.+reallyUnsafeAllUnderlyingRefined r = r+#endif
+ library/Refined/Unsafe/Type.hs view
@@ -0,0 +1,45 @@+--------------------------------------------------------------------------------++-- Copyright © 2015 Nikita Volkov+-- Copyright © 2018 Remy Goldschmidt+-- Copyright © 2018 Daniel Cartwright+--+-- 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 #-}++--------------------------------------------------------------------------------++-- | This module exports the 'Refined' type with its+-- constructor. This is very risky! In particular, the 'Coercible'+-- instances will be visible throughout the importing module.+-- It is usually better to build the necessary coercions locally+-- using the utilities in "Refined.Unsafe", but in some cases+-- it may be more convenient to write a separate module that+-- imports this one and exports some large coercion.+module Refined.Unsafe.Type+ ( Refined(Refined)+ ) where++import Refined.Internal (Refined(Refined))
refined.cabal view
@@ -1,7 +1,7 @@ name: refined version:- 0.2.3.0+ 0.3.0.0 synopsis: Refinement types with static and runtime checking description:@@ -16,7 +16,7 @@ author: Nikita Volkov <nikita.y.volkov@mail.ru> maintainer:- Nikita Volkov <nikita.y.volkov@mail.ru>+ chessai <chessai1996@gmail.com> copyright: Copyright © 2015, Nikita Volkov Copyright © 2018, Remy Goldschmidt@@ -46,15 +46,17 @@ library exposed-modules: Refined- Refined.TH+ Refined.Internal+ Refined.These+ Refined.Unsafe + Refined.Unsafe.Type default-language: Haskell2010 build-depends: base >= 4.9 && < 5- , containers >= 0.5.9.1- , exceptions >= 0.10.0+ , deepseq >= 1.4.0.0 + , exceptions >= 0.8.0 , mtl >= 2.2.1 , prettyprinter >= 1.1.0.1 , template-haskell >= 2.9 && < 3.0- , these >= 0.7.4 , transformers >= 0.5.0.0