back to RelOp type; add simplifier >:)

.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

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

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

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:

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

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

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

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

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

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