Merge pull request #27 from fizruk/generic-zip-match

Generic ZipMatch instances

haskell/free-foil/free-foil.cabal

@@ -1,6 +1,6 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.36.0.
+-- This file has been generated from package.yaml by hpack version 0.37.0.
 --
 -- see: https://github.com/sol/hpack
 
@@ -40,6 +40,7 @@ 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.PatternSynonyms
@@ -56,6 +57,7 @@ library
     , bifunctors
     , containers
     , deepseq
+    , kind-generics >=0.5.0
     , template-haskell >=2.21.0.0
     , text >=1.2.3.1
   default-language: Haskell2010
@@ -75,6 +77,7 @@ test-suite doctests
     , deepseq
     , doctest-parallel
     , free-foil
+    , kind-generics >=0.5.0
     , template-haskell >=2.21.0.0
     , text >=1.2.3.1
   default-language: Haskell2010
@@ -94,6 +97,7 @@ test-suite spec
     , containers
     , deepseq
     , free-foil
+    , kind-generics >=0.5.0
     , template-haskell >=2.21.0.0
     , text >=1.2.3.1
   default-language: Haskell2010

haskell/free-foil/package.yaml

@@ -27,6 +27,7 @@ dependencies:
   bifunctors:
   template-haskell: ">= 2.21.0.0"
   deepseq:
+  kind-generics: ">= 0.5.0"
 
 ghc-options:
   - -Wall

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

@@ -0,0 +1,196 @@
+{-# OPTIONS_GHC -Wno-missing-methods #-}
+{-# LANGUAGE AllowAmbiguousTypes      #-}
+{-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE ConstraintKinds      #-}
+{-# LANGUAGE GADTs      #-}
+{-# LANGUAGE InstanceSigs      #-}
+{-# LANGUAGE DefaultSignatures      #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE DataKinds                #-}
+{-# LANGUAGE FlexibleContexts         #-}
+{-# LANGUAGE PolyKinds                #-}
+{-# LANGUAGE RankNTypes               #-}
+{-# LANGUAGE ScopedTypeVariables      #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications         #-}
+{-# LANGUAGE TypeFamilies             #-}
+{-# LANGUAGE TypeOperators            #-}
+{-# LANGUAGE UndecidableInstances     #-}
+module Control.Monad.Free.Foil.Generic where
+
+import           Data.Kind     (Constraint, Type)
+import           Generics.Kind
+import           Generics.Kind.Examples ()
+import           GHC.TypeError
+
+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)
+
+type Mappings :: LoT k -> LoT k -> LoT k -> Type
+data Mappings (as :: LoT k) (bs :: LoT k) (cs :: LoT k) where
+  M0 :: Mappings LoT0 LoT0 LoT0
+  (:^:) :: (a -> b -> Maybe c) -> Mappings as bs cs -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs)
+
+class PairMappings (as :: LoT k) (bs :: LoT k) where
+  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
+
+class ApplyMappings (v :: TyVar d Type) where
+  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)
+
+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
+
+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
+
+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)
+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)
+
+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
+
+class ZipMatchK (f :: k) where
+  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
+
+zipMatchViaEq :: Eq a => Mappings as bs cs -> a -> a -> Maybe a
+zipMatchViaEq _ x y
+  | x == y = Just x
+  | otherwise = Nothing
+
+zipMatchViaChooseLeft :: Mappings as bs cs -> a -> a -> Maybe a
+zipMatchViaChooseLeft _ x _ = Just x
+
+-- instance ZipMatchK (,)     -- missing GenericK instance upstream
+instance ZipMatchK []
+instance ZipMatchK Maybe
+instance ZipMatchK Either
+instance ZipMatchK a => ZipMatchK (Either a)
+
+type ReqsZipMatch f as bs = ReqsZipMatchWith f as bs (ZipLoT as bs)
+class GZipMatch (f :: LoT k -> Type) where
+  type ReqsZipMatchWith f (as :: LoT k) (bs :: LoT k) (cs :: LoT k) :: Constraint
+  gzipMatchWith :: ReqsZipMatchWith f as bs cs => Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
+
+instance GZipMatch V1 where
+  type ReqsZipMatchWith V1 as bs cs = ()
+  gzipMatchWith _ _ _ = error "impossible: Generics.Kind.V1 value!" -- FIXME: should be absurd
+
+instance GZipMatch U1 where
+  type ReqsZipMatchWith U1 as bs cs = ()
+  gzipMatchWith _ U1 U1 = Just U1
+
+instance GZipMatch f => GZipMatch (M1 i c f) where
+  type ReqsZipMatchWith (M1 i c f) as bs cs = ReqsZipMatchWith f as bs cs
+  gzipMatchWith g (M1 x) (M1 y) = M1 <$> gzipMatchWith g x y
+
+instance (GZipMatch f, GZipMatch g) => GZipMatch (f :+: g) where
+  type ReqsZipMatchWith (f :+: g) as bs cs = (ReqsZipMatchWith f as bs cs, ReqsZipMatchWith g as bs cs)
+  gzipMatchWith g (L1 x) (L1 y) = L1 <$> gzipMatchWith g x y
+  gzipMatchWith g (R1 x) (R1 y) = R1 <$> gzipMatchWith g x y
+  gzipMatchWith _ _ _           = Nothing
+
+instance (GZipMatch f, GZipMatch g) => GZipMatch (f :*: g) where
+  type ReqsZipMatchWith (f :*: g) as bs cs = (ReqsZipMatchWith f as bs cs, ReqsZipMatchWith g as bs cs)
+  gzipMatchWith g (x :*: y) (x' :*: y') =
+    liftA2 (:*:) (gzipMatchWith g x x') (gzipMatchWith g y y')
+
+instance ZipMatchFields t => GZipMatch (Field t) where
+  type ReqsZipMatchWith (Field t) as bs cs = ReqsZipMatchFieldsWith t as bs cs
+  gzipMatchWith f x y = zipMatchFieldsWith f x y
+
+instance GZipMatch f => GZipMatch (c :=>: f) where
+  type ReqsZipMatchWith (c :=>: f) as bs cs = (ReqsZipMatchWith f as bs cs, Interpret c cs)
+  -- really we want          = (Interpret c as, Interpret c bs) => (ReqsZipMatch f as bs, Interpret c (ZipLoT as bs))
+  gzipMatchWith g (SuchThat x) (SuchThat y) = SuchThat <$> gzipMatchWith g x y
+
+instance TypeError ('Text "Existentials are not supported")
+         => GZipMatch (Exists k f) where
+  type ReqsZipMatchWith (Exists k f) as bs cs = TypeError ('Text "Existentials are not supported")
+  gzipMatchWith = undefined
+
+class ZipMatchFields (t :: Atom d Type) where
+  type ReqsZipMatchFieldsWith t (as :: LoT d) (bs :: LoT d) (cs :: LoT d) :: Constraint
+  zipMatchFieldsWith :: ReqsZipMatchFieldsWith t as bs cs => Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)
+
+instance ApplyMappings v => ZipMatchFields (Var v) where
+  -- this is always true, but GHC is not smart enough to know that, I think
+  type ReqsZipMatchFieldsWith (Var v) as bs cs = () -- InterpretVar v cs ~ (InterpretVar v as, InterpretVar v bs))
+  zipMatchFieldsWith g (Field x) (Field y) = Field <$> applyMappings @_ @v g x y
+
+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
+  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 =>
+    Mappings as bs cs -> Field (Kon k :@: t) as -> Field (Kon k :@: t) bs -> Maybe (Field (Kon k :@: t) cs)
+  zipMatchFieldsWith g (Field l) (Field r) =
+    Field <$> zipMatchWithK @_ @k @(Interpret t as :&&: LoT0) @(Interpret t bs :&&: LoT0) @(Interpret t cs :&&: LoT0)
+      ((\ll rr -> unField @t <$> zipMatchFieldsWith g (Field ll) (Field rr)) :^: M0) l r
+
+instance (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k) => ZipMatchFields ((Kon k :@: t1) :@: t2) where
+  type ReqsZipMatchFieldsWith ((Kon k :@: t1) :@: t2) as bs cs = (ReqsZipMatchFieldsWith t1 as bs cs, ReqsZipMatchFieldsWith t2 as bs cs)
+
+  zipMatchFieldsWith :: forall as bs cs. ReqsZipMatchFieldsWith ((Kon k :@: t1) :@: t2) as bs cs =>
+    Mappings as bs cs -> Field ((Kon k :@: t1) :@: t2) as -> Field ((Kon k :@: t1) :@: t2) bs -> Maybe (Field ((Kon k :@: t1) :@: t2) cs)
+  zipMatchFieldsWith g (Field l) (Field r) =
+    Field <$> zipMatchWithK @_ @k @(Interpret t1 as :&&: Interpret t2 as :&&: LoT0) @(Interpret t1 bs :&&: Interpret t2 bs :&&: LoT0) @(Interpret t1 cs :&&: Interpret t2 cs :&&: LoT0)
+      ((\ll rr -> unField @t1 <$> zipMatchFieldsWith g (Field ll) (Field rr))
+        :^: ((\ll rr -> unField @t2 <$> zipMatchFieldsWith g (Field ll) (Field rr))
+        :^: M0)) l r
+
+instance {-# OVERLAPPABLE #-} TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form") => ZipMatchFields (f :@: t) where
+  -- 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
+  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
+  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
+  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 = ???

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

@@ -69,21 +69,56 @@ mkPatternSynonym signatureType scope term = \case
       Left ((b, _), (x, _)) -> ConP 'ScopedAST [] [VarP b, VarP x]
       Right (x, _) -> VarP x
 
-    toPatternArgType i (_bang, VarT typeName)
+    toPatternArgType i (_bang, type_@(VarT typeName))
       | typeName == scope =
           Left
             ( (mkName ("b" ++ show i), foldl AppT binderT [VarT n, VarT l])
-            , (mkName ("x" ++ show i), PeelConT ''AST [binderT, signatureType, VarT l]))
+            , (mkName ("x" ++ show i), replaceScopeTermInType l type_))
       | typeName == term =
-          Right (mkName ("x" ++ show i), PeelConT ''AST [binderT, signatureType, VarT n])
+          Right (mkName ("x" ++ show i), replaceScopeTermInType l type_)
       where
         l = mkName ("l" ++ show i)
     toPatternArgType i (_bang, type_)
-      = Right (mkName ("z" ++ show i), type_)
+      = Right (mkName ("z" ++ show i), replaceScopeTermInType l type_)
+      where
+        l = mkName ("l" ++ show i)
 
     mkPatternName conName = mkName (dropEnd (length "Sig") (nameBase conName))
     dropEnd k = reverse . drop k . reverse
 
     collapse = \case
       Left (x, y) -> [x, y]
       Right x -> [x]
+
+    replaceScopeTermInType lscope = \case
+      VarT typeName
+        | typeName == scope -> PeelConT ''AST [binderT, signatureType, VarT lscope]
+        | typeName == term  -> PeelConT ''AST [binderT, signatureType, VarT n]
+      ForallT bndrs ctx type_ -> ForallT bndrs ctx (replaceScopeTermInType lscope type_)
+      ForallVisT bndrs type_ -> ForallVisT bndrs (replaceScopeTermInType lscope type_)
+      AppT f x -> AppT (replaceScopeTermInType lscope f) (replaceScopeTermInType lscope x)
+      AppKindT f k -> AppKindT (replaceScopeTermInType lscope f) k
+      SigT t k -> SigT (replaceScopeTermInType lscope t) k
+      t@ConT{} -> t
+      t@VarT{} -> t
+      t@PromotedT{} -> t
+      InfixT l op r -> InfixT (replaceScopeTermInType lscope l) op (replaceScopeTermInType lscope r)
+      UInfixT l op r -> UInfixT (replaceScopeTermInType lscope l) op (replaceScopeTermInType lscope r)
+      PromotedInfixT l op r -> PromotedInfixT (replaceScopeTermInType lscope l) op (replaceScopeTermInType lscope r)
+      PromotedUInfixT l op r -> PromotedUInfixT (replaceScopeTermInType lscope l) op (replaceScopeTermInType lscope r)
+      ParensT t -> ParensT (replaceScopeTermInType lscope t)
+      t@TupleT{} -> t
+      t@UnboxedTupleT{} -> t
+      t@UnboxedSumT{} -> t
+      t@ArrowT{} -> t
+      t@MulArrowT{} -> t
+      t@EqualityT{} -> t
+      t@ListT{} -> t
+      t@PromotedTupleT{} -> t
+      t@PromotedNilT{} -> t
+      t@PromotedConsT{} -> t
+      t@StarT{} -> t
+      t@ConstraintT{} -> t
+      t@LitT{} -> t
+      t@WildCardT{} -> t
+      ImplicitParamT s t -> ImplicitParamT s (replaceScopeTermInType lscope t)

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

@@ -89,9 +89,40 @@ mkSignature termT nameT scopeT patternT = do
           where
             k (x, y) = (name, x, y)
 
-        toSignatureParam (bang_, PeelConT typeName _typeParams)
+        toSignatureParam (_bang, PeelConT typeName _typeParams)
           | typeName == nameT = fail ("variable with other stuff in constructor: " ++ show con')
           | typeName == patternT = pure Nothing -- skip binders, they will be inserted automatically with each scoped term
-          | typeName == scopeT = pure (Just (bang_, VarT scope))
-          | typeName == termT = pure (Just (bang_, VarT term))
-        toSignatureParam bt = pure (Just bt)  -- everything else remains as is
+        toSignatureParam (bang_, type_) = pure (Just (bang_, replaceScopeTermInType type_))
+
+        replaceScopeTermInType = \case
+          PeelConT typeName _typeParams
+            | typeName == scopeT -> VarT scope
+            | typeName == termT -> VarT term
+          ForallT bndrs ctx type_ -> ForallT bndrs ctx (replaceScopeTermInType type_)
+          ForallVisT bndrs type_ -> ForallVisT bndrs (replaceScopeTermInType type_)
+          AppT f x -> AppT (replaceScopeTermInType f) (replaceScopeTermInType x)
+          AppKindT f k -> AppKindT (replaceScopeTermInType f) k
+          SigT t k -> SigT (replaceScopeTermInType t) k
+          t@ConT{} -> t
+          t@VarT{} -> t
+          t@PromotedT{} -> t
+          InfixT l op r -> InfixT (replaceScopeTermInType l) op (replaceScopeTermInType r)
+          UInfixT l op r -> UInfixT (replaceScopeTermInType l) op (replaceScopeTermInType r)
+          PromotedInfixT l op r -> PromotedInfixT (replaceScopeTermInType l) op (replaceScopeTermInType r)
+          PromotedUInfixT l op r -> PromotedUInfixT (replaceScopeTermInType l) op (replaceScopeTermInType r)
+          ParensT t -> ParensT (replaceScopeTermInType t)
+          t@TupleT{} -> t
+          t@UnboxedTupleT{} -> t
+          t@UnboxedSumT{} -> t
+          t@ArrowT{} -> t
+          t@MulArrowT{} -> t
+          t@EqualityT{} -> t
+          t@ListT{} -> t
+          t@PromotedTupleT{} -> t
+          t@PromotedNilT{} -> t
+          t@PromotedConsT{} -> t
+          t@StarT{} -> t
+          t@ConstraintT{} -> t
+          t@LitT{} -> t
+          t@WildCardT{} -> t
+          ImplicitParamT s t -> ImplicitParamT s (replaceScopeTermInType t)

haskell/lambda-pi/lambda-pi.cabal

@@ -1,6 +1,6 @@
 cabal-version: 1.24
 
--- This file has been generated from package.yaml by hpack version 0.36.0.
+-- This file has been generated from package.yaml by hpack version 0.37.0.
 --
 -- see: https://github.com/sol/hpack
 
@@ -61,6 +61,7 @@ library
     , containers
     , deepseq
     , free-foil >=0.1.0
+    , kind-generics-th
     , template-haskell
     , text >=1.2.3.1
   default-language: Haskell2010
@@ -84,6 +85,7 @@ executable lambda-pi
     , containers
     , deepseq
     , free-foil >=0.1.0
+    , kind-generics-th
     , lambda-pi
     , template-haskell
     , text >=1.2.3.1
@@ -109,6 +111,7 @@ test-suite doctests
     , deepseq
     , doctest-parallel
     , free-foil >=0.1.0
+    , kind-generics-th
     , lambda-pi
     , template-haskell
     , text >=1.2.3.1
@@ -139,6 +142,7 @@ test-suite spec
     , free-foil >=0.1.0
     , hspec
     , hspec-discover
+    , kind-generics-th
     , lambda-pi
     , mtl
     , template-haskell

haskell/lambda-pi/package.yaml

@@ -40,6 +40,7 @@ dependencies:
   template-haskell:
   deepseq:
   free-foil: ">= 0.1.0"
+  kind-generics-th:
 
 ghc-options:
   - -Wall