Merge pull request #30 from fizruk/data-zipmathk

Factor out Data.ZipMatchK, remove ZipMatch

haskell/free-foil/free-foil.cabal

@@ -40,13 +40,16 @@ library
       Control.Monad.Foil.TH.Util
       Control.Monad.Free.Foil
       Control.Monad.Free.Foil.Example
-      Control.Monad.Free.Foil.Generic
       Control.Monad.Free.Foil.TH
       Control.Monad.Free.Foil.TH.Convert
       Control.Monad.Free.Foil.TH.MkFreeFoil
       Control.Monad.Free.Foil.TH.PatternSynonyms
       Control.Monad.Free.Foil.TH.Signature
-      Control.Monad.Free.Foil.TH.ZipMatch
+      Data.ZipMatchK
+      Data.ZipMatchK.Bifunctor
+      Data.ZipMatchK.Functor
+      Data.ZipMatchK.Generic
+      Data.ZipMatchK.Mappings
   other-modules:
       Paths_free_foil
   hs-source-dirs:

haskell/free-foil/src/Control/Monad/Free/Foil.hs

@@ -23,8 +23,9 @@ import           Control.DeepSeq
 import qualified Control.Monad.Foil.Internal as Foil
 import qualified Control.Monad.Foil.Relative as Foil
 import           Data.Bifoldable
+import           Data.Bitraversable
 import           Data.Bifunctor
-import           Data.Bifunctor.Sum
+import Data.ZipMatchK
 import           Data.Coerce                 (coerce)
 import           Data.Map                    (Map)
 import qualified Data.Map                    as Map
@@ -165,7 +166,7 @@ refreshScopedAST scope (ScopedAST binder body) =
 -- Compared to 'alphaEquiv', this function may perform some unnecessary
 -- changes of bound variables when the binders are the same on both sides.
 alphaEquivRefreshed
-  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
@@ -178,21 +179,21 @@ alphaEquivRefreshed scope t1 t2 = refreshAST scope t1 `unsafeEqAST` refreshAST s
 -- Compared to 'alphaEquivRefreshed', this function might skip unnecessary
 -- changes of bound variables when both binders in two matching scoped terms coincide.
 alphaEquiv
-  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
   -> Bool
 alphaEquiv _scope (Var x) (Var y) = x == coerce y
 alphaEquiv scope (Node l) (Node r) =
-  case zipMatch l r of
+  case zipMatch2 l r of
     Nothing -> False
     Just tt -> getAll (bifoldMap (All . uncurry (alphaEquivScoped scope)) (All . uncurry (alphaEquiv scope)) tt)
 alphaEquiv _ _ _ = False
 
 -- | Same as 'alphaEquiv' but for scoped terms.
 alphaEquivScoped
-  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> ScopedAST binder sig n
   -> ScopedAST binder sig n
@@ -237,20 +238,20 @@ alphaEquivScoped scope
 -- scope extensions under binders (which might happen due to substitution
 -- under a binder in absence of name conflicts).
 unsafeEqAST
-  :: (Bifoldable sig, ZipMatch sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => AST binder sig n
   -> AST binder sig l
   -> Bool
 unsafeEqAST (Var x) (Var y) = x == coerce y
 unsafeEqAST (Node t1) (Node t2) =
-  case zipMatch t1 t2 of
+  case zipMatch2 t1 t2 of
     Nothing -> False
     Just tt -> getAll (bifoldMap (All . uncurry unsafeEqScopedAST) (All . uncurry unsafeEqAST) tt)
 unsafeEqAST _ _ = False
 
 -- | A version of 'unsafeEqAST' for scoped terms.
 unsafeEqScopedAST
-  :: (Bifoldable sig, ZipMatch sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => ScopedAST binder sig n
   -> ScopedAST binder sig l
   -> Bool
@@ -260,20 +261,6 @@ unsafeEqScopedAST (ScopedAST binder1 body1) (ScopedAST binder2 body2) = and
       (Foil.Distinct, Foil.Distinct) -> body1 `unsafeEqAST` body2
   ]
 
--- ** Syntactic matching (unification)
-
--- | Perform one-level matching for the two (non-variable) terms.
-class ZipMatch sig where
-  zipMatch
-    :: sig scope term     -- ^ Left non-variable term.
-    -> sig scope' term'   -- ^ Right non-variable term.
-    -> Maybe (sig (scope, scope') (term, term'))
-
-instance (ZipMatch f, ZipMatch g) => ZipMatch (Sum f g) where
-  zipMatch (L2 f) (L2 f') = L2 <$> zipMatch f f'
-  zipMatch (R2 g) (R2 g') = R2 <$> zipMatch g g'
-  zipMatch _ _            = Nothing
-
 -- * Converting to and from free foil
 
 -- ** Convert to free foil

haskell/free-foil/src/Control/Monad/Free/Foil/TH.hs

@@ -2,10 +2,8 @@ module Control.Monad.Free.Foil.TH (
   module Control.Monad.Free.Foil.TH.Signature,
   module Control.Monad.Free.Foil.TH.PatternSynonyms,
   module Control.Monad.Free.Foil.TH.Convert,
-  module Control.Monad.Free.Foil.TH.ZipMatch,
 ) where
 
 import Control.Monad.Free.Foil.TH.Signature
 import Control.Monad.Free.Foil.TH.PatternSynonyms
 import Control.Monad.Free.Foil.TH.Convert
-import Control.Monad.Free.Foil.TH.ZipMatch

haskell/free-foil/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs

@@ -83,7 +83,7 @@ mkPatternSynonym signatureType scope term = \case
       where
         l = mkName ("l" ++ show i)
 
-    mkPatternName conName = mkName (dropEnd (length "Sig") (nameBase conName))
+    mkPatternName conName = mkName (dropEnd (length ("Sig" :: String)) (nameBase conName))
     dropEnd k = reverse . drop k . reverse
 
     collapse = \case

haskell/free-foil/src/Data/ZipMatchK.hs

@@ -0,0 +1,80 @@
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+-- | Kind-polymorphic syntactic (first-order) unification.
+module Data.ZipMatchK (
+  module Data.ZipMatchK.Mappings,
+  ZipMatchK(..),
+  zipMatchK,
+  -- * Specializations
+  -- ** Unification of plain 'Data.Kind.Type's
+  zipMatchViaEq,
+  zipMatchViaChooseLeft,
+  -- ** Unification of 'Data.Functor.Functor's
+  zipMatchWith1,
+  zipMatch1,
+  -- ** Unification of 'Data.Bifunctor.Bifunctor's
+  zipMatchWith2,
+  zipMatch2,
+) where
+
+import           Generics.Kind
+import Data.Bitraversable
+
+import Data.ZipMatchK.Generic
+import Data.ZipMatchK.Mappings
+
+-- | Perform one level of equality testing for two values and pair up components using @(,)@:
+--
+-- > zipMatchK = zipMatchWithK (\x y -> Just (,) :^: M0)
+zipMatchK :: forall f as bs. (ZipMatchK f, PairMappings as bs) => f :@@: as -> f :@@: bs -> Maybe (f :@@: ZipLoT as bs)
+zipMatchK = zipMatchWithK @_ @f @as @bs pairMappings
+
+-- | Unify values via 'Eq'.
+-- Can be used as an implementation of 'zipMatchWithK' when @k = 'Data.Kind.Type'@.
+zipMatchViaEq :: Eq a => Mappings as bs cs -> a -> a -> Maybe a
+zipMatchViaEq _ x y
+  | x == y = Just x
+  | otherwise = Nothing
+
+-- | Always successfully unify any two values of type @a@ by preferring the left value.
+-- Can be used as an implementation of 'zipMatchWithK' when @k = 'Data.Kind.Type'@.
+zipMatchViaChooseLeft :: Mappings as bs cs -> a -> a -> Maybe a
+zipMatchViaChooseLeft _ x _ = Just x
+
+-- | 'zipMatchWithK' specialised to functors.
+--
+-- Note: 'Traversable' is a morally correct constraint here.
+zipMatchWith1
+  :: (Traversable f, ZipMatchK f)
+  => (a -> a' -> Maybe a'')
+  -> f a -> f a' -> Maybe (f a'')
+zipMatchWith1 f = zipMatchWithK (f :^: M0)
+
+-- | 'zipMatchK' specialised to functors.
+--
+-- Note: 'Traversable' is a morally correct constraint here.
+zipMatch1 :: (Traversable f, ZipMatchK f) => f a -> f a' -> Maybe (f (a, a'))
+zipMatch1 = zipMatchWith1 pairA
+-- | 'zipMatchWithK' specialised to bifunctors.
+--
+-- Note: 'Bitraversable' is a morally correct constraint here.
+zipMatchWith2
+  :: (Bitraversable f, ZipMatchK f)
+  => (a -> a' -> Maybe a'')
+  -> (b -> b' -> Maybe b'')
+  -> f a b -> f a' b' -> Maybe (f a'' b'')
+zipMatchWith2 f g = zipMatchWithK (f :^: g :^: M0)
+
+-- | 'zipMatchK' specialised to bifunctors.
+--
+-- Note: 'Bitraversable' is a morally correct constraint here.
+zipMatch2 :: (Bitraversable f, ZipMatchK f) => f a b -> f a' b' -> Maybe (f (a, a') (b, b'))
+zipMatch2 = zipMatchWith2 pairA pairA

haskell/free-foil/src/Data/ZipMatchK/Bifunctor.hs

@@ -0,0 +1,35 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+-- | This module provides 'GenericK' and 'ZipMatchK' instances for 'Sum' and 'Product',
+-- to enable the use of 'ZipMatchK' with the data types à la carte approach.
+module Data.ZipMatchK.Bifunctor where
+
+import Data.Kind (Type)
+import Generics.Kind
+import Data.Bitraversable
+import Data.Bifunctor.Sum
+import Data.Bifunctor.Product
+
+import Data.ZipMatchK
+
+instance GenericK (Sum f g) where
+  type RepK (Sum f g) =
+    Field ((Kon f :@: Var0) :@: Var1)
+    :+: Field ((Kon g :@: Var0) :@: Var1)
+instance GenericK (Product f g) where
+  type RepK (Product f g) =
+    Field ((Kon f :@: Var0) :@: Var1)
+    :*: Field ((Kon g :@: Var0) :@: Var1)
+
+-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.
+instance (Bitraversable f, Bitraversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f (g :: Type -> Type -> Type))
+-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.
+instance (Bitraversable f, Bitraversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f (g :: Type -> Type -> Type))

haskell/free-foil/src/Data/ZipMatchK/Functor.hs

@@ -0,0 +1,34 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+-- | This module provides 'GenericK' and 'ZipMatchK' instances for 'Sum' and 'Product',
+-- to enable the use of 'ZipMatchK' with the data types à la carte approach.
+module Data.ZipMatchK.Functor where
+
+import Data.Kind (Type)
+import Generics.Kind
+import Data.Functor.Sum
+import Data.Functor.Product
+
+import Data.ZipMatchK
+
+instance GenericK (Sum f g) where
+  type RepK (Sum f g) =
+    Field (Kon f :@: Var0)
+    :+: Field (Kon g :@: Var0)
+instance GenericK (Product f g) where
+  type RepK (Product f g) =
+    Field (Kon f :@: Var0)
+    :*: Field (Kon g :@: Var0)
+
+-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.
+instance (Traversable f, Traversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f (g :: Type -> Type))
+-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.
+instance (Traversable f, Traversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f (g :: Type -> Type))