diff --git a/Setup.hs b/Setup.hs deleted file mode 100644 --- a/Setup.hs +++ /dev/null @@ -1,2 +0,0 @@ -import Distribution.Simple -main = defaultMain diff --git a/library/Refined.hs b/library/Refined.hs --- a/library/Refined.hs +++ b/library/Refined.hs @@ -27,29 +27,12 @@ -------------------------------------------------------------------------------- -{-# OPTIONS_GHC -Wall #-} -{-# OPTIONS_GHC -funbox-strict-fields #-} +{-# OPTIONS_GHC -Wall #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE ExplicitNamespaces #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE QuasiQuotes #-} -{-# LANGUAGE RoleAnnotations #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} +-------------------------------------------------------------------------------- +{-# language ExplicitNamespaces #-} + -------------------------------------------------------------------------------- -- | In type theory, a refinement type is a type endowed @@ -62,6 +45,13 @@ -- -- A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/ -- +-- This module only provides /safe/ constructions of 'Refined' +-- values, /safe/ meaning that the refinement predicate holds, +-- and the construction of the 'Refined' value is total. +-- +-- If you can manually prove that the refinement predicate holds, +-- or you do not necessarily care about this definition of safety, +-- use the module /Refined.Unsafe/. module Refined ( -- * 'Refined' Refined @@ -71,7 +61,6 @@ , refineThrow , refineFail , refineError - , unsafeRefine , refineTH -- ** Consumption @@ -87,6 +76,9 @@ , Or , type (||) + -- * Identity predicate + , IdPred + -- * Numeric predicates , LessThan , GreaterThan @@ -139,661 +131,6 @@ -------------------------------------------------------------------------------- -import Prelude - (Num, error, fromIntegral, undefined) - -import Control.Applicative (Applicative (pure)) -import Control.Exception (Exception (displayException)) -import Control.Monad (Monad, unless, when) -import Data.Bool ((&&)) -import Data.Coerce (coerce) -import Data.Either - (Either (Left, Right), either, isRight) -import Data.Eq (Eq, (==), (/=)) -import Data.Foldable (Foldable(length)) -import Data.Function (const, id, flip, ($)) -import Data.Functor (Functor, fmap) -import Data.Functor.Identity (Identity (runIdentity)) -import Data.List ((++)) -import qualified Data.List as List -import Data.Monoid (mconcat) -import Data.Ord (Ord, (<), (<=), (>), (>=)) -import Data.Proxy (Proxy (Proxy)) -import Data.Semigroup (Semigroup((<>))) -import Data.These (These(..)) -import Data.Typeable (TypeRep, Typeable, typeOf) -import Data.Void (Void) -import Text.Read (Read (readsPrec), lex, readParen) -import Text.Show (Show (show)) - -import Control.Monad.Catch (MonadThrow) -import qualified Control.Monad.Catch as MonadThrow -import Control.Monad.Error.Class (MonadError) -import qualified Control.Monad.Error.Class as MonadError -import Control.Monad.Fail (MonadFail, fail) -import Control.Monad.Fix (MonadFix, fix) -import Control.Monad.Trans.Class (MonadTrans (lift)) - -import Control.Monad.Trans.Except (ExceptT) -import qualified Control.Monad.Trans.Except as ExceptT - -import GHC.Exts (IsList(Item, toList)) -import GHC.Generics (Generic, Generic1) -import GHC.TypeLits (type (<=), KnownNat, Nat, natVal) - -import qualified Data.Text.Prettyprint.Doc as PP - -import qualified Language.Haskell.TH.Syntax as TH - --------------------------------------------------------------------------------- - --- Helper functions, --- from the 'flow' package. -infixl 0 |> -infixl 9 .> - -(|>) :: a -> (a -> b) -> b -(|>) = flip ($) -{-# INLINE (|>) #-} - -(.>) :: (a -> b) -> (b -> c) -> a -> c -f .> g = \x -> g (f x) -{-# INLINE (.>) #-} - --------------------------------------------------------------------------------- - --- | A refinement type, which wraps a value of type @x@, --- ensuring that it satisfies a type-level predicate @p@. --- --- The only ways that this library provides to construct --- a value of type 'Refined' are with the 'refine-' family --- of functions, because the use of the newtype constructor --- gets around the checking of the predicate. This restriction --- on the user makes 'unrefine' safe. --- --- If you would /really/ like to --- construct a 'Refined' value without checking the predicate, --- use 'Unsafe.Coerce.unsafeCoerce'. -newtype Refined p x = Refined x - deriving - ( Eq - , Foldable - , Ord - , Show - , Typeable - ) - -type role Refined phantom representational - -instance (Read x, Predicate p x) => Read (Refined p x) where - readsPrec d = readParen (d > 10) $ \r1 -> do - ("Refined", r2) <- lex r1 - (raw, r3) <- readsPrec 11 r2 - case refine raw of - Right val -> [(val, r3)] - Left _ -> [] - -instance (TH.Lift x) => TH.Lift (Refined p x) where - lift (Refined a) = [|Refined a|] - --------------------------------------------------------------------------------- - --- | A smart constructor of a 'Refined' value. --- Checks the input value at runtime. -refine :: (Predicate p x) => x -> Either RefineException (Refined p x) -refine x = do - let predicateByResult :: RefineM (Refined p x) -> p - predicateByResult = const undefined - runRefineM $ fix $ \result -> do - validate (predicateByResult result) x - pure (Refined x) -{-# INLINABLE refine #-} - --- | Constructs a 'Refined' value at run-time, --- calling 'Control.Monad.Catch.throwM' if the value --- does not satisfy the predicate. -refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x) -refineThrow = refine .> either MonadThrow.throwM pure -{-# INLINABLE refineThrow #-} - --- | Constructs a 'Refined' value at run-time, --- calling 'Control.Monad.Fail.fail' if the value --- does not satisfy the predicate. -refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x) -refineFail = refine .> either (displayException .> fail) pure -{-# INLINABLE refineFail #-} - --- | Constructs a 'Refined' value at run-time, --- calling 'Control.Monad.Error.throwError' if the value --- does not satisfy the predicate. -refineError :: (Predicate p x, MonadError RefineException m) - => x -> m (Refined p x) -refineError = refine .> either MonadError.throwError pure -{-# INLINABLE refineError #-} - --- | Constructs a 'Refined' value at run-time, --- calling 'Prelude.error' if the value --- does not satisfy the predicate. --- --- WARNING: this function is not total! -unsafeRefine :: (Predicate p x) => x -> Refined p x -unsafeRefine = refine .> either (displayException .> error) id -{-# INLINABLE unsafeRefine #-} - --------------------------------------------------------------------------------- - --- | Constructs a 'Refined' value at compile-time using @-XTemplateHaskell@. --- --- For example: --- --- >>> $$(refineTH 23) :: Refined Positive Int --- Refined 23 --- --- Here's an example of an invalid value: --- --- >>> $$(refineTH 0) :: Refined Positive Int --- :6:4: --- Value is not greater than 0 --- In the Template Haskell splice $$(refineTH 0) --- In the expression: $$(refineTH 0) :: Refined Positive Int --- In an equation for ‘it’: --- it = $$(refineTH 0) :: Refined Positive Int --- --- If it's not evident, the example above indicates a compile-time failure, --- which means that the checking was done at compile-time, thus introducing a --- zero runtime overhead compared to a plain value construction. -refineTH :: (Predicate p x, TH.Lift x) => x -> TH.Q (TH.TExp (Refined p x)) -refineTH = let refineByResult :: (Predicate p x) - => TH.Q (TH.TExp (Refined p x)) - -> x - -> Either RefineException (Refined p x) - refineByResult = const refine - in fix $ \loop -> refineByResult (loop undefined) - .> either (show .> fail) TH.lift - .> fmap TH.TExp - --------------------------------------------------------------------------------- - --- | Extracts the refined value. -{-# INLINE unrefine #-} -unrefine :: Refined p x -> x -unrefine = coerce - --------------------------------------------------------------------------------- - --- | A typeclass which defines a runtime interpretation of --- a type-level predicate @p@ for type @x@. -class (Typeable p) => Predicate p x where - {-# MINIMAL validate #-} - -- | Check the value @x@ according to the predicate @p@, - -- producing an error string if the value does not satisfy. - validate :: (Monad m) => p -> x -> RefineT m () - --------------------------------------------------------------------------------- - --- | The negation of a predicate. -data Not p - -instance (Predicate p x, Typeable p) => Predicate (Not p) x where - validate p x = do - result <- runRefineT (validate @p undefined x) - when (isRight result) $ do - throwRefine (RefineNotException (typeOf p)) - --------------------------------------------------------------------------------- - --- | The conjunction of two predicates. -data And l r - -infixr 3 && --- | The conjunction of two predicates. -type (&&) = And - -instance ( Predicate l x, Predicate r x, Typeable l, Typeable r - ) => Predicate (And l r) x where - validate p x = do - a <- lift $ runRefineT $ validate @l undefined x - b <- lift $ runRefineT $ validate @r undefined x - let throw err = throwRefine (RefineAndException (typeOf p) err) - case (a, b) of - (Left e, Left e1) -> throw (These e e1) - (Left e, _) -> throw (This e) - (Right _, Left e) -> throw (That e) - (Right _, Right _) -> pure () - --------------------------------------------------------------------------------- - --- | The disjunction of two predicates. -data Or l r - -infixr 2 || --- | The disjunction of two predicates. -type (||) = Or - -instance ( Predicate l x, Predicate r x, Typeable l, Typeable r - ) => Predicate (Or l r) x where - validate p x = do - left <- lift $ runRefineT $ validate @l undefined x - right <- lift $ runRefineT $ validate @r undefined x - case (left, right) of - (Left l, Left r) -> throwRefine (RefineOrException (typeOf p) l r) - _ -> pure () - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the 'Foldable' has a length --- which is less than the specified type-level number. -data SizeLessThan (n :: Nat) - -instance (Foldable t, KnownNat n) => Predicate (SizeLessThan n) (t a) where - validate p x = do - let x' = natVal p - sz = length x - unless (sz < fromIntegral x') $ do - throwRefineOtherException (typeOf p) - $ "Size of Foldable is not less than " <> PP.pretty x' <> "\n" - <> "\tSize is: " <> PP.pretty sz - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the 'Foldable' has a length --- which is greater than the specified type-level number. -data SizeGreaterThan (n :: Nat) - -instance (Foldable t, KnownNat n) => Predicate (SizeGreaterThan n) (t a) where - validate p x = do - let x' = natVal p - sz = length x - unless (sz > fromIntegral x') $ do - throwRefineOtherException (typeOf p) - $ "Size of Foldable is not greater than " <> PP.pretty x' <> "\n" - <> "\tSize is: " <> PP.pretty sz - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the 'Foldable' has a length --- which is equal to the specified type-level number. -data SizeEqualTo (n :: Nat) - -instance (Foldable t, KnownNat n) => Predicate (SizeEqualTo n) (t a) where - validate p x = do - let x' = natVal p - sz = length x - unless (sz == fromIntegral x') $ do - throwRefineOtherException (typeOf p) - $ "Size of Foldable is not equal to " <> PP.pretty x' <> "\n" - <> "\tSize is: " <> PP.pretty sz - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the 'IsList' contains elements --- in a strictly ascending order. -data Ascending - -instance (IsList t, Ord (Item t)) => Predicate Ascending t where - validate p x = do - let asList = toList x - unless (List.sort asList == asList) $ do - throwRefineOtherException (typeOf p) - $ "IsList is not in ascending order " - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the 'IsList' contains elements --- in a strictly descending order. -data Descending - -instance (IsList t, Ord (Item t)) => Predicate Descending t where - validate p x = do - let asList = toList x - unless (List.reverse (List.sort asList) == asList) $ do - throwRefineOtherException (typeOf p) - $ "IsList is not in ascending order " - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is less than the --- specified type-level number. -data LessThan (n :: Nat) - -instance (Ord x, Num x, KnownNat n) => Predicate (LessThan n) x where - validate p x = do - let x' = natVal p - unless (x < fromIntegral x') $ do - throwRefineOtherException (typeOf p) - $ "Value is not less than " <> PP.pretty x' - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is greater than the --- specified type-level number. -data GreaterThan (n :: Nat) - -instance (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x where - validate p x = do - let x' = natVal p - unless (x > fromIntegral x') $ do - throwRefineOtherException (typeOf p) - $ "Value is not greater than " <> PP.pretty x' - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is greater than or equal to the --- specified type-level number. -data From (n :: Nat) - -instance (Ord x, Num x, KnownNat n) => Predicate (From n) x where - validate p x = do - let x' = natVal p - unless (x >= fromIntegral x') $ do - throwRefineOtherException (typeOf p) - $ "Value is less than " <> PP.pretty x' - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is less than or equal to the --- specified type-level number. -data To (n :: Nat) - -instance (Ord x, Num x, KnownNat n) => Predicate (To n) x where - validate p x = do - let x' = natVal p - unless (x <= fromIntegral x') $ do - throwRefineOtherException (typeOf p) - $ "Value is greater than " <> PP.pretty x' - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is within an inclusive range. -data FromTo (mn :: Nat) (mx :: Nat) - -instance ( Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx - ) => Predicate (FromTo mn mx) x where - validate p x = do - let mn' = natVal (Proxy @mn) - let mx' = natVal (Proxy @mx) - unless ((x >= fromIntegral mn') && (x <= fromIntegral mx')) $ do - let msg = [ "Value is out of range (minimum: " - , PP.pretty mn' - , ", maximum: " - , PP.pretty mx' - , ")" - ] |> mconcat - throwRefineOtherException (typeOf p) msg - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is equal to the specified --- type-level number @n@. -data EqualTo (n :: Nat) - -instance (Eq x, Num x, KnownNat n) => Predicate (EqualTo n) x where - validate p x = do - let x' = natVal p - unless (x == fromIntegral x') $ do - throwRefineOtherException (typeOf p) - $ "Value does not equal " <> PP.pretty x' - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is not equal to the specified --- type-level number @n@. -data NotEqualTo (n :: Nat) - -instance (Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n) x where - validate p x = do - let x' = natVal p - unless (x /= fromIntegral x') $ do - throwRefineOtherException (typeOf p) - $ "Value does equal " <> PP.pretty x' - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is greater than zero. -type Positive = GreaterThan 0 - --- | A 'Predicate' ensuring that the value is less than or equal to zero. -type NonPositive = To 0 - --- | A 'Predicate' ensuring that the value is less than zero. -type Negative = LessThan 0 - --- | A 'Predicate' ensuring that the value is greater than or equal to zero. -type NonNegative = From 0 - --- | An inclusive range of values from zero to one. -type ZeroToOne = FromTo 0 1 - --- | A 'Predicate' ensuring that the value is not equal to zero. -type NonZero = NotEqualTo 0 - --- | A 'Predicate' ensuring that the 'Foldable' is non-empty. -type NonEmpty = SizeGreaterThan 0 - --------------------------------------------------------------------------------- - --- | --- A typeclass containing "safe" conversions between refined predicates --- where the target is /weaker/ than the source: that is, all values that --- satisfy the first predicate will be guarunteed to satisy the second. --- --- Take care: writing an instance declaration for your custom predicates is --- the same as an assertion that 'weaken' is safe to use: --- --- @ --- instance 'Weaken' Pred1 Pred2 --- @ --- --- For most of the instances, explicit type annotations for the result --- value's type might be required. -class Weaken from to where - weaken :: Refined from x -> Refined to x - weaken = coerce - -instance (n <= m) => Weaken (LessThan n) (LessThan m) -instance (n <= m) => Weaken (LessThan n) (To m) -instance (n <= m) => Weaken (To n) (To m) -instance (m <= n) => Weaken (GreaterThan n) (GreaterThan m) -instance (m <= n) => Weaken (GreaterThan n) (From m) -instance (m <= n) => Weaken (From n) (From m) -instance (p <= n, m <= q) => Weaken (FromTo n m) (FromTo p q) -instance (p <= n) => Weaken (FromTo n m) (From p) -instance (m <= q) => Weaken (FromTo n m) (To q) - --- | This function helps type inference. --- It is equivalent to the following: --- --- @ --- instance Weaken (And l r) l --- @ -andLeft :: Refined (And l r) x -> Refined l x -andLeft = coerce - --- | This function helps type inference. --- It is equivalent to the following: --- --- @ --- instance Weaken (And l r) r --- @ -andRight :: Refined (And l r) x -> Refined r x -andRight = coerce - --- | This function helps type inference. --- It is equivalent to the following: --- --- @ --- instance Weaken l (Or l r) --- @ -leftOr :: Refined l x -> Refined (Or l r) x -leftOr = coerce - --- | This function helps type inference. --- It is equivalent to the following: --- --- @ --- instance Weaken r (Or l r) --- @ -rightOr :: Refined r x -> Refined (Or l r) x -rightOr = coerce - --------------------------------------------------------------------------------- - --- | An exception encoding the way in which a 'Predicate' failed. -data RefineException - = -- | A 'RefineException' for failures involving the 'Not' predicate. - RefineNotException - { _RefineException_typeRep :: !TypeRep - -- ^ The 'TypeRep' of the @'Not' p@ type. - } - - | -- | A 'RefineException' for failures involving the 'And' predicate. - RefineAndException - { _RefineException_typeRep :: !TypeRep - -- ^ The 'TypeRep' of the @'And' l r@ type. - , _RefineException_andChild :: !(These RefineException RefineException) - -- ^ A 'These' encoding which branch(es) of the 'And' failed: - -- if the 'RefineException' came from the @l@ predicate, then - -- this will be 'This', if it came from the @r@ predicate, this - -- will be 'That', and if it came from both @l@ and @r@, this - -- will be 'These'. - - -- note to self: what am I, Dr. Seuss? - } - - | -- | A 'RefineException' for failures involving the 'Or' predicate. - RefineOrException - { _RefineException_typeRep :: !TypeRep - -- ^ The 'TypeRep' of the @'Or' l r@ type. - , _RefineException_orLChild :: !RefineException - -- ^ The 'RefineException' for the @l@ failure. - , _RefineException_orRChild :: !RefineException - -- ^ The 'RefineException' for the @l@ failure. - } - - | -- | A 'RefineException' for failures involving all other predicates. - RefineOtherException - { _RefineException_typeRep :: !TypeRep - -- ^ The 'TypeRep' of the predicate that failed. - , _RefineException_message :: !(PP.Doc Void) - -- ^ A custom message to display. - } - deriving (Generic) - -instance Show RefineException where - show = PP.pretty .> show - --- | Display a 'RefineException' as a @'PP.Doc' ann@ -displayRefineException :: RefineException -> PP.Doc ann -displayRefineException (RefineOtherException tr msg) - = PP.pretty ("The predicate (" ++ show tr ++ ") does not hold: \n \t" ++ show msg) -displayRefineException (RefineNotException tr) - = PP.pretty ("The negation of the predicate (" ++ show tr ++ ") does not hold.") -displayRefineException (RefineOrException tr orLChild orRChild) - = PP.pretty ("Both subpredicates failed in: (" ++ show tr ++ "). \n") - <> "\t" <> (displayRefineException orLChild) <> "\n" - <> "\t" <> (displayRefineException orRChild) <> "\n" -displayRefineException (RefineAndException tr andChild) - = PP.pretty ("The predicate (" ++ show tr ++ ") does not hold: \n \t") - <> case andChild of - This a -> "The left subpredicate does not hold:\n\t" <> displayRefineException a <> "\n" - That b -> "The right subpredicate does not hold:\n\t" <> displayRefineException b <> "\n" - These a b -> "\t Neither subpredicate holds: \n" - <> "\t" <> displayRefineException a <> "\n" - <> "\t" <> displayRefineException b <> "\n" - --- | Pretty-print a 'RefineException'. -instance PP.Pretty RefineException where - pretty = displayRefineException - --- | Encode a 'RefineException' for use with \Control.Exception\. -instance Exception RefineException where - displayException = show - --------------------------------------------------------------------------------- - --- | A monad transformer that adds @'RefineException'@s to other monads. --- --- The @'pure'@ and @'Control.Monad.return'@ functions yield computations that produce --- the given value, while @'>>='@ sequences two subcomputations, exiting --- on the first @'RefineException'@. -newtype RefineT m a - = RefineT (ExceptT RefineException m a) - deriving ( Functor, Applicative, Monad, MonadFix - , MonadError RefineException, MonadTrans - , Generic, Generic1 - ) - --- | The inverse of @'RefineT'@. -runRefineT - :: RefineT m a - -> m (Either RefineException a) -runRefineT = coerce .> ExceptT.runExceptT - --- | Map the unwrapped computation using the given function. --- --- @'runRefineT' ('mapRefineT' f m) = f ('runRefineT' m)@ -mapRefineT - :: (m (Either RefineException a) -> n (Either RefineException b)) - -> RefineT m a - -> RefineT n b -mapRefineT f = coerce .> ExceptT.mapExceptT f .> coerce - --------------------------------------------------------------------------------- - --- | @'RefineM' a@ is equivalent to @'RefineT' 'Identity' a@ for any type @a@. -type RefineM a = RefineT Identity a - --- | Constructs a computation in the 'RefineM' monad. (The inverse of @'runRefineM'@). -refineM - :: Either RefineException a - -> RefineM a -refineM = ExceptT.except .> coerce - --- | Run a monadic action of type @'RefineM' a@, --- yielding an @'Either' 'RefineException' a@. --- --- This is just defined as @'runIdentity' '.' 'runRefineT'@. -runRefineM - :: RefineM a - -> Either RefineException a -runRefineM = runRefineT .> runIdentity - --------------------------------------------------------------------------------- - --- | One can use @'throwRefine'@ inside of a monadic --- context to begin processing a @'RefineException'@. -throwRefine - :: (Monad m) - => RefineException - -> RefineT m a -throwRefine = MonadError.throwError - --- | A handler function to handle previous @'RefineException'@s --- and return to normal execution. A common idiom is: --- --- @ do { action1; action2; action3 } `'catchRefine'` handler @ --- --- where the action functions can call @'throwRefine'@. Note that --- handler and the do-block must have the same return type. -catchRefine - :: (Monad m) - => RefineT m a - -> (RefineException -> RefineT m a) - -> RefineT m a -catchRefine = MonadError.catchError - --- | A handler for a @'RefineException'@. --- --- 'throwRefineOtherException' is useful for defining what --- behaviour 'validate' should have in the event of a predicate failure. -throwRefineOtherException - :: (Monad m) - => TypeRep - -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeOf'. - -> PP.Doc Void - -- ^ A 'PP.Doc' 'Void' encoding a custom error message to be pretty-printed. - -> RefineT m a -throwRefineOtherException rep - = RefineOtherException rep .> throwRefine +import Refined.Internal --------------------------------------------------------------------------------- +------------------------------------------------------------------------------- diff --git a/library/Refined/Internal.hs b/library/Refined/Internal.hs new file mode 100644 --- /dev/null +++ b/library/Refined/Internal.hs @@ -0,0 +1,835 @@ +-------------------------------------------------------------------------------- + +-- Copyright © 2015 Nikita Volkov +-- Copyright © 2018 Remy Goldschmidt +-- Copyright © 2018 Daniel Cartwright +-- +-- Permission is hereby granted, free of charge, to any person +-- obtaining a copy of this software and associated documentation +-- files (the "Software"), to deal in the Software without +-- restriction, including without limitation the rights to use, +-- copy, modify, merge, publish, distribute, sublicense, and/or sell +-- copies of the Software, and to permit persons to whom the +-- Software is furnished to do so, subject to the following +-- conditions: +-- +-- The above copyright notice and this permission notice shall be +-- included in all copies or substantial portions of the Software. +-- +-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES +-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT +-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, +-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR +-- OTHER DEALINGS IN THE SOFTWARE. + +-------------------------------------------------------------------------------- + +{-# OPTIONS_GHC -Wall #-} +{-# OPTIONS_GHC -funbox-strict-fields #-} + +-------------------------------------------------------------------------------- + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +-------------------------------------------------------------------------------- + +-- | In type theory, a refinement type is a type endowed +-- with a predicate which is assumed to hold for any element +-- of the refined type. +-- +-- This library allows one to capture the idea of a refinement type +-- using the 'Refined' type. A 'Refined' @p@ @x@ wraps a value +-- of type @x@, ensuring that it satisfies a type-level predicate @p@. +-- +-- A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/ +-- +module Refined.Internal + ( -- * 'Refined' + Refined(Refined) + + -- ** Creation + , refine + , refineThrow + , refineFail + , refineError + , refineTH + + -- ** Consumption + , unrefine + + -- * 'Predicate' + , Predicate (validate) + + -- * Logical predicates + , Not + , And + , type (&&) + , Or + , type (||) + + -- * Identity predicate + , IdPred + + -- * Numeric predicates + , LessThan + , GreaterThan + , From + , To + , FromTo + , EqualTo + , NotEqualTo + , Positive + , NonPositive + , Negative + , NonNegative + , ZeroToOne + , NonZero + + -- * Foldable predicates + , SizeLessThan + , SizeGreaterThan + , SizeEqualTo + , NonEmpty + + -- * IsList predicates + , Ascending + , Descending + + -- * Weakening + , Weaken (weaken) + , andLeft + , andRight + , leftOr + , rightOr + + -- * Error handling + + -- ** 'RefineException' + , RefineException + ( RefineNotException + , RefineAndException + , RefineOrException + , RefineOtherException + ) + , displayRefineException + + -- ** 'RefineT' and 'RefineM' + , RefineT, runRefineT, mapRefineT + , RefineM, refineM, runRefineM + , throwRefine, catchRefine + , throwRefineOtherException + + , (|>) + , (.>) + ) where + +-------------------------------------------------------------------------------- + +import Prelude + (Num, fromIntegral, undefined) + +import Control.Applicative (Applicative (pure)) +import Control.Exception (Exception (displayException)) +import Control.Monad (Monad, unless, when) +import Data.Bool (Bool(True,False),(&&), otherwise) +import Data.Coerce (coerce) +import Data.Either + (Either (Left, Right), either, isRight) +import Data.Eq (Eq, (==), (/=)) +import Data.Foldable (Foldable(length, foldl')) +import Data.Function (const, flip, ($), (.)) +import Data.Functor (Functor, fmap) +import Data.Functor.Identity (Identity (runIdentity)) +import Data.List ((++)) +import Data.Monoid (mconcat) +import Data.Ord (Ord, (<), (<=), (>), (>=)) +import Data.Proxy (Proxy (Proxy)) +import Data.Semigroup (Semigroup((<>))) +import Data.Typeable (TypeRep, Typeable, typeOf) +import Data.Void (Void) +import Text.Read (Read (readsPrec), lex, readParen) +import Text.Show (Show (show)) + +import Control.Monad.Catch (MonadThrow) +import qualified Control.Monad.Catch as MonadThrow +import Control.Monad.Error.Class (MonadError) +import qualified Control.Monad.Error.Class as MonadError +import Control.Monad.Fail (MonadFail, fail) +import Control.Monad.Fix (MonadFix, fix) +import Control.Monad.Trans.Class (MonadTrans (lift)) + +import Control.Monad.Trans.Except (ExceptT) +import qualified Control.Monad.Trans.Except as ExceptT + +import GHC.Generics (Generic, Generic1) +import GHC.TypeLits (type (<=), KnownNat, Nat, natVal) + +import Refined.These (These(This,That,These)) + +import qualified Data.Text.Prettyprint.Doc as PP +import qualified Language.Haskell.TH.Syntax as TH + +-------------------------------------------------------------------------------- + +infixl 0 |> +infixl 9 .> + +-- | Helper function, stolen from the 'flow' package. +(|>) :: a -> (a -> b) -> b +(|>) = flip ($) +{-# INLINE (|>) #-} + +-- | Helper function, stolen from the 'flow' package. +(.>) :: (a -> b) -> (b -> c) -> a -> c +f .> g = \x -> g (f x) +{-# INLINE (.>) #-} + +-- | FIXME: doc +data Ordered a = Empty | Decreasing a | Increasing a + +-- | FIXME: doc +inc :: Ordered a -> Bool +inc (Decreasing _) = False +inc _ = True +{-# INLINE inc #-} + +-- | FIXME: doc +dec :: Ordered a -> Bool +dec (Increasing _) = False +dec _ = True +{-# INLINE dec #-} + +increasing :: (Foldable t, Ord a) => t a -> Bool +increasing = inc . foldl' go Empty where + go Empty y = Increasing y + go (Decreasing x) _ = Decreasing x + go (Increasing x) y + | x <= y = Increasing y + | otherwise = Decreasing y +{-# INLINABLE increasing #-} + +decreasing :: (Foldable t, Ord a) => t a -> Bool +decreasing = dec . foldl' go Empty where + go Empty y = Decreasing y + go (Increasing x) _ = Increasing x + go (Decreasing x) y + | x >= y = Decreasing y + | otherwise = Increasing y +{-# INLINABLE decreasing #-} + +-------------------------------------------------------------------------------- + +-- | A refinement type, which wraps a value of type @x@, +-- ensuring that it satisfies a type-level predicate @p@. +newtype Refined p x = Refined x + deriving (Eq, Foldable , Ord, Show, Typeable) + +type role Refined nominal nominal + +-- | This instance makes sure to check the refinement. +instance (Read x, Predicate p x) => Read (Refined p x) where + readsPrec d = readParen (d > 10) $ \r1 -> do + ("Refined", r2) <- lex r1 + (raw, r3) <- readsPrec 11 r2 + case refine raw of + Right val -> [(val, r3)] + Left _ -> [] + +instance (TH.Lift x) => TH.Lift (Refined p x) where + lift (Refined a) = [|Refined a|] + +-------------------------------------------------------------------------------- + +-- | A smart constructor of a 'Refined' value. +-- Checks the input value at runtime. +refine :: (Predicate p x) => x -> Either RefineException (Refined p x) +refine x = do + let predicateByResult :: RefineM (Refined p x) -> p + predicateByResult = const undefined + runRefineM $ fix $ \result -> do + validate (predicateByResult result) x + pure (Refined x) +{-# INLINABLE refine #-} + +-- | Constructs a 'Refined' value at run-time, +-- calling 'Control.Monad.Catch.throwM' if the value +-- does not satisfy the predicate. +refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x) +refineThrow = refine .> either MonadThrow.throwM pure +{-# INLINABLE refineThrow #-} + +-- | Constructs a 'Refined' value at run-time, +-- calling 'Control.Monad.Fail.fail' if the value +-- does not satisfy the predicate. +refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x) +refineFail = refine .> either (displayException .> fail) pure +{-# INLINABLE refineFail #-} + +-- | Constructs a 'Refined' value at run-time, +-- calling 'Control.Monad.Error.throwError' if the value +-- does not satisfy the predicate. +refineError :: (Predicate p x, MonadError RefineException m) + => x -> m (Refined p x) +refineError = refine .> either MonadError.throwError pure +{-# INLINABLE refineError #-} + +-------------------------------------------------------------------------------- + +-- | Constructs a 'Refined' value at compile-time using @-XTemplateHaskell@. +-- +-- For example: +-- +-- >>> $$(refineTH 23) :: Refined Positive Int +-- Refined 23 +-- +-- Here's an example of an invalid value: +-- +-- >>> $$(refineTH 0) :: Refined Positive Int +-- :6:4: +-- Value is not greater than 0 +-- In the Template Haskell splice $$(refineTH 0) +-- In the expression: $$(refineTH 0) :: Refined Positive Int +-- In an equation for ‘it’: +-- it = $$(refineTH 0) :: Refined Positive Int +-- +-- If it's not evident, the example above indicates a compile-time failure, +-- which means that the checking was done at compile-time, thus introducing a +-- zero runtime overhead compared to a plain value construction. +-- +-- It may be useful to use this function with the `th-lift-instances` package at https://hackage.haskell.org/package/th-lift-instances/ +refineTH :: (Predicate p x, TH.Lift x) => x -> TH.Q (TH.TExp (Refined p x)) +refineTH = let refineByResult :: (Predicate p x) + => TH.Q (TH.TExp (Refined p x)) + -> x + -> Either RefineException (Refined p x) + refineByResult = const refine + in fix $ \loop -> refineByResult (loop undefined) + .> either (show .> fail) TH.lift + .> fmap TH.TExp + +-------------------------------------------------------------------------------- + +-- | Extracts the refined value. +{-# INLINE unrefine #-} +unrefine :: Refined p x -> x +unrefine = coerce + +-------------------------------------------------------------------------------- + +-- | A typeclass which defines a runtime interpretation of +-- a type-level predicate @p@ for type @x@. +class (Typeable p) => Predicate p x where + {-# MINIMAL validate #-} + -- | Check the value @x@ according to the predicate @p@, + -- producing an error string if the value does not satisfy. + validate :: (Monad m) => p -> x -> RefineT m () + +-------------------------------------------------------------------------------- + +-- | A predicate which is satisfied for all types. +data IdPred + deriving (Generic) + +instance Predicate IdPred x where + validate _ _ = pure () + +-------------------------------------------------------------------------------- + +-- | The negation of a predicate. +data Not p + deriving (Generic, Generic1) + +instance (Predicate p x, Typeable p) => Predicate (Not p) x where + validate p x = do + result <- runRefineT (validate @p undefined x) + when (isRight result) $ do + throwRefine (RefineNotException (typeOf p)) + +-------------------------------------------------------------------------------- + +-- | The conjunction of two predicates. +data And l r + deriving (Generic, Generic1) + +infixr 3 && +-- | The conjunction of two predicates. +type (&&) = And + +instance ( Predicate l x, Predicate r x, Typeable l, Typeable r + ) => Predicate (And l r) x where + validate p x = do + a <- lift $ runRefineT $ validate @l undefined x + b <- lift $ runRefineT $ validate @r undefined x + let throw err = throwRefine (RefineAndException (typeOf p) err) + case (a, b) of + (Left e, Left e1) -> throw (These e e1) + (Left e, _) -> throw (This e) + (Right _, Left e) -> throw (That e) + (Right _, Right _) -> pure () + +-------------------------------------------------------------------------------- + +-- | The disjunction of two predicates. +data Or l r + deriving (Generic, Generic1) + +infixr 2 || +-- | The disjunction of two predicates. +type (||) = Or + +instance ( Predicate l x, Predicate r x, Typeable l, Typeable r + ) => Predicate (Or l r) x where + validate p x = do + left <- lift $ runRefineT $ validate @l undefined x + right <- lift $ runRefineT $ validate @r undefined x + case (left, right) of + (Left l, Left r) -> throwRefine (RefineOrException (typeOf p) l r) + _ -> pure () + +-------------------------------------------------------------------------------- + +-- | A 'Predicate' ensuring that the 'Foldable' has a length +-- which is less than the specified type-level number. +data SizeLessThan (n :: Nat) + deriving (Generic) + +instance (Foldable t, KnownNat n) => Predicate (SizeLessThan n) (t a) where + validate p x = do + let x' = natVal p + sz = length x + unless (sz < fromIntegral x') $ do + throwRefineOtherException (typeOf p) + $ "Size of Foldable is not less than " <> PP.pretty x' <> "\n" + <> "\tSize is: " <> PP.pretty sz + +-------------------------------------------------------------------------------- + +-- | A 'Predicate' ensuring that the 'Foldable' has a length +-- which is greater than the specified type-level number. +data SizeGreaterThan (n :: Nat) + deriving (Generic) + +instance (Foldable t, KnownNat n) => Predicate (SizeGreaterThan n) (t a) where + validate p x = do + let x' = natVal p + sz = length x + unless (sz > fromIntegral x') $ do + throwRefineOtherException (typeOf p) + $ "Size of Foldable is not greater than " <> PP.pretty x' <> "\n" + <> "\tSize is: " <> PP.pretty sz + +-------------------------------------------------------------------------------- + +-- | A 'Predicate' ensuring that the 'Foldable' has a length +-- which is equal to the specified type-level number. +data SizeEqualTo (n :: Nat) + deriving (Generic) + +instance (Foldable t, KnownNat n) => Predicate (SizeEqualTo n) (t a) where + validate p x = do + let x' = natVal p + sz = length x + unless (sz == fromIntegral x') $ do + throwRefineOtherException (typeOf p) + $ "Size of Foldable is not equal to " <> PP.pretty x' <> "\n" + <> "\tSize is: " <> PP.pretty sz + +-------------------------------------------------------------------------------- + +-- | A 'Predicate' ensuring that the 'Foldable' contains elements +-- in a strictly ascending order. +data Ascending + deriving (Generic) + +instance (Foldable t, Ord a) => Predicate Ascending (t a) where + validate p x = do + unless (increasing x) $ do + throwRefineOtherException (typeOf p) + $ "Foldable is not in ascending order " + +-------------------------------------------------------------------------------- + +-- | A 'Predicate' ensuring that the 'Foldable' contains elements +-- in a strictly descending order. +data Descending + deriving (Generic) + +instance (Foldable t, Ord a) => Predicate Descending (t a) where + validate p x = do + unless (decreasing x) $ do + throwRefineOtherException (typeOf p) + $ "Foldable is not in descending order " + +-------------------------------------------------------------------------------- + +-- | A 'Predicate' ensuring that the value is less than the +-- specified type-level number. +data LessThan (n :: Nat) + deriving (Generic) + +instance (Ord x, Num x, KnownNat n) => Predicate (LessThan n) x where + validate p x = do + let x' = natVal p + unless (x < fromIntegral x') $ do + throwRefineOtherException (typeOf p) + $ "Value is not less than " <> PP.pretty x' + +-------------------------------------------------------------------------------- + +-- | A 'Predicate' ensuring that the value is greater than the +-- specified type-level number. +data GreaterThan (n :: Nat) + deriving (Generic) + +instance (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x where + validate p x = do + let x' = natVal p + unless (x > fromIntegral x') $ do + throwRefineOtherException (typeOf p) + $ "Value is not greater than " <> PP.pretty x' + +-------------------------------------------------------------------------------- + +-- | A 'Predicate' ensuring that the value is greater than or equal to the +-- specified type-level number. +data From (n :: Nat) + deriving (Generic) + +instance (Ord x, Num x, KnownNat n) => Predicate (From n) x where + validate p x = do + let x' = natVal p + unless (x >= fromIntegral x') $ do + throwRefineOtherException (typeOf p) + $ "Value is less than " <> PP.pretty x' + +-------------------------------------------------------------------------------- + +-- | A 'Predicate' ensuring that the value is less than or equal to the +-- specified type-level number. +data To (n :: Nat) + deriving (Generic) + +instance (Ord x, Num x, KnownNat n) => Predicate (To n) x where + validate p x = do + let x' = natVal p + unless (x <= fromIntegral x') $ do + throwRefineOtherException (typeOf p) + $ "Value is greater than " <> PP.pretty x' + +-------------------------------------------------------------------------------- + +-- | A 'Predicate' ensuring that the value is within an inclusive range. +data FromTo (mn :: Nat) (mx :: Nat) + deriving (Generic) + +instance ( Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx + ) => Predicate (FromTo mn mx) x where + validate p x = do + let mn' = natVal (Proxy @mn) + let mx' = natVal (Proxy @mx) + unless ((x >= fromIntegral mn') && (x <= fromIntegral mx')) $ do + let msg = [ "Value is out of range (minimum: " + , PP.pretty mn' + , ", maximum: " + , PP.pretty mx' + , ")" + ] |> mconcat + throwRefineOtherException (typeOf p) msg + +-------------------------------------------------------------------------------- + +-- | A 'Predicate' ensuring that the value is equal to the specified +-- type-level number @n@. +data EqualTo (n :: Nat) + deriving (Generic) + +instance (Eq x, Num x, KnownNat n) => Predicate (EqualTo n) x where + validate p x = do + let x' = natVal p + unless (x == fromIntegral x') $ do + throwRefineOtherException (typeOf p) + $ "Value does not equal " <> PP.pretty x' + +-------------------------------------------------------------------------------- + +-- | A 'Predicate' ensuring that the value is not equal to the specified +-- type-level number @n@. +data NotEqualTo (n :: Nat) + deriving (Generic) + +instance (Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n) x where + validate p x = do + let x' = natVal p + unless (x /= fromIntegral x') $ do + throwRefineOtherException (typeOf p) + $ "Value does equal " <> PP.pretty x' + +-------------------------------------------------------------------------------- + +-- | A 'Predicate' ensuring that the value is greater than zero. +type Positive = GreaterThan 0 + +-- | A 'Predicate' ensuring that the value is less than or equal to zero. +type NonPositive = To 0 + +-- | A 'Predicate' ensuring that the value is less than zero. +type Negative = LessThan 0 + +-- | A 'Predicate' ensuring that the value is greater than or equal to zero. +type NonNegative = From 0 + +-- | An inclusive range of values from zero to one. +type ZeroToOne = FromTo 0 1 + +-- | A 'Predicate' ensuring that the value is not equal to zero. +type NonZero = NotEqualTo 0 + +-- | A 'Predicate' ensuring that the 'Foldable' is non-empty. +type NonEmpty = SizeGreaterThan 0 + +-------------------------------------------------------------------------------- + +-- | +-- A typeclass containing "safe" conversions between refined predicates +-- where the target is /weaker/ than the source: that is, all values that +-- satisfy the first predicate will be guarunteed to satisy the second. +-- +-- Take care: writing an instance declaration for your custom predicates is +-- the same as an assertion that 'weaken' is safe to use: +-- +-- @ +-- instance 'Weaken' Pred1 Pred2 +-- @ +-- +-- For most of the instances, explicit type annotations for the result +-- value's type might be required. +class Weaken from to where + weaken :: Refined from x -> Refined to x + weaken = coerce + +instance (n <= m) => Weaken (LessThan n) (LessThan m) +instance (n <= m) => Weaken (LessThan n) (To m) +instance (n <= m) => Weaken (To n) (To m) +instance (m <= n) => Weaken (GreaterThan n) (GreaterThan m) +instance (m <= n) => Weaken (GreaterThan n) (From m) +instance (m <= n) => Weaken (From n) (From m) +instance (p <= n, m <= q) => Weaken (FromTo n m) (FromTo p q) +instance (p <= n) => Weaken (FromTo n m) (From p) +instance (m <= q) => Weaken (FromTo n m) (To q) + +-- | This function helps type inference. +-- It is equivalent to the following: +-- +-- @ +-- instance Weaken (And l r) l +-- @ +andLeft :: Refined (And l r) x -> Refined l x +andLeft = coerce + +-- | This function helps type inference. +-- It is equivalent to the following: +-- +-- @ +-- instance Weaken (And l r) r +-- @ +andRight :: Refined (And l r) x -> Refined r x +andRight = coerce + +-- | This function helps type inference. +-- It is equivalent to the following: +-- +-- @ +-- instance Weaken l (Or l r) +-- @ +leftOr :: Refined l x -> Refined (Or l r) x +leftOr = coerce + +-- | This function helps type inference. +-- It is equivalent to the following: +-- +-- @ +-- instance Weaken r (Or l r) +-- @ +rightOr :: Refined r x -> Refined (Or l r) x +rightOr = coerce + +-------------------------------------------------------------------------------- + +-- | An exception encoding the way in which a 'Predicate' failed. +data RefineException + = -- | A 'RefineException' for failures involving the 'Not' predicate. + RefineNotException + { _RefineException_typeRep :: !TypeRep + -- ^ The 'TypeRep' of the @'Not' p@ type. + } + + | -- | A 'RefineException' for failures involving the 'And' predicate. + RefineAndException + { _RefineException_typeRep :: !TypeRep + -- ^ The 'TypeRep' of the @'And' l r@ type. + , _RefineException_andChild :: !(These RefineException RefineException) + -- ^ A 'These' encoding which branch(es) of the 'And' failed: + -- if the 'RefineException' came from the @l@ predicate, then + -- this will be 'This', if it came from the @r@ predicate, this + -- will be 'That', and if it came from both @l@ and @r@, this + -- will be 'These'. + + -- note to self: what am I, Dr. Seuss? + } + + | -- | A 'RefineException' for failures involving the 'Or' predicate. + RefineOrException + { _RefineException_typeRep :: !TypeRep + -- ^ The 'TypeRep' of the @'Or' l r@ type. + , _RefineException_orLChild :: !RefineException + -- ^ The 'RefineException' for the @l@ failure. + , _RefineException_orRChild :: !RefineException + -- ^ The 'RefineException' for the @l@ failure. + } + + | -- | A 'RefineException' for failures involving all other predicates. + RefineOtherException + { _RefineException_typeRep :: !TypeRep + -- ^ The 'TypeRep' of the predicate that failed. + , _RefineException_message :: !(PP.Doc Void) + -- ^ A custom message to display. + } + deriving (Generic) + +instance Show RefineException where + show = PP.pretty .> show + +-- | Display a 'RefineException' as a @'PP.Doc' ann@ +displayRefineException :: RefineException -> PP.Doc ann +displayRefineException (RefineOtherException tr msg) + = PP.pretty ("The predicate (" ++ show tr ++ ") does not hold: \n \t" ++ show msg) +displayRefineException (RefineNotException tr) + = PP.pretty ("The negation of the predicate (" ++ show tr ++ ") does not hold.") +displayRefineException (RefineOrException tr orLChild orRChild) + = PP.pretty ("Both subpredicates failed in: (" ++ show tr ++ "). \n") + <> "\t" <> (displayRefineException orLChild) <> "\n" + <> "\t" <> (displayRefineException orRChild) <> "\n" +displayRefineException (RefineAndException tr andChild) + = PP.pretty ("The predicate (" ++ show tr ++ ") does not hold: \n \t") + <> case andChild of + This a -> "The left subpredicate does not hold:\n\t" <> displayRefineException a <> "\n" + That b -> "The right subpredicate does not hold:\n\t" <> displayRefineException b <> "\n" + These a b -> "\t Neither subpredicate holds: \n" + <> "\t" <> displayRefineException a <> "\n" + <> "\t" <> displayRefineException b <> "\n" + +-- | Pretty-print a 'RefineException'. +instance PP.Pretty RefineException where + pretty = displayRefineException + +-- | Encode a 'RefineException' for use with \Control.Exception\. +instance Exception RefineException where + displayException = show + +-------------------------------------------------------------------------------- + +-- | A monad transformer that adds @'RefineException'@s to other monads. +-- +-- The @'pure'@ and @'Control.Monad.return'@ functions yield computations that produce +-- the given value, while @'>>='@ sequences two subcomputations, exiting +-- on the first @'RefineException'@. +newtype RefineT m a + = RefineT (ExceptT RefineException m a) + deriving ( Functor, Applicative, Monad, MonadFix + , MonadError RefineException, MonadTrans + , Generic, Generic1 + ) + +-- | The inverse of @'RefineT'@. +runRefineT + :: RefineT m a + -> m (Either RefineException a) +runRefineT = coerce .> ExceptT.runExceptT + +-- | Map the unwrapped computation using the given function. +-- +-- @'runRefineT' ('mapRefineT' f m) = f ('runRefineT' m)@ +mapRefineT + :: (m (Either RefineException a) -> n (Either RefineException b)) + -> RefineT m a + -> RefineT n b +mapRefineT f = coerce .> ExceptT.mapExceptT f .> coerce + +-------------------------------------------------------------------------------- + +-- | @'RefineM' a@ is equivalent to @'RefineT' 'Identity' a@ for any type @a@. +type RefineM a = RefineT Identity a + +-- | Constructs a computation in the 'RefineM' monad. (The inverse of @'runRefineM'@). +refineM + :: Either RefineException a + -> RefineM a +refineM = ExceptT.except .> coerce + +-- | Run a monadic action of type @'RefineM' a@, +-- yielding an @'Either' 'RefineException' a@. +-- +-- This is just defined as @'runIdentity' '.' 'runRefineT'@. +runRefineM + :: RefineM a + -> Either RefineException a +runRefineM = runRefineT .> runIdentity + +-------------------------------------------------------------------------------- + +-- | One can use @'throwRefine'@ inside of a monadic +-- context to begin processing a @'RefineException'@. +throwRefine + :: (Monad m) + => RefineException + -> RefineT m a +throwRefine = MonadError.throwError + +-- | A handler function to handle previous @'RefineException'@s +-- and return to normal execution. A common idiom is: +-- +-- @ do { action1; action2; action3 } `'catchRefine'` handler @ +-- +-- where the action functions can call @'throwRefine'@. Note that +-- handler and the do-block must have the same return type. +catchRefine + :: (Monad m) + => RefineT m a + -> (RefineException -> RefineT m a) + -> RefineT m a +catchRefine = MonadError.catchError + +-- | A handler for a @'RefineException'@. +-- +-- 'throwRefineOtherException' is useful for defining what +-- behaviour 'validate' should have in the event of a predicate failure. +throwRefineOtherException + :: (Monad m) + => TypeRep + -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeOf'. + -> PP.Doc Void + -- ^ A 'PP.Doc' 'Void' encoding a custom error message to be pretty-printed. + -> RefineT m a +throwRefineOtherException rep + = RefineOtherException rep .> throwRefine + +-------------------------------------------------------------------------------- diff --git a/library/Refined/TH.hs b/library/Refined/TH.hs deleted file mode 100644 --- a/library/Refined/TH.hs +++ /dev/null @@ -1,41 +0,0 @@ --------------------------------------------------------------------------------- - -{-# LANGUAGE DeriveLift #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TemplateHaskell #-} - --------------------------------------------------------------------------------- - -{-| This module contains orphan 'Lift' instances of types in common libraries - such as 'containers', for more available compile-time checking of predicates. - --} - -module Refined.TH () where - --------------------------------------------------------------------------------- - -import Data.IntMap.Internal (IntMap(..)) -import Data.Map.Internal (Map(..)) -import Data.Sequence.Internal (Digit(..), Elem(..), FingerTree(..), Node(..), Seq(..), ViewL(..), ViewR(..)) -import Data.Set.Internal (Set(..)) -import Data.Tree (Tree(..)) - -import Language.Haskell.TH.Syntax (Lift) - --------------------------------------------------------------------------------- - --- [containers] -deriving instance (Lift a) => Lift (IntMap a) -deriving instance (Lift k, Lift v) => Lift (Map k v) -deriving instance (Lift v) => Lift (Set v) -deriving instance (Lift a) => Lift (Elem a) -deriving instance (Lift a) => Lift (Node a) -deriving instance (Lift a) => Lift (Digit a) -deriving instance (Lift a) => Lift (FingerTree a) -deriving instance (Lift a) => Lift (Seq a) -deriving instance (Lift a) => Lift (ViewL a) -deriving instance (Lift a) => Lift (ViewR a) -deriving instance (Lift a) => Lift (Tree a) - --------------------------------------------------------------------------------- diff --git a/library/Refined/These.hs b/library/Refined/These.hs new file mode 100644 --- /dev/null +++ b/library/Refined/These.hs @@ -0,0 +1,264 @@ +-------------------------------------------------------------------------------- + +-- Copyright © 2015 Nikita Volkov +-- Copyright © 2018 Remy Goldschmidt +-- Copyright © 2018 Daniel Cartwright +-- +-- Permission is hereby granted, free of charge, to any person +-- obtaining a copy of this software and associated documentation +-- files (the "Software"), to deal in the Software without +-- restriction, including without limitation the rights to use, +-- copy, modify, merge, publish, distribute, sublicense, and/or sell +-- copies of the Software, and to permit persons to whom the +-- Software is furnished to do so, subject to the following +-- conditions: +-- +-- The above copyright notice and this permission notice shall be +-- included in all copies or substantial portions of the Software. +-- +-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES +-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT +-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, +-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR +-- OTHER DEALINGS IN THE SOFTWARE. + +-------------------------------------------------------------------------------- + +{-# OPTIONS_GHC -Wall #-} + +-------------------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE InstanceSigs #-} + +-------------------------------------------------------------------------------- + +-- | This module is defined internally to avoid using the 'these' +-- package, which brings in a lot of very heavy and unnecessary +-- transitive dependencies. We export the type and constructors +-- here, in case a user should need it. +-- We provide a small API for working with the 'These' type here. +-- If one should need a fuller API, see https://hackage.haskell.org/package/these +-- Converting to/from the two types should be trivial, as the +-- data constructors are exported from both. +module Refined.These + ( + -- * 'These' type + These(This, That, These) + + -- * Consumption + , these + , fromThese + , mergeThese + , mergeTheseWith + + -- * Traversals + , here, there + + -- * Case selections + , justThis + , justThat + , justThese + + , catThis + , catThat + , catThese + + , partitionThese + + -- * Case predicates + , isThis + , isThat + , isThese + + -- * Map operations + , mapThese + , mapThis + , mapThat + ) where + +-------------------------------------------------------------------------------- + +import Control.DeepSeq (NFData(rnf)) +#if MIN_VERSION_base(4,10,0) +import Data.Bifoldable (Bifoldable(bifold, bifoldr, bifoldl)) +#endif +#if MIN_VERSION_base(4,8,0) +import Data.Bifunctor (Bifunctor(bimap, first, second)) +#endif +import Data.Data (Data) +import Data.Maybe (isJust, mapMaybe) +import Data.Semigroup (Semigroup((<>))) +import Data.Typeable (Typeable) +import GHC.Generics (Generic, Generic1) + +-- | This is defined internally to avoid using the 'these' +-- package, which brings in a lot of very heavy and unnecessary +-- transitive dependencies. We export the type and constructors +-- here, in case a user should need it. +data These a b = This a | That b | These a b + deriving (Eq, Ord, Read, Show, Typeable, Data, Generic, Generic1) + +-- | Case analysis for the 'These' type. +these :: (a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c +these l _ _ (This a) = l a +these _ r _ (That x) = r x +these _ _ lr (These a x) = lr a x + +-- | Takes two default values and produces a tuple. +fromThese :: a -> b -> These a b -> (a, b) +fromThese _ x (This a ) = (a, x) +fromThese a _ (That x ) = (a, x) +fromThese _ _ (These a x) = (a, x) + +-- | Coalesce with the provided operation. +mergeThese :: (a -> a -> a) -> These a a -> a +mergeThese = these id id + +-- | BiMap and coalesce results with the provided operation. +mergeTheseWith :: (a -> c) -> (b -> c) -> (c -> c -> c) -> These a b -> c +mergeTheseWith f g op t = mergeThese op $ mapThese f g t + +-- | A @Traversal@ of the first half of a 'These', suitable for use with @Control.Lens@. +here :: (Applicative f) => (a -> f b) -> These a t -> f (These b t) +here f (This x) = This <$> f x +here f (These x y) = flip These y <$> f x +here _ (That x) = pure (That x) + +-- | A @Traversal@ of the second half of a 'These', suitable for use with @Control.Lens@. +there :: (Applicative f) => (a -> f b) -> These t a -> f (These t b) +there _ (This x) = pure (This x) +there f (These x y) = These x <$> f y +there f (That x) = That <$> f x + +-- | @'justThis' = 'these' 'Just' (\_ -> 'Nothing') (\_ _ -> 'Nothing')@ +justThis :: These a b -> Maybe a +justThis = these Just (\_ -> Nothing) (\_ _ -> Nothing) + +-- | @'justThat' = 'these' (\_ -> 'Nothing') 'Just' (\_ _ -> 'Nothing')@ +justThat :: These a b -> Maybe b +justThat = these (\_ -> Nothing) Just (\_ _ -> Nothing) + +-- | @'justThese' = 'these' (\_ -> 'Nothing') (\_ -> 'Nothing') (\a b -> 'Just' (a, b))@ +justThese :: These a b -> Maybe (a, b) +justThese = these (\_ -> Nothing) (\_ -> Nothing) (\a b -> Just (a, b)) + +isThis, isThat, isThese :: These a b -> Bool +-- | @'isThis' = 'isJust' . 'justThis'@ +isThis = isJust . justThis + +-- | @'isThat' = 'isJust' . 'justThat'@ +isThat = isJust . justThat + +-- | @'isThese' = 'isJust' . 'justThese'@ +isThese = isJust . justThese + +-- | 'Bifunctor' map. +mapThese :: (a -> c) -> (b -> d) -> These a b -> These c d +mapThese f _ (This a ) = This (f a) +mapThese _ g (That x) = That (g x) +mapThese f g (These a x) = These (f a) (g x) + +-- | @'mapThis' = over 'here'@ +mapThis :: (a -> c) -> These a b -> These c b +mapThis f = mapThese f id + +-- | @'mapThat' = over 'there'@ +mapThat :: (b -> d) -> These a b -> These a d +mapThat f = mapThese id f + +-- | Select all 'This' constructors from a list. +catThis :: [These a b] -> [a] +catThis = mapMaybe justThis + +-- | Select all 'That' constructors from a list. +catThat :: [These a b] -> [b] +catThat = mapMaybe justThat + +-- | Select all 'These' constructors from a list. +catThese :: [These a b] -> [(a, b)] +catThese = mapMaybe justThese + +-- | Select each constructor and partition them into separate lists. +partitionThese :: [These a b] -> ( [(a, b)], ([a], [b]) ) +partitionThese [] = ([], ([], [])) +partitionThese (These x y:xs) = first ((x, y):) $ partitionThese xs +partitionThese (This x :xs) = second (first (x:)) $ partitionThese xs +partitionThese (That y:xs) = second (second (y:)) $ partitionThese xs + +instance (Semigroup a, Semigroup b) => Semigroup (These a b) where + This a <> This b = This (a <> b) + This a <> That y = These a y + This a <> These b y = These (a <> b) y + That x <> This b = These b x + That x <> That y = That (x <> y) + That x <> These b y = These b (x <> y) + These a x <> This b = These (a <> b) x + These a x <> That y = These a (x <> y) + These a x <> These b y = These (a <> b) (x <> y) + +#if MIN_VERSION_base(4,8,0) +instance Bifunctor These where + bimap :: (a -> c) -> (b -> d) -> These a b -> These c d + bimap f _ (This a ) = This (f a) + bimap _ g (That b) = That (g b) + bimap f g (These a b) = These (f a) (g b) + first :: (a -> c) -> These a b -> These c b + first f = bimap f id + second :: (b -> d) -> These a b -> These a d + second f = bimap id f +#endif + +instance Functor (These a) where + fmap _ (This x) = This x + fmap f (That y) = That (f y) + fmap f (These x y) = These x (f y) + +instance Semigroup a => Applicative (These a) where + pure = That + This a <*> _ = This a + That _ <*> This b = This b + That f <*> That x = That (f x) + That f <*> These b x = These b (f x) + These a _ <*> This b = This (a <> b) + These a f <*> That x = These a (f x) + These a f <*> These b x = These (a <> b) (f x) + +instance Semigroup a => Monad (These a) where + return = pure + This a >>= _ = This a + That x >>= k = k x + These a x >>= k = case k x of + This b -> This (a <> b) + That y -> These a y + These b y -> These (a <> b) y + +instance (NFData a, NFData b) => NFData (These a b) where + rnf (This a) = rnf a + rnf (That b) = rnf b + rnf (These a b) = rnf a `seq` rnf b + +instance Foldable (These a) where + foldr _ z (This _) = z + foldr f z (That x) = f x z + foldr f z (These _ x) = f x z + +instance Traversable (These a) where + traverse _ (This a ) = pure $ This a + traverse f (That x) = That <$> f x + traverse f (These a x) = These a <$> f x + sequenceA (This a ) = pure $ This a + sequenceA (That x) = That <$> x + sequenceA (These a x) = These a <$> x + +#if MIN_VERSION_base(4,10,0) +instance Bifoldable These where + bifold = these id id mappend + bifoldr f g z = these (`f` z) (`g` z) (\x y -> x `f` (y `g` z)) + bifoldl f g z = these (z `f`) (z `g`) (\x y -> (z `f` x) `g` y) +#endif diff --git a/library/Refined/Unsafe.hs b/library/Refined/Unsafe.hs new file mode 100644 --- /dev/null +++ b/library/Refined/Unsafe.hs @@ -0,0 +1,122 @@ +-------------------------------------------------------------------------------- + +-- Copyright © 2015 Nikita Volkov +-- Copyright © 2018 Remy Goldschmidt +-- Copyright © 2018 Daniel Cartwright +-- +-- Permission is hereby granted, free of charge, to any person +-- obtaining a copy of this software and associated documentation +-- files (the "Software"), to deal in the Software without +-- restriction, including without limitation the rights to use, +-- copy, modify, merge, publish, distribute, sublicense, and/or sell +-- copies of the Software, and to permit persons to whom the +-- Software is furnished to do so, subject to the following +-- conditions: +-- +-- The above copyright notice and this permission notice shall be +-- included in all copies or substantial portions of the Software. +-- +-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES +-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT +-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, +-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR +-- OTHER DEALINGS IN THE SOFTWARE. + +-------------------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} +#if __GLASGOW_HASKELL__ >= 805 +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +#endif +{-# OPTIONS_GHC -Wall #-} + +-------------------------------------------------------------------------------- + +-- | This module exposes /unsafe/ refinements. An /unsafe/ refinement +-- is one which either does not make the guarantee of totality in construction +-- of the 'Refined' value or does not perform a check of the refinement +-- predicate. It is recommended only to use this when you can manually prove +-- that the refinement predicate holds. +module Refined.Unsafe + ( -- * 'Refined' + Refined + + -- ** Creation + , reallyUnsafeRefine + , unsafeRefine + + -- ** Coercion + , reallyUnsafeUnderlyingRefined +#if __GLASGOW_HASKELL__ >= 805 + , reallyUnsafeAllUnderlyingRefined +#endif + , reallyUnsafePredEquiv + ) where + +-------------------------------------------------------------------------------- + +import Control.Exception (Exception(displayException)) +import Data.Coerce (coerce) +import Data.Either (either) +import Data.Function (id) + +import GHC.Err (error) + +import Refined.Internal (Refined(Refined), Predicate, refine, (.>)) +import Data.Type.Coercion (Coercion (..)) +#if __GLASGOW_HASKELL__ >= 805 +import Data.Coerce (Coercible) +#endif + +-------------------------------------------------------------------------------- + +-- | Constructs a 'Refined' value at run-time, +-- calling 'Prelude.error' if the value +-- does not satisfy the predicate. +-- +-- WARNING: this function is not total! +unsafeRefine :: (Predicate p x) => x -> Refined p x +unsafeRefine = refine .> either (displayException .> error) id +{-# INLINABLE unsafeRefine #-} + +-- | Constructs a 'Refined' value, completely +-- ignoring any refinements! Use this only +-- when you can manually prove that the refinement +-- holds. +reallyUnsafeRefine :: x -> Refined p x +reallyUnsafeRefine = coerce +{-# INLINE reallyUnsafeRefine #-} + +-- | A coercion between a type and any refinement of that type. +-- See "Data.Type.Coercion" for functions manipulating coercions. +reallyUnsafeUnderlyingRefined :: Coercion x (Refined p x) +reallyUnsafeUnderlyingRefined = Coercion + +-- | A coercion between two 'Refined' types, magicking up the claim +-- that one predicate is entirely equivalent to another. +reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x) +reallyUnsafePredEquiv = Coercion +-- Note: reallyUnsafePredEquiv = +-- sym 'reallyUnsafeUnderlyingRefined' `trans` 'reallyUnsafeUnderlyingRefined' + +#if __GLASGOW_HASKELL__ >= 805 +-- | Reveal that @x@ and @'Refined' p x@ are 'Coercible' for +-- /all/ @x@ and @p@ simultaneously. +-- +-- === Example +-- +-- @ +-- reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x) +-- reallyUnsafePredEquiv = reallyUnsafeAllUnderlyingRefined Coercion +-- @ +reallyUnsafeAllUnderlyingRefined + :: ((forall x y p. (Coercible x y => Coercible y (Refined p x))) => r) -> r +-- Why is this constraint so convoluted? Because otherwise the constraint +-- solver doesn't handle transitivity properly. See "Safe Zero-cost Coercions +-- for Haskell" by Breitner et al. +reallyUnsafeAllUnderlyingRefined r = r +#endif diff --git a/library/Refined/Unsafe/Type.hs b/library/Refined/Unsafe/Type.hs new file mode 100644 --- /dev/null +++ b/library/Refined/Unsafe/Type.hs @@ -0,0 +1,45 @@ +-------------------------------------------------------------------------------- + +-- Copyright © 2015 Nikita Volkov +-- Copyright © 2018 Remy Goldschmidt +-- Copyright © 2018 Daniel Cartwright +-- +-- Permission is hereby granted, free of charge, to any person +-- obtaining a copy of this software and associated documentation +-- files (the "Software"), to deal in the Software without +-- restriction, including without limitation the rights to use, +-- copy, modify, merge, publish, distribute, sublicense, and/or sell +-- copies of the Software, and to permit persons to whom the +-- Software is furnished to do so, subject to the following +-- conditions: +-- +-- The above copyright notice and this permission notice shall be +-- included in all copies or substantial portions of the Software. +-- +-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES +-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT +-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, +-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR +-- OTHER DEALINGS IN THE SOFTWARE. + +-------------------------------------------------------------------------------- + +{-# OPTIONS_GHC -Wall #-} + +-------------------------------------------------------------------------------- + +-- | This module exports the 'Refined' type with its +-- constructor. This is very risky! In particular, the 'Coercible' +-- instances will be visible throughout the importing module. +-- It is usually better to build the necessary coercions locally +-- using the utilities in "Refined.Unsafe", but in some cases +-- it may be more convenient to write a separate module that +-- imports this one and exports some large coercion. +module Refined.Unsafe.Type + ( Refined(Refined) + ) where + +import Refined.Internal (Refined(Refined)) diff --git a/refined.cabal b/refined.cabal --- a/refined.cabal +++ b/refined.cabal @@ -1,7 +1,7 @@ name: refined version: - 0.2.3.0 + 0.3.0.0 synopsis: Refinement types with static and runtime checking description: @@ -16,7 +16,7 @@ author: Nikita Volkov maintainer: - Nikita Volkov + chessai copyright: Copyright © 2015, Nikita Volkov Copyright © 2018, Remy Goldschmidt @@ -46,15 +46,17 @@ library exposed-modules: Refined - Refined.TH + Refined.Internal + Refined.These + Refined.Unsafe + Refined.Unsafe.Type default-language: Haskell2010 build-depends: base >= 4.9 && < 5 - , containers >= 0.5.9.1 - , exceptions >= 0.10.0 + , deepseq >= 1.4.0.0 + , exceptions >= 0.8.0 , mtl >= 2.2.1 , prettyprinter >= 1.1.0.1 , template-haskell >= 2.9 && < 3.0 - , these >= 0.7.4 , transformers >= 0.5.0.0