Use QuantifiedConstraints instead of Eq1,Ord1,Show1

Author: alt-romes

README.md

@@ -47,20 +47,22 @@ Our second step is to instance `Language` for our `SymExpr`
 represented in e-graph and on which equality saturation can be run:
 
 ```hs
-class (Analysis l, Traversable l, Ord1 l) => Language l
+type Language l = (Traversable l, ∀ a. Ord a => Ord (l a))
 ```
 
-To declare a `Language` we must write the "base functor" of `SymExpr` 
-(i.e. use a type parameter where the recursion points used to be in the original `SymExpr`),
-then instance `Traversable`, `Ord1`, and write an `Analysis` instance for it (see next section).
+To declare a `Language` we must write the "base functor" of `SymExpr` (i.e. use
+a type parameter where the recursion points used to be in the original
+`SymExpr`), then instance `Traversable l`, `∀ a. Ord a => Ord (l a)` (we can do
+it automatically through deriving), and write an `Analysis` instance for it (see
+next section).
 
 ```hs
 data SymExpr a = Const Double
                | Symbol String
                | a :+: a
                | a :*: a
                | a :/: a
-               deriving (Functor, Foldable, Traversable)
+               deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
 infix 6 :+:
 infix 7 :*:, :/:
 ```
@@ -76,14 +78,6 @@ fixed-point form
 e1 :: Fix SymExpr
 e1 = Fix (Fix (Fix (Symbol "x") :*: Fix (Const 2)) :/: (Fix (Const 2))) -- (x*2)/2
 ```
-
-We've already automagically derived `Functor`, `Foldable` and `Traversable`
-instances, and can use the following template haskell functions from `derive-compat` to derive `Ord1`.
-```hs
-deriveEq1   ''SymExpr
-deriveOrd1  ''SymExpr
-```
-
 Then, we define an `Analysis` for our `SymExpr`.
 
 ### Analysis

hegg.cabal

@@ -114,7 +114,6 @@ test-suite hegg-test
     build-depends:    base,
                       hegg,
                       containers,
-                      deriving-compat  >= 0.6 && < 0.7,
                       tasty            >= 1.4 && < 1.5,
                       tasty-hunit      >= 0.10 && < 0.11,
                       tasty-quickcheck >= 0.10 && < 0.11
@@ -127,7 +126,6 @@ benchmark hegg-bench
   type:           exitcode-stdio-1.0
   build-depends:  base, hegg,
                   containers,
-                  deriving-compat,
                   tasty,
                   tasty-hunit,
                   tasty-quickcheck,

src/Data/Equality/Analysis.hs

@@ -6,6 +6,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ImpredicativeTypes #-}
 {-|
 
 E-class analysis, which allows the concise expression of a program analysis over

src/Data/Equality/Extraction.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE MonoLocalBinds #-}
 {-|
    Given an e-graph representing expressions of our language, we might want to
    extract, out of all expressions represented by some equivalence class, /the best/

src/Data/Equality/Graph/Classes.hs

@@ -10,8 +10,6 @@ module Data.Equality.Graph.Classes
 
 import qualified Data.Set as S
 
-import Data.Functor.Classes
-
 import Data.Equality.Graph.Classes.Id
 import Data.Equality.Graph.Nodes
 
@@ -30,6 +28,6 @@ data EClass analysis_domain language = EClass
     , eClassParents :: !(SList (ClassId, ENode language)) -- ^ E-nodes which are parents of this e-class and their corresponding e-class ids.
     }
 
-instance (Show a, Show1 l) => Show (EClass a l) where
+instance (Show a, Show (l ClassId)) => Show (EClass a l) where
     show (EClass a b d (SList c _)) = "Id: " <> show a <> "\nNodes: " <> show b <> "\nParents: " <> show c <> "\nData: " <> show d
 

src/Data/Equality/Graph/Internal.hs

@@ -6,8 +6,6 @@
  -}
 module Data.Equality.Graph.Internal where
 
-import Data.Functor.Classes
-
 import Data.Equality.Graph.ReprUnionFind
 import Data.Equality.Graph.Classes
 import Data.Equality.Graph.Nodes
@@ -31,7 +29,7 @@ type Memo l = NodeMap l ClassId
 -- | Maintained worklist of e-class ids that need to be “upward merged”
 type Worklist l = [(ClassId, ENode l)]
 
-instance (Show a, Show1 l) => Show (EGraph a l) where
+instance (Show a, Show (l ClassId)) => Show (EGraph a l) where
     show (EGraph a b c d e) =
         "UnionFind: " <> show a <>
             "\n\nE-Classes: " <> show b <>

src/Data/Equality/Graph/Lens.hs

@@ -24,7 +24,7 @@ import Data.Equality.Graph.ReprUnionFind
 
 -- | A 'Lens'' as defined in other lenses libraries
 type Lens' s a = forall f. Functor f => (a -> f a) -> (s -> f s)
-type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
+type Traversal s t a b = forall f. Applicative f => (a -> f b) -> (s -> f t)
 
 -- outdated comment for "getClass":
 --

src/Data/Equality/Graph/Monad.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE TupleSections #-}
+{-# LANGUAGE MonoLocalBinds #-}
 {-|
    Monadic interface to e-graph stateful computations
  -}

src/Data/Equality/Graph/Nodes.hs

@@ -1,10 +1,12 @@
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE DeriveGeneric #-}
-{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE UnicodeSyntax #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-|
 
 Module defining e-nodes ('ENode'), the e-node function symbol ('Operator'), and
@@ -13,7 +15,6 @@ mappings from e-nodes ('NodeMap').
 -}
 module Data.Equality.Graph.Nodes where
 
-import Data.Functor.Classes
 import Data.Foldable
 import Data.Bifunctor
 
@@ -34,6 +35,10 @@ import Data.Equality.Graph.Classes.Id
 -- parametrized over 'ClassId', i.e. all recursive fields are rather e-class ids.
 newtype ENode l = Node { unNode :: l ClassId }
 
+deriving instance Eq (l ClassId) => (Eq (ENode l))
+deriving instance Ord (l ClassId) => (Ord (ENode l))
+deriving instance Show (l ClassId) => (Show (ENode l))
+
 -- | Get the children e-class ids of an e-node
 children :: Traversable l => ENode l -> [ClassId]
 children = toList . unNode
@@ -45,68 +50,54 @@ children = toList . unNode
 -- this means children e-classes are ignored.
 newtype Operator l = Operator { unOperator :: l () }
 
+deriving instance Eq (l ()) => (Eq (Operator l))
+deriving instance Ord (l ()) => (Ord (Operator l))
+deriving instance Show (l ()) => (Show (Operator l))
+
 -- | Get the operator (function symbol) of an e-node
 operator :: Traversable l => ENode l -> Operator l
 operator = Operator . void . unNode
 {-# INLINE operator #-}
 
-instance Eq1 l => (Eq (ENode l)) where
-    (==) (Node a) (Node b) = liftEq (==) a b
-    {-# INLINE (==) #-}
-
-instance Ord1 l => (Ord (ENode l)) where
-    compare (Node a) (Node b) = liftCompare compare a b
-    {-# INLINE compare #-}
-
-instance Show1 l => (Show (ENode l)) where
-    showsPrec p (Node l) = liftShowsPrec showsPrec showList p l
-
-instance Eq1 l => (Eq (Operator l)) where
-    (==) (Operator a) (Operator b) = liftEq (\_ _ -> True) a b
-    {-# INLINE (==) #-}
-
-instance Ord1 l => (Ord (Operator l)) where
-    compare (Operator a) (Operator b) = liftCompare (\_ _ -> EQ) a b
-    {-# INLINE compare #-}
-
-instance Show1 l => (Show (Operator l)) where
-    showsPrec p (Operator l) = liftShowsPrec (const . const $ showString "") (const $ showString "") p l
-
 -- * Node Map
 
 -- | A mapping from e-nodes of @l@ to @a@
 newtype NodeMap (l :: Type -> Type) a = NodeMap { unNodeMap :: M.Map (ENode l) a }
 -- TODO: Investigate whether it would be worth it requiring a trie-map for the
 -- e-node definition. Probably it isn't better since e-nodes aren't recursive.
-  deriving (Show, Functor, Foldable, Traversable, Semigroup, Monoid)
+  deriving (Functor, Foldable, Traversable)
+
+deriving instance (Show a, Show (l ClassId)) => Show (NodeMap l a)
+deriving instance Ord (l ClassId) => Semigroup (NodeMap l a)
+deriving instance Ord (l ClassId) => Monoid (NodeMap l a)
 
 -- | Insert a value given an e-node in a 'NodeMap'
-insertNM :: Ord1 l => ENode l -> a -> NodeMap l a -> NodeMap l a
+insertNM :: Ord (l ClassId) => ENode l -> a -> NodeMap l a -> NodeMap l a
 insertNM e v (NodeMap m) = NodeMap (M.insert e v m)
 {-# INLINE insertNM #-}
 
 -- | Lookup an e-node in a 'NodeMap'
-lookupNM :: Ord1 l => ENode l -> NodeMap l a -> Maybe a
+lookupNM :: Ord (l ClassId) => ENode l -> NodeMap l a -> Maybe a
 lookupNM e = M.lookup e . unNodeMap
 {-# INLINE lookupNM #-}
 
 -- | Delete an e-node in a 'NodeMap'
-deleteNM :: Ord1 l => ENode l -> NodeMap l a -> NodeMap l a
+deleteNM :: Ord (l ClassId) => ENode l -> NodeMap l a -> NodeMap l a
 deleteNM e (NodeMap m) = NodeMap (M.delete e m)
 {-# INLINE deleteNM #-}
 
 -- | Insert a value and lookup by e-node in a 'NodeMap'
-insertLookupNM :: Ord1 l => ENode l -> a -> NodeMap l a -> (Maybe a, NodeMap l a)
+insertLookupNM :: Ord (l ClassId) => ENode l -> a -> NodeMap l a -> (Maybe a, NodeMap l a)
 insertLookupNM e v (NodeMap m) = second NodeMap $ M.insertLookupWithKey (\_ a _ -> a) e v m
 {-# INLINE insertLookupNM #-}
 
 -- | As 'Data.Map.foldlWithKeyNM'' but in a 'NodeMap'
-foldlWithKeyNM' :: Ord1 l => (b -> ENode l -> a -> b) -> b -> NodeMap l a -> b 
+foldlWithKeyNM' :: Ord (l ClassId) => (b -> ENode l -> a -> b) -> b -> NodeMap l a -> b 
 foldlWithKeyNM' f b = M.foldlWithKey' f b . unNodeMap
 {-# INLINE foldlWithKeyNM' #-}
 
 -- | As 'Data.Map.foldrWithKeyNM'' but in a 'NodeMap'
-foldrWithKeyNM' :: Ord1 l => (ENode l -> a -> b -> b) -> b -> NodeMap l a -> b 
+foldrWithKeyNM' :: Ord (l ClassId) => (ENode l -> a -> b -> b) -> b -> NodeMap l a -> b 
 foldrWithKeyNM' f b = M.foldrWithKey' f b . unNodeMap
 {-# INLINE foldrWithKeyNM' #-}
 

src/Data/Equality/Language.hs

@@ -1,5 +1,11 @@
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-|
 
 Defines 'Language', which is the required constraint on /expressions/ that are
@@ -29,7 +35,7 @@ instance Language Expr
 -}
 module Data.Equality.Language where
 
-import Data.Functor.Classes
+import Data.Kind
 
 -- | A 'Language' is the required constraint on /expressions/ that are to be
 -- represented in an e-graph.
@@ -39,5 +45,7 @@ import Data.Functor.Classes
 -- e-graphs), note that it must satisfy the other class constraints. In
 -- particular an 'Data.Equality.Analysis.Analysis' must be defined for the
 -- language.
-type Language l = (Traversable l, Ord1 l)
+type Language :: (Type -> Type) -> Constraint
+class (∀ a. Ord a => Ord (l a), Traversable l) => Language l
+instance (∀ a. Ord a => Ord (l a), Traversable l) => Language l