diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,6 +1,6 @@ Copyright © 2015 Nikita Volkov Copyright © 2018 Remy Goldschmidt -Copyright © 2018 Daniel Cartwright +Copyright © 2019 chessai Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation diff --git a/library/Refined.hs b/library/Refined.hs deleted file mode 100644 --- a/library/Refined.hs +++ /dev/null @@ -1,139 +0,0 @@ --------------------------------------------------------------------------------- - --- 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 ExplicitNamespaces #-} - --------------------------------------------------------------------------------- - --- | 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/ --- --- 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 - - -- ** 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 - - -- * Re-Exports - , pretty - ) where - --------------------------------------------------------------------------------- - -import Refined.Internal - -------------------------------------------------------------------------------- diff --git a/library/Refined/Internal.hs b/library/Refined/Internal.hs deleted file mode 100644 --- a/library/Refined/Internal.hs +++ /dev/null @@ -1,909 +0,0 @@ --------------------------------------------------------------------------------- - --- 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 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 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 - , NegativeFromTo - - -- * 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 - - , (|>) - , (.>) - - -- * 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 Data.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 --- :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 () - {-# INLINE validate #-} - --------------------------------------------------------------------------------- - --- | 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' - , 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. -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' - , 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. -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' - , newline - , twoSpaces - , "Size is: " - , PP.pretty sz - ] |> mconcat - ) - --------------------------------------------------------------------------------- - --- | 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 or equal than a negative --- number specified as a type-level (positive) number @n@ and less than a --- type-level (positive) number @m@. -data NegativeFromTo (n :: Nat) (m :: Nat) - deriving (Generic) - -instance (Ord x, Num x, KnownNat n, KnownNat m, n <= 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 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 - -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 - --------------------------------------------------------------------------------- - --- | 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 - --------------------------------------------------------------------------------- diff --git a/library/Refined/Orphan.hs b/library/Refined/Orphan.hs deleted file mode 100644 --- a/library/Refined/Orphan.hs +++ /dev/null @@ -1,44 +0,0 @@ --------------------------------------------------------------------------------- - --- 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 #-} - --------------------------------------------------------------------------------- - --- | This module exposes orphan instances for the 'Refined' type. --- This is unavoidable given the current module structure. -module Refined.Orphan () where - --------------------------------------------------------------------------------- - -import Refined.Orphan.Aeson () -import Refined.Orphan.QuickCheck () - --------------------------------------------------------------------------------- - diff --git a/library/Refined/Orphan/Aeson.hs b/library/Refined/Orphan/Aeson.hs deleted file mode 100644 --- a/library/Refined/Orphan/Aeson.hs +++ /dev/null @@ -1,56 +0,0 @@ --------------------------------------------------------------------------------- - --- 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 #-} - --------------------------------------------------------------------------------- - --- | This module exposes orphan instances for the 'Refined' type. --- This is unavoidable given the current module structure. -module Refined.Orphan.Aeson () where - --------------------------------------------------------------------------------- - -#if HAVE_AESON - -import Control.Monad ((<=<)) -import Data.Aeson (FromJSON(parseJSON), ToJSON(toJSON)) -import Refined.Internal (Refined, Predicate, refineFail, unrefine) - --------------------------------------------------------------------------------- - -instance (FromJSON a, Predicate p a) => FromJSON (Refined p a) where - parseJSON = refineFail <=< parseJSON - -instance (ToJSON a, Predicate p a) => ToJSON (Refined p a) where - toJSON = toJSON . unrefine - --------------------------------------------------------------------------------- - -#endif diff --git a/library/Refined/Orphan/QuickCheck.hs b/library/Refined/Orphan/QuickCheck.hs deleted file mode 100644 --- a/library/Refined/Orphan/QuickCheck.hs +++ /dev/null @@ -1,54 +0,0 @@ --------------------------------------------------------------------------------- - --- 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 #-} -{-# LANGUAGE ScopedTypeVariables #-} - --------------------------------------------------------------------------------- - --- | This module exposes orphan instances for the 'Refined' type. --- This is unavoidable given the current module structure. -module Refined.Orphan.QuickCheck () where - --------------------------------------------------------------------------------- - -#if HAVE_QUICKCHECK - -import Data.Either (isRight) -import Refined.Internal (Refined(Refined), RefineException, Predicate, refine) -import Test.QuickCheck (Arbitrary(arbitrary), suchThat, Gen) - --------------------------------------------------------------------------------- - -instance forall p a. (Arbitrary a, Predicate p a) => Arbitrary (Refined p a) where - arbitrary = Refined <$> suchThat (arbitrary :: Gen a) (isRight . (refine :: a -> Either RefineException (Refined p a))) - --------------------------------------------------------------------------------- - -#endif diff --git a/library/Refined/Unsafe.hs b/library/Refined/Unsafe.hs deleted file mode 100644 --- a/library/Refined/Unsafe.hs +++ /dev/null @@ -1,122 +0,0 @@ --------------------------------------------------------------------------------- - --- 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 diff --git a/library/Refined/Unsafe/Type.hs b/library/Refined/Unsafe/Type.hs deleted file mode 100644 --- a/library/Refined/Unsafe/Type.hs +++ /dev/null @@ -1,45 +0,0 @@ --------------------------------------------------------------------------------- - --- 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)) diff --git a/refined.cabal b/refined.cabal --- a/refined.cabal +++ b/refined.cabal @@ -3,27 +3,26 @@ name: refined version: - 0.4.1 + 0.4.2 synopsis: Refinement types with static and runtime checking description: - For an extensive introduction to the library please follow to + For an extensive introduction to the library please follow to . category: Data homepage: https://github.com/nikita-volkov/refined bug-reports: - https://github.com/nikita-volkov/refined/issues + https://github.com/nikita-volkov/refined/issues author: Nikita Volkov maintainer: - chessai + chessai copyright: Copyright © 2015, Nikita Volkov Copyright © 2018, Remy Goldschmidt - Copyright © 2018, Daniel Cartwright - + Copyright © 2019, chessai license: MIT license-file: @@ -34,7 +33,7 @@ GHC == 8.0.2 , GHC == 8.2.2 , GHC == 8.4.4 - , GHC == 8.6.4 + , GHC == 8.6.5 flag aeson description: @@ -60,29 +59,39 @@ library hs-source-dirs: - library + src exposed-modules: Refined Refined.Internal Refined.Orphan Refined.Orphan.Aeson Refined.Orphan.QuickCheck - Refined.Unsafe + Refined.These + Refined.Unsafe Refined.Unsafe.Type default-language: Haskell2010 build-depends: - base >= 4.9.1.0 && < 4.13.0.0 - , deepseq >= 1.4.0.0 && < 1.5.0.0 - , exceptions >= 0.8.0.0 && < 0.11.0 - , mtl >= 2.2.1.0 && < 3.0.0.0 - , prettyprinter >= 1.1.0.1 && < 1.3.0.0 - , template-haskell >= 2.9.0.0 && < 2.15.0.0 - , these >= 0.7.0.0 && < 0.8.0.0 - , transformers >= 0.5.0.0 && < 0.6.0.0 + base >= 4.9.1 && < 4.14 + , deepseq >= 1.4 && < 1.5 + , exceptions >= 0.8 && < 0.11 + , mtl >= 2.2.1 && < 2.3 + , prettyprinter >= 1.1.0.1 && < 1.4 + , template-haskell >= 2.9 && < 2.15 + , transformers >= 0.5 && < 0.6 if flag(aeson) - build-depends: aeson >= 0.9 && < 1.5.0.0 + build-depends: aeson >= 0.9 && < 1.5 cpp-options: -DHAVE_AESON if flag(QuickCheck) build-depends: QuickCheck >= 2.1 && < 2.13 cpp-options: -DHAVE_QUICKCHECK + +test-suite doctest + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: Doctests.hs + build-depends: + base + , refined + , doctest >= 0.10 + default-language: Haskell2010 diff --git a/src/Refined.hs b/src/Refined.hs new file mode 100644 --- /dev/null +++ b/src/Refined.hs @@ -0,0 +1,139 @@ +-------------------------------------------------------------------------------- + +-- 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 #-} + +-------------------------------------------------------------------------------- + +{-# language ExplicitNamespaces #-} + +-------------------------------------------------------------------------------- + +-- | 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/ +-- +-- 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 + + -- ** 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 + + -- * Re-Exports + , pretty + ) where + +-------------------------------------------------------------------------------- + +import Refined.Internal + +------------------------------------------------------------------------------- diff --git a/src/Refined/Internal.hs b/src/Refined/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Refined/Internal.hs @@ -0,0 +1,1090 @@ +-------------------------------------------------------------------------------- + +-- 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 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 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(..) + , 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 + + -- * Error handling + + -- ** 'RefineException' + , RefineException + ( RefineNotException + , RefineAndException + , RefineOrException + , RefineOtherException + ) + , displayRefineException + + -- ** 'RefineT' and 'RefineM' + , RefineT, runRefineT, 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 #-} + +-- | 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 +-- > :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. +-- The value is not evaluated by 'validate'. +-- +-- >>> 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@. +-- That is to say, @m `mod` 'natVal' ('Proxy' @n) '==' 0@ +-- +-- >>> 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 + +-------------------------------------------------------------------------------- + +-- | 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 + +-------------------------------------------------------------------------------- + +-- | 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 + +-------------------------------------------------------------------------------- diff --git a/src/Refined/Orphan.hs b/src/Refined/Orphan.hs new file mode 100644 --- /dev/null +++ b/src/Refined/Orphan.hs @@ -0,0 +1,44 @@ +-------------------------------------------------------------------------------- + +-- 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. + +-------------------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} + +-------------------------------------------------------------------------------- + +-- | This module exposes orphan instances for the 'Refined' type. +-- This is unavoidable given the current module structure. +module Refined.Orphan () where + +-------------------------------------------------------------------------------- + +import Refined.Orphan.Aeson () +import Refined.Orphan.QuickCheck () + +-------------------------------------------------------------------------------- + diff --git a/src/Refined/Orphan/Aeson.hs b/src/Refined/Orphan/Aeson.hs new file mode 100644 --- /dev/null +++ b/src/Refined/Orphan/Aeson.hs @@ -0,0 +1,56 @@ +-------------------------------------------------------------------------------- + +-- 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. + +-------------------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} + +-------------------------------------------------------------------------------- + +-- | This module exposes orphan instances for the 'Refined' type. +-- This is unavoidable given the current module structure. +module Refined.Orphan.Aeson () where + +-------------------------------------------------------------------------------- + +#if HAVE_AESON + +import Control.Monad ((<=<)) +import Data.Aeson (FromJSON(parseJSON), ToJSON(toJSON)) +import Refined.Internal (Refined, Predicate, refineFail, unrefine) + +-------------------------------------------------------------------------------- + +instance (FromJSON a, Predicate p a) => FromJSON (Refined p a) where + parseJSON = refineFail <=< parseJSON + +instance (ToJSON a, Predicate p a) => ToJSON (Refined p a) where + toJSON = toJSON . unrefine + +-------------------------------------------------------------------------------- + +#endif diff --git a/src/Refined/Orphan/QuickCheck.hs b/src/Refined/Orphan/QuickCheck.hs new file mode 100644 --- /dev/null +++ b/src/Refined/Orphan/QuickCheck.hs @@ -0,0 +1,54 @@ +-------------------------------------------------------------------------------- + +-- 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. + +-------------------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-------------------------------------------------------------------------------- + +-- | This module exposes orphan instances for the 'Refined' type. +-- This is unavoidable given the current module structure. +module Refined.Orphan.QuickCheck () where + +-------------------------------------------------------------------------------- + +#if HAVE_QUICKCHECK + +import Data.Either (isRight) +import Refined.Internal (Refined(Refined), RefineException, Predicate, refine) +import Test.QuickCheck (Arbitrary(arbitrary), suchThat, Gen) + +-------------------------------------------------------------------------------- + +instance forall p a. (Arbitrary a, Predicate p a) => Arbitrary (Refined p a) where + arbitrary = Refined <$> suchThat (arbitrary :: Gen a) (isRight . (refine :: a -> Either RefineException (Refined p a))) + +-------------------------------------------------------------------------------- + +#endif diff --git a/src/Refined/These.hs b/src/Refined/These.hs new file mode 100644 --- /dev/null +++ b/src/Refined/These.hs @@ -0,0 +1,265 @@ +-------------------------------------------------------------------------------- + +-- 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 #-} + +-------------------------------------------------------------------------------- + +{-# 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 + diff --git a/src/Refined/Unsafe.hs b/src/Refined/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Refined/Unsafe.hs @@ -0,0 +1,122 @@ +-------------------------------------------------------------------------------- + +-- 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. + +-------------------------------------------------------------------------------- + +{-# 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 diff --git a/src/Refined/Unsafe/Type.hs b/src/Refined/Unsafe/Type.hs new file mode 100644 --- /dev/null +++ b/src/Refined/Unsafe/Type.hs @@ -0,0 +1,45 @@ +-------------------------------------------------------------------------------- + +-- 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 #-} + +-------------------------------------------------------------------------------- + +-- | 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)) diff --git a/test/Doctests.hs b/test/Doctests.hs new file mode 100644 --- /dev/null +++ b/test/Doctests.hs @@ -0,0 +1,23 @@ +module Main (main) where + +import Test.DocTest + +main :: IO () +main = doctest $ srcFiles ++ compFlags + +srcFiles :: [String] +srcFiles = + [ "src/Refined.hs" + , "src/Refined/Internal.hs" + , "src/Refined/Orphan/Aeson.hs" + , "src/Refined/Orphan/QuickCheck.hs" + , "src/Refined/Orphan.hs" + , "src/Refined/These.hs" + , "src/Refined/Unsafe/Type.hs" + , "src/Refined/Unsafe.hs" + ] + +compFlags :: [String] +compFlags = + [ "-XScopedTypeVariables" + ]