diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil.hs b/haskell/free-foil/src/Control/Monad/Free/Foil.hs index bdb3438c..6f768cbd 100644 --- a/haskell/free-foil/src/Control/Monad/Free/Foil.hs +++ b/haskell/free-foil/src/Control/Monad/Free/Foil.hs @@ -23,6 +23,7 @@ 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.ZipMatchK import Data.Coerce (coerce) @@ -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, ZipMatchK 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,7 +179,7 @@ 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, ZipMatchK 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 @@ -192,7 +193,7 @@ alphaEquiv _ _ _ = False -- | Same as 'alphaEquiv' but for scoped terms. alphaEquivScoped - :: (Bifunctor sig, Bifoldable sig, ZipMatchK 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,7 +238,7 @@ alphaEquivScoped scope -- scope extensions under binders (which might happen due to substitution -- under a binder in absence of name conflicts). unsafeEqAST - :: (Bifoldable sig, ZipMatchK 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 @@ -250,7 +251,7 @@ unsafeEqAST _ _ = False -- | A version of 'unsafeEqAST' for scoped terms. unsafeEqScopedAST - :: (Bifoldable sig, ZipMatchK 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 diff --git a/haskell/free-foil/src/Data/ZipMatchK.hs b/haskell/free-foil/src/Data/ZipMatchK.hs index a1151319..0d979137 100644 --- a/haskell/free-foil/src/Data/ZipMatchK.hs +++ b/haskell/free-foil/src/Data/ZipMatchK.hs @@ -1,3 +1,4 @@ +{-# OPTIONS_GHC -Wno-redundant-constraints #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE RankNTypes #-} @@ -7,30 +8,73 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} +-- | Kind-polymorphic syntactic (first-order) unification. module Data.ZipMatchK ( module Data.ZipMatchK.Mappings, ZipMatchK(..), zipMatchK, - zipMatch2, + -- * Specializations + -- ** Unification of plain 'Type's zipMatchViaEq, zipMatchViaChooseLeft, + -- ** Unification of '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 -zipMatch2 :: forall f a b a' b'. (ZipMatchK f) => f a b -> f a' b' -> Maybe (f (a, a') (b, b')) -zipMatch2 = zipMatchK @f @(a :&&: b :&&: LoT0) @(a' :&&: b' :&&: LoT0) - +-- | Unify values via 'Eq'. +-- Can be used as an implementation of 'zipMatchWithK' when @k = '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 = '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 diff --git a/haskell/free-foil/src/Data/ZipMatchK/Bifunctor.hs b/haskell/free-foil/src/Data/ZipMatchK/Bifunctor.hs index 5d752440..9a758218 100644 --- a/haskell/free-foil/src/Data/ZipMatchK/Bifunctor.hs +++ b/haskell/free-foil/src/Data/ZipMatchK/Bifunctor.hs @@ -8,6 +8,8 @@ {-# 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) @@ -26,5 +28,7 @@ instance GenericK (Product f g) where Field ((Kon f :@: Var0) :@: Var1) :*: Field ((Kon g :@: Var0) :@: Var1) -instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum (f :: Type -> Type -> Type) g) -instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Product (f :: Type -> Type -> Type) g) +-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@. +instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f (g :: Type -> Type -> Type)) +-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@. +instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f (g :: Type -> Type -> Type)) diff --git a/haskell/free-foil/src/Data/ZipMatchK/Generic.hs b/haskell/free-foil/src/Data/ZipMatchK/Generic.hs index a8da90ab..109ff9f9 100644 --- a/haskell/free-foil/src/Data/ZipMatchK/Generic.hs +++ b/haskell/free-foil/src/Data/ZipMatchK/Generic.hs @@ -1,4 +1,4 @@ -{-# OPTIONS_GHC -Wno-missing-methods #-} +{-# OPTIONS_GHC -Wno-missing-methods -Wno-orphans #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} @@ -24,18 +24,30 @@ import Generics.Kind.Examples () import GHC.TypeError import Data.ZipMatchK.Mappings +-- | Kind-polymorphic syntactic (first-order) unification of two values. +-- +-- Note: @f@ is expected to be a traversable n-functor, +-- but at the moment we lack a @TraversableK@ constraint. class ZipMatchK (f :: k) where + -- | Perform one level of equality testing: + -- + -- * when @k = 'Type'@, values are compared directly (e.g. via 'Eq'); + -- * when @k = 'Type' -> 'Type'@, we compare term constructors; + -- if term constructors are unequal, we return 'Nothing'; + -- otherwise, we pair up all components with a given function. zipMatchWithK :: forall as bs cs. Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs) default zipMatchWithK :: forall as bs cs. (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs) => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs) zipMatchWithK = genericZipMatchWithK @f @as @bs @cs +-- | Generic implementation of 'Data.ZipMatch.zipMatchK'. genericZipMatchK :: forall f as bs. (GenericK f, GZipMatch (RepK f), ReqsZipMatch (RepK f) as bs, PairMappings as bs) => f :@@: as -> f :@@: bs -> Maybe (f :@@: (ZipLoT as bs)) genericZipMatchK = genericZipMatchWithK @f @as @bs pairMappings +-- | Generic implementation of 'zipMatchWithK'. genericZipMatchWithK :: forall f as bs cs. (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs) => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs) @@ -43,13 +55,13 @@ genericZipMatchWithK mappings x y = toK @_ @f @cs <$> gzipMatchWith mappings (fromK @_ @f @as x) (fromK @_ @f @bs y) -genericZipMatch2 - :: forall sig scope scope' term term'. - (GenericK sig, GZipMatch (RepK sig), ReqsZipMatch (RepK sig) (scope :&&: term :&&: 'LoT0) (scope' :&&: term' :&&: 'LoT0)) - => sig scope term -> sig scope' term' -> Maybe (sig (scope, scope') (term, term')) -genericZipMatch2 = genericZipMatchK @sig @(scope :&&: term :&&: 'LoT0) @(scope' :&&: term' :&&: 'LoT0) +instance GenericK (,) where + type RepK (,) = Field Var0 :*: Field Var1 +instance GenericK ((,) a) where + type RepK ((,) a) = Field (Kon a) :*: Field Var0 --- instance ZipMatchK (,) -- missing GenericK instance upstream +instance ZipMatchK (,) +instance ZipMatchK a => ZipMatchK ((,) a) instance ZipMatchK [] instance ZipMatchK Maybe instance ZipMatchK Either @@ -110,7 +122,7 @@ instance ZipMatchK k => ZipMatchFields (Kon k) where type ReqsZipMatchFieldsWith (Kon k) as bs cs = () zipMatchFieldsWith _ (Field l) (Field r) = Field <$> zipMatchWithK @_ @k M0 l r -instance (ZipMatchFields t, ZipMatchK k) => ZipMatchFields (Kon k :@: t) where +instance {-# OVERLAPPING #-} (ZipMatchFields t, ZipMatchK k) => ZipMatchFields (Kon k :@: t) where type ReqsZipMatchFieldsWith (Kon k :@: t) as bs cs = ReqsZipMatchFieldsWith t as bs cs zipMatchFieldsWith :: forall as bs cs. ReqsZipMatchFieldsWith (Kon k :@: t) as bs cs => @@ -130,6 +142,24 @@ instance {-# OVERLAPPING #-} (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k) :^: ((\ll rr -> unField @t2 <$> zipMatchFieldsWith g (Field ll) (Field rr)) :^: M0)) l r +instance {-# OVERLAPPABLE #-} TypeError + ('Text "The type constructor is kind-polymorphic:" + :$$: 'Text " " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (kk -> Type) + :$$: 'Text "Possible fix:" + :$$: 'Text " add an explicit kind signature" + :$$: 'Text " " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (Type -> Type)) + => ZipMatchFields (Kon (k :: kk -> Type) :@: t) where + zipMatchFieldsWith = undefined + +instance {-# OVERLAPPABLE #-} TypeError + ('Text "The type constructor is kind-polymorphic:" + :$$: 'Text " " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (kk1 -> kk2 -> Type) + :$$: 'Text "Possible fix:" + :$$: 'Text " add an explicit kind signature" + :$$: 'Text " " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (Type -> Type -> Type)) + => ZipMatchFields ((Kon (k :: kk1 -> kk2 -> Type) :@: t1) :@: t2) where + zipMatchFieldsWith = undefined + instance {-# OVERLAPPABLE #-} TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form:" :$$: 'Text " when attempting to use a generic instance for" @@ -139,24 +169,21 @@ instance {-# OVERLAPPABLE #-} TypeError -- type ReqsZipMatchFieldsWith (f :@: t) as bs cs = TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form") zipMatchFieldsWith = undefined -instance TypeError ('Text "Atom ForAll is not supported by ZipMatchFields") => ZipMatchFields (ForAll a) where +instance TypeError + ('Text "Atom ForAll is not supported by ZipMatchFields" + :$$: 'Text " when attempting to use a generic instance for" + :$$: 'ShowType (ForAll a)) => ZipMatchFields (ForAll a) where type ReqsZipMatchFieldsWith (ForAll a) as bs cs = TypeError ('Text "Atom ForAll is not supported by ZipMatchFields") zipMatchFieldsWith = undefined -instance TypeError ('Text "Atom :=>>: is not supported by ZipMatchFields") => ZipMatchFields (c :=>>: a) where +instance TypeError + ('Text "Atom :=>>: is not supported by ZipMatchFields" + :$$: 'Text " when attempting to use a generic instance for" + :$$: 'ShowType (c :=>>: a)) => ZipMatchFields (c :=>>: a) where type ReqsZipMatchFieldsWith (c :=>>: a) as bs cs = TypeError ('Text "Atom :=>>: is not supported by ZipMatchFields") zipMatchFieldsWith = undefined -instance TypeError ('Text "Atom Eval is not supported by ZipMatchFields") => ZipMatchFields (Eval a) where +instance TypeError + ('Text "Atom Eval is not supported by ZipMatchFields" + :$$: 'Text " when attempting to use a generic instance for" + :$$: 'ShowType (Eval a)) => ZipMatchFields (Eval a) where type ReqsZipMatchFieldsWith (Eval a) as bs cs = TypeError ('Text "Atom Eval is not supported by ZipMatchFields") zipMatchFieldsWith = undefined - --- instance ZipMatchFields (ForAll f) where --- type ReqsZipMatchFields (ForAll f) as bs = ??? --- zipMatchFields = ??? - --- instance ZipMatchFields (c :=>>: f) where --- type ReqsZipMatchFields (c :=>>: f) as bs = ??? --- zipMatchFields = ??? - --- instance ZipMatchFields (Eval f) where --- type ReqsZipMatchFields (Eval f) as bs = ??? --- zipMatchFields = ??? diff --git a/haskell/free-foil/src/Data/ZipMatchK/Mappings.hs b/haskell/free-foil/src/Data/ZipMatchK/Mappings.hs index 9cdef001..e18836a4 100644 --- a/haskell/free-foil/src/Data/ZipMatchK/Mappings.hs +++ b/haskell/free-foil/src/Data/ZipMatchK/Mappings.hs @@ -14,31 +14,47 @@ module Data.ZipMatchK.Mappings where import Data.Kind (Type) import Generics.Kind +-- | Zip to lists of types into a single list of pair types. type ZipLoT :: LoT k -> LoT k -> LoT k type family ZipLoT as bs where ZipLoT LoT0 LoT0 = LoT0 ZipLoT (a :&&: as) (b :&&: bs) = ((a, b) :&&: ZipLoT as bs) +infixr 5 :^: type Mappings :: LoT k -> LoT k -> LoT k -> Type +-- | A collection of zipping functions for 'Data.ZipMatchK.zipMatchWithK'. data Mappings (as :: LoT k) (bs :: LoT k) (cs :: LoT k) where + -- | An empty collection (when there no (more) type parameters). M0 :: Mappings LoT0 LoT0 LoT0 - (:^:) :: (a -> b -> Maybe c) -> Mappings as bs cs -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs) + -- | A non-empty collection (when there is at least one type parameter). + (:^:) :: (a -> b -> Maybe c) -- ^ Zipping for the first type parameter. + -> Mappings as bs cs -- ^ Zipping for other type parameters. + -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs) class PairMappings (as :: LoT k) (bs :: LoT k) where + -- | A collection of pairing functions @(\\x y -> Just (x, y))@ for 'Data.ZipMatchK.zipMatchK'. pairMappings :: Mappings as bs (ZipLoT as bs) instance PairMappings LoT0 LoT0 where pairMappings = M0 instance PairMappings as bs => PairMappings ((a :: Type) :&&: as) ((b :: Type) :&&: bs) where - pairMappings = (\x y -> Just (x, y)) :^: pairMappings + pairMappings = pairA :^: pairMappings class ApplyMappings (v :: TyVar d Type) where + -- | Apply a collection of zipping functions to collections of values. applyMappings :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d). - Mappings as bs cs -> Interpret (Var v) as -> Interpret (Var v) bs -> Maybe (Interpret (Var v) cs) + Mappings as bs cs -- ^ A collection of zipping functions. + -> Interpret (Var v) as -- ^ First collection of values (one per type parameter). + -> Interpret (Var v) bs -- ^ Second collection of values (one per type parameter). + -> Maybe (Interpret (Var v) cs) instance ApplyMappings (VZ :: TyVar (Type -> tys) Type) where applyMappings (f :^: _) x y = f x y instance ApplyMappings v => ApplyMappings (VS v :: TyVar (ty -> tys) Type) where applyMappings (_ :^: fs) x y = applyMappings @_ @v fs x y + +-- | Pair two values in a context. +pairA :: Applicative f => a -> b -> f (a, b) +pairA x y = pure (x, y)