rerefined 0.3.0 → 0.4.0

raw patch · 17 files changed

+128/−133 lines, 17 filesdep +QuickCheck

Dependencies added: QuickCheck

Files

• CHANGELOG.md +5/−0
• rerefined.cabal +3/−4
• src/Rerefined.hs +2/−0
• src/Rerefined/Predicate.hs +9/−11
• src/Rerefined/Predicate/Common.hs +0/−6
• src/Rerefined/Predicate/Logical/And.hs +2/−3
• src/Rerefined/Predicate/Logical/If.hs +1/−1
• src/Rerefined/Predicate/Logical/Iff.hs +1/−1
• src/Rerefined/Predicate/Logical/Nand.hs +1/−1
• src/Rerefined/Predicate/Logical/Nor.hs +1/−1
• src/Rerefined/Predicate/Logical/Not.hs +1/−1
• src/Rerefined/Predicate/Logical/Or.hs +1/−1
• src/Rerefined/Predicate/Logical/Xor.hs +1/−1
• src/Rerefined/Predicate/Relational/Length.hs +1/−1
• src/Rerefined/Refine.hs +99/−3
• src/Rerefined/Refine/Unsafe.hs +0/−50
• src/Rerefined/Refined.hs +0/−48

@@ -1,3 +1,8 @@+## 0.4.0 (2024-05-11)+* add `Eq`, `Ord`, `Arbitrary` instances+* simplify modules (fewer)+* add `reifyPredicate`, `reifyPredicate1` for reifying predicates to `a -> Bool`+ ## 0.3.0 (2024-05-07) * refactor predicate names: now handled with a sort of type-level `Show`. no   `Typeable`, lots of custom prettiness (infix operators!)

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           rerefined-version:        0.3.0+version:        0.4.0 synopsis:       Refinement types, again description:    Please see README.md. category:       Types, Data@@ -53,8 +53,6 @@       Rerefined.Predicates       Rerefined.Refine       Rerefined.Refine.TH-      Rerefined.Refine.Unsafe-      Rerefined.Refined   other-modules:       Paths_rerefined   hs-source-dirs:@@ -72,7 +70,8 @@       MagicHash   ghc-options: -Wall -Wno-unticked-promoted-constructors   build-depends:-      base >=4.17 && <5+      QuickCheck >=2.14 && <2.16+    , base >=4.17 && <5     , mono-traversable >=1.0.17.0 && <1.1     , template-haskell >=2.19.0.0 && <2.22     , text >=2.0 && <2.2

@@ -1,7 +1,9 @@ module Rerefined   ( module Rerefined.Refine+  , module Rerefined.Refine.TH   , Predicate, Refine, Refine1   ) where  import Rerefined.Refine+import Rerefined.Refine.TH import Rerefined.Predicate

@@ -7,6 +7,7 @@   , Refine1(validate1)   , RefineFailure(..)   , Predicate(..)+  , KnownPredicateName   , predicateName   ) where @@ -21,22 +22,19 @@     -- Predicate names should aim to communicate the meaning of the predicate as     -- clearly and concisely as possible.     ---    -- Consider using @type-level-show@ to build this. However, note that GHC-    -- cannot figure out 'KnownSymbol' when there are type families in play, so-    -- you may need to put 'KnownSymbol' constraints in instance contexts.+    -- Consider using the package @type-level-show@ to build this.     type PredicateName (d :: Natural) p :: Symbol         -- ^ TODO d: the operator precedence of the enclosing context (a number         --   from 0 to 11). Function application has precedence 10. -{- TODO-stuffing the KnownSymbol constraint into a Predicate superclass is handy, but-then we have to handle it in combinator predicates. probably _not_ doing so is-better, so I'm trying that first.--}+-- | Constraint for reifying a predicate name.+type KnownPredicateName p = KnownSymbol (PredicateName 0 p) --- | Reify predicate name.-predicateName-    :: forall p. (Predicate p, KnownSymbol (PredicateName 0 p)) => String+-- | Reify predicate name to a 'String'.+--+-- Using this regrettably necessitates @UndecidableInstances@, due to the type+-- family in the constraint. It sucks, but that's life.+predicateName :: forall p. KnownPredicateName p => String predicateName = symbolVal' (proxy# @(PredicateName 0 p))  -- | Refine @a@ with predicate @p@.

@@ -8,20 +8,14 @@     module Rerefined.Predicate   , proxy#   , TBL.Builder-  , IsString -- TODO remove    -- * Predicate validation   , validateFail, validateBool-  , KnownPredicateName   ) where  import Rerefined.Predicate import GHC.Exts ( Proxy#, proxy#, IsString(fromString) )-import GHC.TypeLits ( KnownSymbol ) import Data.Text.Builder.Linear qualified as TBL---- TODO maybe move to main 'Rerefined.Predicate' module-type KnownPredicateName p = KnownSymbol (PredicateName 0 p)  -- | Shortcut for returning a predicate validation failure. validateFail

@@ -5,13 +5,12 @@  import Rerefined.Predicate.Common.Binary import Rerefined.Predicate.Common-import Rerefined.Refine.Unsafe-import Rerefined.Refined+import Rerefined.Refine  -- | Logical conjunction. Also AND logic gate. data And l r --- | Precendence of 3 (matching 'Data.Bool.&&').+-- | Precedence of 3 (matching 'Data.Bool.&&'). instance (Predicate l, Predicate r) => Predicate (And l r) where     type PredicateName d (And l r) = PredicateNameBOp " ∧ " 3 d l r 

@@ -9,7 +9,7 @@ -- | Logical implication. "If l then r". data If l r --- | Precendence of 4 (matching '==').+-- | Precedence of 4 (matching '=='). instance (Predicate l, Predicate r) => Predicate (If l r) where     -- TODO double arrow? idk     type PredicateName d (If l r) = PredicateNameBOp " → " 4 d l r

@@ -10,7 +10,7 @@ --   equivalence (loosely). data Iff l r --- | Precendence of 4 (matching '==').+-- | Precedence of 4 (matching '=='). instance (Predicate l, Predicate r) => Predicate (Iff l r) where     type PredicateName d (Iff l r) = PredicateNameBOp " ↔ " 4 d l r 

@@ -9,7 +9,7 @@ -- | NAND logic gate. Also called the Sheffer stroke, or non-conjunction. data Nand l r --- | Precendence of 3 (matching 'Data.Bool.&&').+-- | Precedence of 3 (matching 'Data.Bool.&&'). instance (Predicate l, Predicate r) => Predicate (Nand l r) where     type PredicateName d (Nand l r) = PredicateNameBOp " ⊼ " 3 d l r 

@@ -9,7 +9,7 @@ -- | NOR logic gate. Also called non-disjunction, or joint denial. data Nor l r --- | Precendence of 2 (matching 'Data.Bool.||').+-- | Precedence of 2 (matching 'Data.Bool.||'). instance (Predicate l, Predicate r) => Predicate (Nor l r) where     type PredicateName d (Nor l r) = PredicateNameBOp " ⊽ " 2 d l r 

@@ -9,7 +9,7 @@ -- | Logical negation. Also NOT logic gate, or logical complement. data Not p --- | Precendence of 9 (one below function application).+-- | Precedence of 9 (one below function application). instance Predicate p => Predicate (Not p) where     type PredicateName d (Not p) = ShowParen (d > 9)         ("¬ " ++ PredicateName 10 p)

@@ -9,7 +9,7 @@ -- | Logical disjunction. Also OR logic gate. data Or l r --- | Precendence of 2 (matching 'Data.Bool.||').+-- | Precedence of 2 (matching 'Data.Bool.||'). instance (Predicate l, Predicate r) => Predicate (Or l r) where     type PredicateName d (Or l r) = PredicateNameBOp " ∨ " 2 d l r 

@@ -9,7 +9,7 @@ -- | Logical exclusive disjunction. Also XOR logic gate. data Xor l r --- | Precendence of 4 (matching '==').+-- | Precedence of 4 (matching '=='). instance (Predicate l, Predicate r) => Predicate (Xor l r) where     type PredicateName d (Xor l r) = PredicateNameBOp " ⊕ " 4 d l r 

@@ -9,7 +9,7 @@ import Data.MonoTraversable ( MonoFoldable(olength) ) import GHC.Exts ( Proxy# ) -import Rerefined.Refine.Unsafe+import Rerefined.Refine import GHC.TypeError import Data.Kind ( type Constraint ) import TypeLevelShow.Utils

@@ -1,4 +1,6 @@ {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE AllowAmbiguousTypes #-} -- for predicate reification+{-# LANGUAGE UndecidableInstances #-} -- for KnownPredicateName in Arbitrary  module Rerefined.Refine   (@@ -6,11 +8,18 @@     type Refined   , refine   , unrefine+  , reifyPredicate+  , unsafeRefine+  , unsafeRerefine    -- * @Refined1@   , type Refined1   , refine1   , unrefine1+  , reifyPredicate1+  , squashRefined1+  , unsafeRefine1+  , unsafeRerefine1    -- * Errors   , type RefineFailure@@ -18,12 +27,45 @@   , prettyRefineFailure'   ) where -import Rerefined.Refined import Rerefined.Predicate+import Language.Haskell.TH.Syntax ( Lift ) import GHC.Exts ( proxy# ) import Data.Text ( Text ) import Data.Text.Builder.Linear qualified as TBL +import Test.QuickCheck ( Arbitrary(arbitrary) )+import Test.QuickCheck.Gen qualified as QC++-- | @a@ refined with predicate @p@.+newtype Refined p a = Refined a+    deriving stock (Lift, Eq, Ord, Show)++-- | Strip the refinement from a 'Refined'.+--+-- This is kept as a separate function for prettier @'Show' 'Refined'@ output.+unrefine :: Refined p a -> a+unrefine (Refined a) = a++-- | @f a@ refined with predicate @p@.+--+-- We may derive legal 'Functor', 'Traversable' instances for this as+-- 'Rerefined.Predicate.Refine1' guarantees that the predicate only applies to+-- the functor structure. That is, you _may_ alter a 'Refined1' without+-- re-asserting its predicate, provided your changes are made without altering+-- the structure/shape of @f@ (e.g. 'fmap', 'traverse').+newtype Refined1 p f a = Refined1 (f a)+    deriving stock (Functor, Foldable, Traversable, Lift, Eq, Ord, Show)++-- | Strip the refinement from a 'Refined1'.+--+-- This is kept as a separate function for prettier @'Show' 'Refined1'@ output.+unrefine1 :: Refined1 p f a -> f a+unrefine1 (Refined1 fa) = fa++-- | Squash a 'Refined1' into a 'Refined'. Essentially forget the @f@.+squashRefined1 :: Refined1 p f a -> Refined p (f a)+squashRefined1 = Refined . unrefine1+ -- | Refine @a@ with predicate @p@. refine     :: forall p a. Refine p a@@ -33,9 +75,22 @@       Nothing -> Right (Refined a)       Just e  -> Left e --- reifyPredicate is just a weaker version of validate without proxy.--- Maybe the latter is useful, though...?+-- | Construct a 'Refined' without validating the predicate @p@.+--+-- Unsafe. Use only when you can manually prove that the predicate holds.+unsafeRefine :: a -> Refined p a+unsafeRefine = Refined +-- | Replace a 'Refined''s predicate without validating the new prdicate @pNew@.+--+-- Unsafe. Use only when you can manually prove that the new predicate holds.+unsafeRerefine :: forall pNew pOld a. Refined pOld a -> Refined pNew a+unsafeRerefine = Refined . unrefine++-- | Reify a predicate.+reifyPredicate :: forall p a. Refine p a => a -> Bool+reifyPredicate a = case refine @p a of Right{} -> True; Left{} -> False+ -- | Refine @f a@ with functor predicate @p@. refine1     :: forall p f a. Refine1 p f@@ -45,6 +100,23 @@       Nothing -> Right (Refined1 fa)       Just e  -> Left e +-- | Construct a 'Refined1' without validating the predicate @p@.+--+-- Unsafe. Use only when you can manually prove that the predicate holds.+unsafeRefine1 :: f a -> Refined1 p f a+unsafeRefine1 = Refined1++-- | Replace a 'Refined1''s predicate without validating the new prdicate+--   @pNew@.+--+-- Unsafe. Use only when you can manually prove that the new predicate holds.+unsafeRerefine1 :: forall pNew pOld f a. Refined1 pOld f a -> Refined1 pNew f a+unsafeRerefine1 = Refined1 . unrefine1++-- | Reify a functor predicate.+reifyPredicate1 :: forall p f a. Refine1 p f => f a -> Bool+reifyPredicate1 fa = case refine1 @p fa of Right{} -> True; Left{} -> False+ {- TODO * got an extra \n at start oops * make it look better lol@@ -84,3 +156,27 @@     idk n rs = \case       []   -> rs       l:ls -> idk n ((n, l):rs) ls++-- | Generate a refined term by generating an unrefined term and asserting the+--   predicate.+--+-- Will runtime error if it fails to find a satisfying term (based on size).+instance (Arbitrary a, Refine p a, KnownPredicateName p)+  => Arbitrary (Refined p a) where+    arbitrary = QC.suchThatMaybe arbitrary (reifyPredicate @p) >>= \case+      Just a  -> pure $ Refined a+      Nothing -> error $+           "rerefined: couldn't generate a value satisfying predicate: "+        <> predicateName @p++-- | Generate a refined term by generating an unrefined term and asserting the+--   functor predicate.+--+-- Will runtime error if it fails to find a satisfying term (based on size).+instance (Arbitrary (f a), Refine1 p f, KnownPredicateName p)+  => Arbitrary (Refined1 p f a) where+    arbitrary = QC.suchThatMaybe arbitrary (reifyPredicate1 @p) >>= \case+      Just fa -> pure $ Refined1 fa+      Nothing -> error $+           "rerefined: couldn't generate a value satisfying predicate: "+        <> predicateName @p

@@ -1,50 +0,0 @@-{- | Unsafe refining.--Sometimes, you know that your value satisfies some predicate before validating.-For those cases, we permit skipping validation and obtaining a refined value-"for free".--You should be certain that your value cannot possibly fail the predicate you are-skipping. A good practice is to annotate all call sites with an explanation of-why the usage is safe.--}--module Rerefined.Refine.Unsafe-  (-  -- * @Refined@-    type Refined-  , unsafeRefine-  , unsafeRerefine--  -- * @Refined1@-  , type Refined1-  , unsafeRefine1-  , unsafeRerefine1-  ) where--import Rerefined.Refined---- | Construct a 'Refined' without validating the predicate @p@.------ Unsafe. Use only when you can manually prove that the predicate holds.-unsafeRefine :: a -> Refined p a-unsafeRefine = Refined---- | Replace a 'Refined''s predicate without validating the new prdicate @pNew@.------ Unsafe. Use only when you can manually prove that the new predicate holds.-unsafeRerefine :: forall pNew pOld a. Refined pOld a -> Refined pNew a-unsafeRerefine = Refined . unrefine---- | Construct a 'Refined1' without validating the predicate @p@.------ Unsafe. Use only when you can manually prove that the predicate holds.-unsafeRefine1 :: f a -> Refined1 p f a-unsafeRefine1 = Refined1---- | Replace a 'Refined1''s predicate without validating the new prdicate---   @pNew@.------ Unsafe. Use only when you can manually prove that the new predicate holds.-unsafeRerefine1 :: forall pNew pOld f a. Refined1 pOld f a -> Refined1 pNew f a-unsafeRerefine1 = Refined1 . unrefine1

@@ -1,48 +0,0 @@--- | 'Refined' and 'Refined1' definitions for refined values.------ Not intended for external use. For unsafe refining, use--- 'Rerefined.Refine.Unsafe'.--module Rerefined.Refined-  (-  -- * @Refined@-    Refined(..)-  , unrefine--  -- * @Refined1@-  , Refined1(..)-  , unrefine1-  , squashRefined1-  ) where--import Language.Haskell.TH.Syntax ( Lift )---- | @a@ refined with predicate @p@.-newtype Refined p a = Refined a-    deriving stock (Lift, Show)---- | Strip the refinement from a 'Refined'.------ This is kept as a separate function for prettier @'Show' 'Refined'@ output.-unrefine :: Refined p a -> a-unrefine (Refined a) = a---- | @f a@ refined with predicate @p@.------ We may derive legal 'Functor', 'Traversable' instances for this as--- 'Rerefined.Predicate.Refine1' guarantees that the predicate only applies to--- the functor structure. That is, you _may_ alter a 'Refined1' without--- re-asserting its predicate, provided your changes are made without altering--- the structure/shape of @f@ (e.g. 'fmap', 'traverse').-newtype Refined1 p f a = Refined1 (f a)-    deriving stock (Functor, Foldable, Traversable, Lift, Show)---- | Strip the refinement from a 'Refined1'.------ This is kept as a separate function for prettier @'Show' 'Refined1'@ output.-unrefine1 :: Refined1 p f a -> f a-unrefine1 (Refined1 fa) = fa---- | Squash a 'Refined1' into a 'Refined'. Essentially forget the @f@.-squashRefined1 :: Refined1 p f a -> Refined p (f a)-squashRefined1 = Refined . unrefine1