From e20800a93327c3d5877d64ee7ba623526c0b3b14 Mon Sep 17 00:00:00 2001 From: Ben Orchard Date: Thu, 10 Oct 2024 22:13:13 +0100 Subject: [PATCH 1/4] Predicate.Relational: back to RelOp type It has much better type-level ergonomics. --- src/Rerefined/Predicate/Relational.hs | 4 +- .../Predicate/Relational/Internal.hs | 114 ++++++------------ src/Rerefined/Predicate/Relational/Length.hs | 2 +- src/Rerefined/Predicate/Relational/Value.hs | 2 +- src/Rerefined/Predicates.hs | 2 +- src/Rerefined/Predicates/Operators.hs | 12 +- 6 files changed, 51 insertions(+), 85 deletions(-) diff --git a/src/Rerefined/Predicate/Relational.hs b/src/Rerefined/Predicate/Relational.hs index 3b6da39..11802ec 100644 --- a/src/Rerefined/Predicate/Relational.hs +++ b/src/Rerefined/Predicate/Relational.hs @@ -1,8 +1,8 @@ module Rerefined.Predicate.Relational - ( CompareValue + ( RelOp(..) + , CompareValue , Sign(..) , CompareLength - , LTE, GTE ) where import Rerefined.Predicate.Relational.Internal diff --git a/src/Rerefined/Predicate/Relational/Internal.hs b/src/Rerefined/Predicate/Relational/Internal.hs index 45294f5..35bd87f 100644 --- a/src/Rerefined/Predicate/Relational/Internal.hs +++ b/src/Rerefined/Predicate/Relational/Internal.hs @@ -1,111 +1,77 @@ {-# LANGUAGE AllowAmbiguousTypes #-} -- for ReifyRelOp {-# LANGUAGE UndecidableInstances #-} -- for WidenRelOp -{- | Relational operator definitions. - -Haskell base exports the type 'Ordering', which is an enum that states the -result of comparing two 'Ord's. We can utilize this to define /relational -operators/: - -* 'LT', 'EQ' and 'GT' already map to relational operators. -* The others can be defined by combining the above with 'Or'. e.g. @'LT' ``Or`` - 'EQ'@ -> "less than or equal" ('<=') - -What's the point? We save on definitions, and get to reuse well-known data types -which most users will have intuition for. We do have to contest with -commutativity, but this is an extremely minor concern which can only come up if -you don't use the provided type synonyms, or do lots of type-level predicate -manipulation. And we provide those swapped-order instances anyway! --} +-- | Relational operator definitions. module Rerefined.Predicate.Relational.Internal where -import Rerefined.Predicate.Logical.Or import GHC.TypeNats import Data.Type.Ord ( OrdCond ) import GHC.TypeLits ( Symbol ) -import Data.Kind ( Type ) - -type LTE = LT `Or` EQ - --- | "not equal to" is equivalent to "strictly less than or greater than". We --- could use 'Rerefined.Predicate.Logical.Not.Not', but sticking with just --- 'Or' keeps the internals simple. -type NEQ = LT `Or` GT +{- | Relational operator. -type GTE = GT `Or` EQ +Constructor order is arbitrary due to @NEQ@, which obstructs ordering in a +meaningful way. --- | Reify a relational operator type tag. --- --- Permitted operators are @Ordering@ constructors 'LT', 'EQ' and 'GT'; and --- combinations of these using 'Or'. -class ReifyRelOp op where +Note that these operators may be defined by combining 'Ordering's in certain +ways: for example @'LT' OR 'EQ'@ could be @LTE@, @'LT' OR 'GT'@ could be @NEQ@. +This is convenient for user intuition, permitting the use of e.g. 'LT' as a +relational operator directly. However, it complicates type-level work, as now we +can't restrict relational operators to a given kind, and we have to handle +non-standard orderings like @'GT' OR 'LT'@. +-} +data RelOp + = RelOpLT -- ^ @<@ less than + | RelOpLTE -- ^ @<=@ less than or equal to + | RelOpEQ -- ^ @==@ equal to + | RelOpNEQ -- ^ @/=@ less than or greater than (also not equal to) + | RelOpGTE -- ^ @>=@ equal to or greater than + | RelOpGT -- ^ @>@ greater than + +-- | Reify a 'RelOp'. +class ReifyRelOp (op :: RelOp) where -- | Pretty @op@. type ShowRelOp op :: Symbol - -- | The term-level relational operator that @op@ describes. + -- | The term-level relational operator that @op :: 'RelOp'@ describes. reifyRelOp :: forall a. Ord a => a -> a -> Bool -instance ReifyRelOp LT where - type ShowRelOp LT = "<" +instance ReifyRelOp RelOpLT where + type ShowRelOp RelOpLT = "<" reifyRelOp = (<) -instance ReifyRelOp LTE where - type ShowRelOp LTE = "<=" +instance ReifyRelOp RelOpLTE where + type ShowRelOp RelOpLTE = "<=" reifyRelOp = (<=) --- | Hidden instance. You won't see this if you use the type synonyms. -deriving via LTE instance ReifyRelOp (EQ `Or` LT) - -instance ReifyRelOp EQ where - type ShowRelOp EQ = "==" +instance ReifyRelOp RelOpEQ where + type ShowRelOp RelOpEQ = "==" reifyRelOp = (==) -instance ReifyRelOp NEQ where - type ShowRelOp NEQ = "/=" +instance ReifyRelOp RelOpNEQ where + type ShowRelOp RelOpNEQ = "/=" reifyRelOp = (/=) --- | Hidden instance. You won't see this if you use the type synonyms. -deriving via NEQ instance ReifyRelOp (GT `Or` LT) - -instance ReifyRelOp GTE where - type ShowRelOp GTE = ">=" +instance ReifyRelOp RelOpGTE where + type ShowRelOp RelOpGTE = ">=" reifyRelOp = (>=) --- | Hidden instance. You won't see this if you use the type synonyms. -deriving via GTE instance ReifyRelOp (EQ `Or` GT) - -instance ReifyRelOp GT where - type ShowRelOp GT = ">" +instance ReifyRelOp RelOpGT where + type ShowRelOp RelOpGT = ">" reifyRelOp = (>) -- | Can we widen the given 'RelOp' on the given 'Natural' from @n@ to @m@? -type WidenRelOp :: k -> Natural -> Natural -> Bool +type WidenRelOp :: RelOp -> Natural -> Natural -> Bool type family WidenRelOp op n m where -- @n == m@? no problem WidenRelOp op n n = True -- I'd love to simplify this, but 'CmpNat' is opaque. - WidenRelOp LT n m = OrdCond (CmpNat n m) True True False - WidenRelOp LTE n m = OrdCond (CmpNat n m) True True False - WidenRelOp GTE n m = OrdCond (CmpNat n m) False True True - WidenRelOp GT n m = OrdCond (CmpNat n m) False True True - - -- | swapped LTE, lower down in equation list because less common - WidenRelOp (EQ `Or` LT) n m = - OrdCond (CmpNat n m) True True False - - -- | swapped GTE, lower down in equation list because less common - WidenRelOp (EQ `Or` GT) n m = - OrdCond (CmpNat n m) False True True + WidenRelOp RelOpLT n m = OrdCond (CmpNat n m) True True False + WidenRelOp RelOpLTE n m = OrdCond (CmpNat n m) True True False + WidenRelOp RelOpGTE n m = OrdCond (CmpNat n m) False True True + WidenRelOp RelOpGT n m = OrdCond (CmpNat n m) False True True -- can't widen (==) or (/=) - WidenRelOp _ _ _ = False - --- this gets clumsier due to kinding clashes (k vs. Ordering) -type NormalizeOrRelOp :: Type -> Type -type family NormalizeOrRelOp op where - NormalizeOrRelOp (EQ `Or` LT) = LTE - NormalizeOrRelOp (GT `Or` LT) = NEQ - NormalizeOrRelOp (EQ `Or` GT) = GTE + WidenRelOp op n m = False diff --git a/src/Rerefined/Predicate/Relational/Length.hs b/src/Rerefined/Predicate/Relational/Length.hs index 3a716b8..b0a16a2 100644 --- a/src/Rerefined/Predicate/Relational/Length.hs +++ b/src/Rerefined/Predicate/Relational/Length.hs @@ -17,7 +17,7 @@ import TypeLevelShow.Natural import Data.Text.Builder.Linear qualified as TBL -- | Compare length to a type-level 'Natural' using the given 'RelOp'. -data CompareLength op (n :: Natural) +data CompareLength (op :: RelOp) (n :: Natural) -- | Precedence of 4 (matching base relational operators e.g. '>='). instance Predicate (CompareLength op n) where diff --git a/src/Rerefined/Predicate/Relational/Value.hs b/src/Rerefined/Predicate/Relational/Value.hs index 4cd893f..abbcc54 100644 --- a/src/Rerefined/Predicate/Relational/Value.hs +++ b/src/Rerefined/Predicate/Relational/Value.hs @@ -12,7 +12,7 @@ import TypeLevelShow.Natural import GHC.TypeLits ( Symbol ) -- | Compare value to a type-level 'Natural' using the given 'RelOp'. -data CompareValue op (sign :: Sign) (n :: Natural) +data CompareValue (op :: RelOp) (sign :: Sign) (n :: Natural) -- | Precedence of 4 (matching base relational operators e.g. '>='). instance Predicate (CompareValue op sign n) where diff --git a/src/Rerefined/Predicates.hs b/src/Rerefined/Predicates.hs index 20d250b..bcd7179 100644 --- a/src/Rerefined/Predicates.hs +++ b/src/Rerefined/Predicates.hs @@ -11,10 +11,10 @@ module Rerefined.Predicates , And, Iff, If, Nand, Nor, Not, Or, Xor -- * Relational + , RelOp(..) , CompareValue , Sign(..) , CompareLength - , LTE, GTE ) where import Rerefined.Predicate.Succeed diff --git a/src/Rerefined/Predicates/Operators.hs b/src/Rerefined/Predicates/Operators.hs index 5b557e0..5e0ea31 100644 --- a/src/Rerefined/Predicates/Operators.hs +++ b/src/Rerefined/Predicates/Operators.hs @@ -59,9 +59,9 @@ infixr 4 .-> type (.->) = If infix 4 .<, .<=, .==, ./=, .>=, .> -type (.<) = LT -type (.<=) = LTE -type (.==) = EQ -type (./=) = NEQ -type (.>=) = GTE -type (.>) = GT +type (.<) = RelOpLT +type (.<=) = RelOpLTE +type (.==) = RelOpEQ +type (./=) = RelOpNEQ +type (.>=) = RelOpGTE +type (.>) = RelOpGT From 6f6248bf7a3dc96dac6184f8f85a92852b611b13 Mon Sep 17 00:00:00 2001 From: Ben Orchard Date: Thu, 10 Oct 2024 22:14:40 +0100 Subject: [PATCH 2/4] CI: tweak syntax --- .github/workflows/nix.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/nix.yaml b/.github/workflows/nix.yaml index a10edd2..d7dd46e 100644 --- a/.github/workflows/nix.yaml +++ b/.github/workflows/nix.yaml @@ -12,8 +12,8 @@ jobs: ghc: [ghc98, ghc910] runs-on: ubuntu-latest permissions: - id-token: "write" - contents: "read" + id-token: write # ? requested by magic-nix-cache + contents: read # ? requested by magic-nix-cache steps: - uses: actions/checkout@v4 - uses: DeterminateSystems/nix-installer-action@main From 3af36ac32d4c5d4f9c20033658923ba6369e7dac Mon Sep 17 00:00:00 2001 From: Ben Orchard Date: Thu, 10 Oct 2024 22:15:00 +0100 Subject: [PATCH 3/4] add predicate simplifier --- TODO.md | 7 - rerefined.cabal | 3 +- src/Rerefined/Predicate/Logical/Normalize.hs | 10 - src/Rerefined/Predicate/Normalize.hs | 12 -- src/Rerefined/Simplify.hs | 190 +++++++++++++++++++ 5 files changed, 191 insertions(+), 31 deletions(-) delete mode 100644 src/Rerefined/Predicate/Logical/Normalize.hs delete mode 100644 src/Rerefined/Predicate/Normalize.hs create mode 100644 src/Rerefined/Simplify.hs diff --git a/TODO.md b/TODO.md index 258f2aa..a4a1715 100644 --- a/TODO.md +++ b/TODO.md @@ -15,13 +15,6 @@ ## Predicates * `All ps`, `And` a list of predicates? My errors work for it. Seems fun. -## Predicate normalization -I've got basic logical predicate normalization. It seems adding further -normalization will be more complicated. Relational normalization seems to -rely on inspecting logical predicates as well e.g. `(< n) && (> m) where n > m = -_|_`. I'm fairly certain we have to take a heuristic approach, and I'm fairly -happy with leaving this for a while. - ## Predicate names: fixity I do precedence, but not associativity. Not sure how to. `Show` doesn't help. See: http://intrologic.stanford.edu/dictionary/operator_precedence.html diff --git a/rerefined.cabal b/rerefined.cabal index efeb7d6..c4620f1 100644 --- a/rerefined.cabal +++ b/rerefined.cabal @@ -40,11 +40,9 @@ library Rerefined.Predicate.Logical.Iff Rerefined.Predicate.Logical.Nand Rerefined.Predicate.Logical.Nor - Rerefined.Predicate.Logical.Normalize Rerefined.Predicate.Logical.Not Rerefined.Predicate.Logical.Or Rerefined.Predicate.Logical.Xor - Rerefined.Predicate.Normalize Rerefined.Predicate.Relational Rerefined.Predicate.Relational.Internal Rerefined.Predicate.Relational.Length @@ -55,6 +53,7 @@ library Rerefined.Predicates.Operators Rerefined.Refine Rerefined.Refine.TH + Rerefined.Simplify other-modules: Paths_rerefined hs-source-dirs: diff --git a/src/Rerefined/Predicate/Logical/Normalize.hs b/src/Rerefined/Predicate/Logical/Normalize.hs deleted file mode 100644 index 445969b..0000000 --- a/src/Rerefined/Predicate/Logical/Normalize.hs +++ /dev/null @@ -1,10 +0,0 @@ -module Rerefined.Predicate.Logical.Normalize where - -import Rerefined.Predicate.Logical - -type family NormLogi p where - NormLogi (Not (Not p)) = Just p - NormLogi (Or l l) = Just l - NormLogi (And l l) = Just l - NormLogi (Nand l l) = Just (Not l) - NormLogi p = Nothing diff --git a/src/Rerefined/Predicate/Normalize.hs b/src/Rerefined/Predicate/Normalize.hs deleted file mode 100644 index d346d75..0000000 --- a/src/Rerefined/Predicate/Normalize.hs +++ /dev/null @@ -1,12 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - -module Rerefined.Predicate.Normalize where - -import Rerefined.Predicate.Logical.Normalize - -type family Norm p where - Norm p = Norm' p (NormLogi p) - -type family Norm' p mp where - Norm' p Nothing = p - Norm' p (Just p') = Norm p' diff --git a/src/Rerefined/Simplify.hs b/src/Rerefined/Simplify.hs new file mode 100644 index 0000000..587528e --- /dev/null +++ b/src/Rerefined/Simplify.hs @@ -0,0 +1,190 @@ +{-# LANGUAGE UndecidableInstances #-} + +{- | Primitive predicate simplifier. + +This is related to an NP-complete problem (see Boolean satisfiability problem). +We focus on /immediate, operation-reducing simplifications/, and hope that the +input is formed in such a way that our rules match. + +The simplifier may not be expectected to consistently implement any +transformations whatsoever. The only guarantees are + +* the output has the same or fewer operations +* the output meaning is identical to the input + +Implementation pitfalls: + +* not extensible: only works for built-in logical & relational predicates +* no protection against non-termination e.g. if a pair of transformations loop +* very tedious to write. that's life +-} + +module Rerefined.Simplify + ( Simplify + , Simplify' + ) where + +import Rerefined.Predicate.Succeed +import Rerefined.Predicate.Fail + +import Rerefined.Predicate.Logical + +import Rerefined.Predicate.Relational +import GHC.TypeNats ( Natural, CmpNat ) +import Data.Type.Ord ( OrdCond ) + +-- | Simplify the given predicate. +-- +-- Returns the input predicate if we were unable to simplify. +type Simplify p = FromMaybe p (Simplify' p) + +-- | Promoted 'Data.Maybe.fromMaybe'. +type family FromMaybe a ma where + FromMaybe a Nothing = a + FromMaybe a (Just a') = a' + +-- | Try to simplify the given predicate. +-- +-- Returns 'Nothing' if we were unable to simplify. +type family Simplify' p where + Simplify' (And l r) = SimplifyAnd l r + Simplify' (Or l r) = SimplifyOr l r + Simplify' (Nand l r) = SimplifyNand l r + Simplify' (Not p) = SimplifyNot p + + Simplify' (CompareLength op n) = SimplifyCompareLength op n + + Simplify' p = Nothing + +type family SimplifyAnd l r where + -- identity laws + SimplifyAnd p Fail = Just Fail + SimplifyAnd Fail p = Just Fail + SimplifyAnd p Succeed = Just p + SimplifyAnd Succeed p = Just p + + SimplifyAnd p p = Just p + + -- distributivity + SimplifyAnd (Or x y) (Or x z) = Just (Or x (And y z)) + + -- special + SimplifyAnd (CompareLength lop ln) (CompareLength rop rn) = + SimplifyCompareLengthAnd lop ln rop rn + + -- recurse + SimplifyAnd l r = + (OrElseAndL r (Simplify' l) + (OrElseAndR l (Simplify' r) + Nothing)) + +type family OrElseAndL r mp cont where + OrElseAndL r Nothing cont = cont + OrElseAndL r (Just l') cont = Just (And l' r) + +type family OrElseAndR l mp cont where + OrElseAndR l Nothing cont = cont + OrElseAndR l (Just r') cont = Just (And l r') + +type family SimplifyOr l r where + -- identity laws + SimplifyOr Succeed p = Just Succeed + SimplifyOr p Succeed = Just Succeed + SimplifyOr Fail p = Just p + SimplifyOr p Fail = Just p + + SimplifyOr p p = Just p + + -- distributivity + SimplifyOr (And x y) (And x z) = Just (And x (Or y z)) + + -- special + SimplifyOr (CompareLength lop ln) (CompareLength rop rn) = + SimplifyCompareLengthOr lop ln rop rn + + -- recurse + SimplifyOr l r = + (OrElseOrL r (Simplify' l) + (OrElseOrR l (Simplify' r) + Nothing)) + +type family OrElseOrL r mp cont where + OrElseOrL r Nothing cont = cont + OrElseOrL r (Just l') cont = Just (Or l' r) + +type family OrElseOrR l mp cont where + OrElseOrR l Nothing cont = cont + OrElseOrR l (Just r') cont = Just (Or l r') + +type family SimplifyCompareLength (op :: RelOp) (n :: Natural) where + SimplifyCompareLength RelOpLT 0 = Just Fail + SimplifyCompareLength RelOpLTE 0 = Just (CompareLength RelOpEQ 0) + + -- TODO I think that's it for single relational predicates. + SimplifyCompareLength op n = Nothing + +type family SimplifyCompareLengthAnd + (lop :: RelOp) (ln :: Natural) (rop :: RelOp) (rn :: Natural) where + -- @m@: @n<=m@ -> False + SimplifyCompareLengthAnd RelOpLT n RelOpGT m = + OrdCond (CmpNat n m) + (Just Fail) + (Just Fail) + Nothing + SimplifyCompareLengthAnd RelOpGT m RelOpLT n = + OrdCond (CmpNat n m) + (Just Fail) + (Just Fail) + Nothing + + SimplifyCompareLengthAnd lop ln rop rn = Nothing + +type family SimplifyCompareLengthOr + (lop :: RelOp) (ln :: Natural) (rop :: RelOp) (rn :: Natural) where + -- @m@: @n==m@ -> NEQ; @n>m@ -> True (?) + SimplifyCompareLengthOr RelOpLT n RelOpGT m = + OrdCond (CmpNat n m) + Nothing + (Just (CompareLength RelOpNEQ n)) + (Just Succeed) + SimplifyCompareLengthOr RelOpGT m RelOpLT n = + OrdCond (CmpNat n m) + Nothing + (Just (CompareLength RelOpNEQ n)) + (Just Succeed) + + SimplifyCompareLengthOr lop ln rop rn = Nothing + +type family SimplifyNand l r where + -- TODO fill in rest + SimplifyNand p p = Just (Not p) + + -- recurse + SimplifyNand l r = + (OrElseNandL r (Simplify' l) + (OrElseNandR l (Simplify' r) + Nothing)) + +type family OrElseNandL r mp cont where + OrElseNandL r Nothing cont = cont + OrElseNandL r (Just l') cont = Just (Nand l' r) + +type family OrElseNandR l mp cont where + OrElseNandR l Nothing cont = cont + OrElseNandR l (Just r') cont = Just (Nand l r') + +type family SimplifyNot p where + -- double negation + SimplifyNot (Not p) = Just p + + SimplifyNot Succeed = Just Fail + SimplifyNot Fail = Just Succeed + + -- TODO handle relational predicates! + + -- recurse + SimplifyNot p = OrElseNot (Simplify' p) Nothing + +type family OrElseNot mp cont where + OrElseNot Nothing cont = cont + OrElseNot (Just p') cont = Just (Not p') From 0c3da551699154054b8b1e57da391758427f958a Mon Sep 17 00:00:00 2001 From: Ben Orchard Date: Thu, 10 Oct 2024 22:20:35 +0100 Subject: [PATCH 4/4] update changelog --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3e01bfd..0f1bbe5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,7 @@ +## 0.7.0 (unreleased) +* add predicate simplifier at `Rerefined.Simplify` + * old "normalizer" stuff removed + ## 0.6.0 (2024-10-01) * remove `Via` predicate, only need `validateVia` * swap `validateBool` args