From 917805a7cc32d295f11889b538c6a555bafdd939 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Mon, 28 Oct 2024 10:02:46 +0300 Subject: [PATCH] Add limited support for existentials in generic Sinkable --- .../src/Control/Monad/Foil/Internal.hs | 100 +++++++++++++++++- .../free-foil/src/Control/Monad/Free/Foil.hs | 6 +- .../soas/src/Language/SOAS/Impl/Generated.hs | 7 ++ 3 files changed, 103 insertions(+), 10 deletions(-) diff --git a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs index 1980b841..67d00905 100644 --- a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs +++ b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs @@ -966,21 +966,111 @@ type GSinkableExistsTypeError k f = ('Text "Generic Sinkable is not supported for existential data constructors" :$$: 'Text " when attempting to use a generic instance for" :$$: 'ShowType (Exists k f)) -instance GSinkableExistsTypeError k f => GSinkable (Exists k f) where - type GSinkableReqs (Exists k f) n l = GSinkableExistsTypeError k f +instance {-# OVERLAPPABLE #-} GSinkableExistsTypeError k f => GSinkable (Exists k f) where gsinkabilityProof = undefined +instance GSinkableExists f => GSinkable (Exists S f) where + type GSinkableReqs (Exists S f) n l = GSinkableExistsReqs f n l + gsinkabilityProof f (Exists e) = + gcosinkabilityExistsProof f id e $ \_f' e' -> + Exists e' + +class GSinkableExists f where + type GSinkableExistsReqs f (n :: S) (l :: S) :: Constraint + gcosinkabilityExistsProof + :: GSinkableExistsReqs f n l + => (Name n -> Name l) -> (Name i -> Name i') -> f (i :&&: n :&&: LoT0) + -> (forall i''. (Name i -> Name i'') -> f (i'' :&&: l :&&: LoT0) -> r) + -> r + +instance (GSinkableExists f, GSinkableExists g) => GSinkableExists (f :*: g) where + type GSinkableExistsReqs (f :*: g) n l + = (GSinkableExistsReqs f n l, GSinkableExistsReqs g n l) + gcosinkabilityExistsProof rename irename (x :*: y) cont = + gcosinkabilityExistsProof rename irename x $ \irename' x' -> + gcosinkabilityExistsProof rename irename' y $ \irename'' y' -> + cont irename'' (unsafeCoerce {- FIXME: sink? -} x' :*: y') + +instance (GSinkableExists f) => GSinkableExists (M1 i' c f) where + type GSinkableExistsReqs (M1 i' c f) n l = (GSinkableExistsReqs f n l) + gcosinkabilityExistsProof rename irename (M1 f) cont = + gcosinkabilityExistsProof rename irename f $ \irename' f' -> + cont irename' (M1 f') + +instance GSinkableExists (Field (Kon a)) where + type GSinkableExistsReqs (Field (Kon a)) n l = () + gcosinkabilityExistsProof _rename irename (Field x) cont = + cont irename (Field x) + +instance (Functor f, Sinkable g) => GSinkableExists (Field (Kon f :@: (Kon g :@: Var0))) where + type GSinkableExistsReqs (Field (Kon f :@: (Kon g :@: Var0))) n l = () + gcosinkabilityExistsProof _rename irename (Field x) cont = + cont irename (Field (fmap (sinkabilityProof irename) x)) +instance (Bifunctor f, Sinkable g, Sinkable g') => GSinkableExists (Field (Kon f :@: (Kon g :@: Var0) :@: (Kon g' :@: Var0))) where + type GSinkableExistsReqs (Field (Kon f :@: (Kon g :@: Var0) :@: (Kon g' :@: Var0))) n l = () + gcosinkabilityExistsProof _rename irename (Field x) cont = + cont irename (Field (bimap (sinkabilityProof irename) (sinkabilityProof irename) x)) +-- FIXME: this instance is too specific, need better generic decomposition +instance (Functor f, Bifunctor f', Sinkable g, Sinkable g') => GSinkableExists (Field (Kon f :@: (Kon f' :@: (Kon g :@: Var0) :@: (Kon g' :@: Var0)))) where + type GSinkableExistsReqs (Field (Kon f :@: (Kon f' :@: (Kon g :@: Var0) :@: (Kon g' :@: Var0)))) n l = () + gcosinkabilityExistsProof _rename irename (Field x) cont = + cont irename (Field (fmap (bimap (sinkabilityProof irename) (sinkabilityProof irename)) x)) + +instance Sinkable f => GSinkableExists (Field (Kon f :@: Var0)) where + type GSinkableExistsReqs (Field (Kon f :@: Var0)) n l = () + gcosinkabilityExistsProof _rename irename (Field x) cont = + cont irename (Field (sinkabilityProof irename x)) + +instance Sinkable f => GSinkableExists (Field (Kon f :@: Var1)) where + type GSinkableExistsReqs (Field (Kon f :@: Var1)) n l = () + gcosinkabilityExistsProof rename irename (Field x) cont = + cont irename (Field (sinkabilityProof rename x)) + +instance Sinkable (f a) => GSinkableExists (Field (Kon f :@: Kon a :@: Var0)) where + type GSinkableExistsReqs (Field (Kon f :@: Kon a :@: Var0)) n l = () + gcosinkabilityExistsProof _rename irename (Field x) cont = + cont irename (Field (sinkabilityProof irename x)) + +instance Sinkable (f a) => GSinkableExists (Field (Kon f :@: Kon a :@: Var1)) where + type GSinkableExistsReqs (Field (Kon f :@: Kon a :@: Var1)) n l = () + gcosinkabilityExistsProof rename irename (Field x) cont = + cont irename (Field (sinkabilityProof rename x)) + +instance Sinkable (f a b) => GSinkableExists (Field (Kon f :@: Kon a :@: Kon b :@: Var0)) where + type GSinkableExistsReqs (Field (Kon f :@: Kon a :@: Kon b :@: Var0)) n l = () + gcosinkabilityExistsProof _rename irename (Field x) cont = + cont irename (Field (sinkabilityProof irename x)) + +instance Sinkable (f a b) => GSinkableExists (Field (Kon f :@: Kon a :@: Kon b :@: Var1)) where + type GSinkableExistsReqs (Field (Kon f :@: Kon a :@: Kon b :@: Var1)) n l = () + gcosinkabilityExistsProof rename irename (Field x) cont = + cont irename (Field (sinkabilityProof rename x)) + +instance CoSinkable f => GSinkableExists (Field (Kon f :@: Var1 :@: Var0)) where + type GSinkableExistsReqs (Field (Kon f :@: Var1 :@: Var0)) n l = () + gcosinkabilityExistsProof rename _irename (Field x) cont = + coSinkabilityProof rename x $ \rename' x' -> + cont rename' (Field x') + class GSinkableField f where type GSinkableFieldReqs f (n :: S) (l :: S) :: Constraint gsinkabilityProofField :: GSinkableFieldReqs f n l => (Name n -> Name l) -> Field f (n :&&: LoT0) -> Field f (l :&&: LoT0) +instance GSinkableField (Kon a) where + type GSinkableFieldReqs (Kon a) n l = () + gsinkabilityProofField _f (Field x) = Field x + +instance GSinkableField (Kon a :@: Kon b) where + type GSinkableFieldReqs (Kon a :@: Kon b) n l = () + gsinkabilityProofField _f (Field x) = Field x + instance GSinkableField (f :@: Var0) where type GSinkableFieldReqs (f :@: Var0) n l = (Sinkable (Interpret f (n :&&: LoT0)), Interpret f (n :&&: LoT0) ~ Interpret f (l :&&: LoT0)) gsinkabilityProofField f (Field x) = Field (sinkabilityProof f x) -instance (Functor f, GSinkableField x) => GSinkableField (Kon f :@: x) where - type GSinkableFieldReqs (Kon f :@: x) n l = GSinkableFieldReqs x n l - gsinkabilityProofField f (Field x) = Field (fmap (unField . gsinkabilityProofField @x f . Field) x) +instance (Functor f, GSinkableField (x :@: Var0)) => GSinkableField (Kon f :@: (x :@: Var0)) where + type GSinkableFieldReqs (Kon f :@: (x :@: Var0)) n l = GSinkableFieldReqs (x :@: Var0) n l + gsinkabilityProofField f (Field x) = Field (fmap (unField . gsinkabilityProofField @(x :@: Var0) f . Field) x) instance (GSinkableField x, GSinkableField y) => GSinkableField (f :@: x :@: y) where type GSinkableFieldReqs (f :@: x :@: y) n l = diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil.hs b/haskell/free-foil/src/Control/Monad/Free/Foil.hs index 5c017ef8..f43cd8a4 100644 --- a/haskell/free-foil/src/Control/Monad/Free/Foil.hs +++ b/haskell/free-foil/src/Control/Monad/Free/Foil.hs @@ -69,11 +69,7 @@ instance GenericK (AST binder sig) where :$: (Kon ScopedAST :@: Kon binder :@: Kon sig :@: Var0) :@: (Kon AST :@: Kon binder :@: Kon sig :@: Var0)) -instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.Sinkable (ScopedAST binder sig) where - sinkabilityProof rename (ScopedAST binder body) = - Foil.extendRenaming rename binder $ \rename' binder' -> - ScopedAST binder' (Foil.sinkabilityProof rename' body) - +instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.Sinkable (ScopedAST binder sig) instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.Sinkable (AST binder sig) instance Foil.InjectName (AST binder sig) where diff --git a/haskell/soas/src/Language/SOAS/Impl/Generated.hs b/haskell/soas/src/Language/SOAS/Impl/Generated.hs index 6385487c..e3cd18be 100644 --- a/haskell/soas/src/Language/SOAS/Impl/Generated.hs +++ b/haskell/soas/src/Language/SOAS/Impl/Generated.hs @@ -44,6 +44,9 @@ deriveGenericK ''OpArg'Sig deriveGenericK ''Term'Sig deriveGenericK ''OpArgTyping'Sig deriveGenericK ''Type'Sig +deriveGenericK ''Subst' +deriveGenericK ''Constraint' +deriveGenericK ''OpTyping' deriveBifunctor ''OpArg'Sig deriveBifunctor ''Term'Sig @@ -51,6 +54,10 @@ deriveBifunctor ''OpArgTyping'Sig deriveBifunctor ''ScopedOpArgTyping'Sig deriveBifunctor ''Type'Sig +instance Foil.Sinkable (Subst' a) +instance Foil.Sinkable (Constraint' a) +instance Foil.Sinkable (OpTyping' a) + -- FIXME: derive via GenericK instance Foil.CoSinkable (Binders' a) where coSinkabilityProof rename (NoBinders loc) cont = cont rename (NoBinders loc)