From a14ee939bf06e9426367f5c288910c8ec207248d Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Tue, 29 Oct 2024 21:41:21 +0300 Subject: [PATCH] Implement a separate generic check to ensure valid binders/patterns --- haskell/free-foil/free-foil.cabal | 1 + .../src/Control/Monad/Foil/Internal.hs | 19 +- .../Monad/Foil/Internal/ValidNameBinders.hs | 178 ++++++++++++++++++ 3 files changed, 189 insertions(+), 9 deletions(-) create mode 100644 haskell/free-foil/src/Control/Monad/Foil/Internal/ValidNameBinders.hs diff --git a/haskell/free-foil/free-foil.cabal b/haskell/free-foil/free-foil.cabal index 41748029..e9f83e8a 100644 --- a/haskell/free-foil/free-foil.cabal +++ b/haskell/free-foil/free-foil.cabal @@ -31,6 +31,7 @@ library Control.Monad.Foil Control.Monad.Foil.Example Control.Monad.Foil.Internal + Control.Monad.Foil.Internal.ValidNameBinders Control.Monad.Foil.Relative Control.Monad.Foil.TH Control.Monad.Foil.TH.MkFoilData diff --git a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs index a818fcc4..0b215191 100644 --- a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs +++ b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs @@ -56,6 +56,8 @@ import qualified Data.Type.Equality as Type import Generics.Kind import Unsafe.Coerce +import Control.Monad.Foil.Internal.ValidNameBinders + -- * Safe types and operations -- | 'S' is a data kind of scope indices. @@ -731,7 +733,7 @@ class CoSinkable (pattern :: S -> S -> Type) where -- ^ Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern. -> r default withPattern - :: (Distinct o, GenericK pattern, GHasNameBinders (RepK pattern)) + :: (Distinct o, GenericK pattern, GValidNameBinders pattern (RepK pattern), GHasNameBinders (RepK pattern)) => (forall x y z r'. Distinct z => Scope z -> NameBinder x y -> (forall z'. DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall x z z'. DExt z z' => f x x z z') -> (forall x y y' z z' z''. (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') @@ -1122,7 +1124,7 @@ instance (Bifunctor f, GSinkableK (Field x), GSinkableK (Field y)) => GSinkableK -- This can be used as a default implementation of 'withPattern'. gunsafeWithPatternViaHasNameBinders :: forall pattern f o n l r. - (Distinct o, GenericK pattern, GHasNameBinders (RepK pattern)) + (Distinct o, GenericK pattern, GValidNameBinders pattern (RepK pattern), GHasNameBinders (RepK pattern)) => (forall x y z r'. Distinct z => Scope z -> NameBinder x y -> (forall z'. DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -- ^ Processing of a single 'NameBinder', this will be applied to each binder in a pattern. -> (forall x z z'. DExt z z' => f x x z z') @@ -1141,7 +1143,6 @@ gunsafeWithPatternViaHasNameBinders withBinder id_ comp_ scope pat cont = cont result (gunsafeSetNameBinders (unsafeCoerce pat) binders) -- FIXME: safer version -- ** Manipulating nested 'NameBinder's - -- | If @'HasNameBinders' f@, then @f n l@ is expected to act as a binder, -- introducing into scope @n@ some local variables, extending it to scope @l@. -- This class allows to extract and modify the set of binders. @@ -1174,7 +1175,7 @@ class HasNameBinders f where -- -- You should never use this. This is only used for generic implementation of 'HasNameBinders'. reallyUnsafeSetNameBindersRaw :: f n l -> [RawName] -> (f n l', [RawName]) - default reallyUnsafeSetNameBindersRaw :: forall n l l'. (GenericK f, GHasNameBinders (RepK f)) => f n l -> [RawName] -> (f n l', [RawName]) + default reallyUnsafeSetNameBindersRaw :: forall n l l'. (GenericK f, GValidNameBinders f (RepK f), GHasNameBinders (RepK f)) => f n l -> [RawName] -> (f n l', [RawName]) reallyUnsafeSetNameBindersRaw e names = let (e', names') = greallyUnsafeSetNameBindersRaw (fromK @_ @f @(n :&&: l :&&: LoT0) e) names in (toK @_ @f @(n :&&: l' :&&: LoT0) e', names') @@ -1185,12 +1186,12 @@ instance HasNameBinders NameBinder where instance HasNameBinders NameBinderList --- ** Generic (and slightly unsafe) +-- ** Generic ggetNameBinders :: forall f n l. (GenericK f, GHasNameBinders (RepK f)) => f n l -> NameBinders n l ggetNameBinders = UnsafeNameBinders . IntSet.fromList . ggetNameBindersRaw . fromK @_ @f @(n :&&: l :&&: LoT0) -gunsafeSetNameBinders :: forall f n l l'. (GenericK f, GHasNameBinders (RepK f)) => f n l -> NameBinders n l' -> f n l' +gunsafeSetNameBinders :: forall f n l l'. (GenericK f, GValidNameBinders f (RepK f), GHasNameBinders (RepK f)) => f n l -> NameBinders n l' -> f n l' gunsafeSetNameBinders e (UnsafeNameBinders m) = toK @_ @f @(n :&&: l' :&&: LoT0) $ fst (greallyUnsafeSetNameBindersRaw (fromK @_ @f @(n :&&: l :&&: LoT0) e) (IntSet.toList m)) @@ -1239,13 +1240,13 @@ instance GHasNameBinders f => GHasNameBinders (M1 i c f) where let (x', names') = greallyUnsafeSetNameBindersRaw x names in (M1 x', names') -instance GHasNameBinders f => GHasNameBinders (a :~~: b :=>: f) where +instance GHasNameBinders f => GHasNameBinders (Var i :~~: Var j :=>: f) where ggetNameBindersRaw (SuchThat x) = ggetNameBindersRaw x - greallyUnsafeSetNameBindersRaw :: forall as bs. (a :~~: b :=>: f) as -> [RawName] -> ((a :~~: b :=>: f) bs, [RawName]) + greallyUnsafeSetNameBindersRaw :: forall as bs. (Var i :~~: Var j :=>: f) as -> [RawName] -> ((Var i :~~: Var j :=>: f) bs, [RawName]) greallyUnsafeSetNameBindersRaw (SuchThat x) names = -- this is sort of safe... - case unsafeCoerce (Type.Refl :: Interpret a bs Type.:~: Interpret a bs) :: Interpret a bs Type.:~: Interpret b bs of + case unsafeCoerce (Type.Refl :: Interpret (Var i) bs Type.:~: Interpret (Var i) bs) :: Interpret (Var i) bs Type.:~: Interpret (Var j) bs of Type.Refl -> let (x', names') = greallyUnsafeSetNameBindersRaw x names in (SuchThat x', names') diff --git a/haskell/free-foil/src/Control/Monad/Foil/Internal/ValidNameBinders.hs b/haskell/free-foil/src/Control/Monad/Foil/Internal/ValidNameBinders.hs new file mode 100644 index 00000000..8b31ed62 --- /dev/null +++ b/haskell/free-foil/src/Control/Monad/Foil/Internal/ValidNameBinders.hs @@ -0,0 +1,178 @@ +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} +module Control.Monad.Foil.Internal.ValidNameBinders where + +import Data.Kind (Type, Constraint) +import GHC.TypeError +import GHC.TypeLits +import Generics.Kind +import qualified GHC.Generics as GHC + +type SubstInRepK :: TyVar d k -> Atom d k -> (LoT d -> Type) -> LoT d -> Type +type family SubstInRepK i atom f where + SubstInRepK i atom V1 = V1 + SubstInRepK i atom U1 = U1 + SubstInRepK i atom (M1 info c f) = M1 info c (SubstInRepK i atom f) + SubstInRepK i atom (Field field) = Field (SubstInAtom i atom field) + SubstInRepK i atom f = + TypeError + ('Text "cannot substitute variable" + :$$: 'Text " " :<>: 'ShowType (Var i) + :$$: 'Text "with atom" + :$$: 'Text " " :<>: 'ShowType atom + :$$: 'Text "in" + :$$: 'Text " " :<>: 'ShowType f) + +type SubstInAtom :: TyVar d k -> Atom d k -> Atom d k1 -> Atom d k1 +type family SubstInAtom i atom f where + SubstInAtom i atom (Var i) = atom + SubstInAtom i atom (Var j) = Var j + SubstInAtom i atom (Kon a) = Kon a + SubstInAtom i atom (f :@: x) = SubstInAtom i atom f :@: SubstInAtom i atom x + -- SubstInAtom i atom atom' = atom' + SubstInAtom i atom atom' = + TypeError + ('Text "cannot substitute variable" + :$$: 'Text " " :<>: 'ShowType (Var i) + :$$: 'Text "with atom" + :$$: 'Text " " :<>: 'ShowType atom + :$$: 'Text "in an atom" + :$$: 'Text " " :<>: 'ShowType atom') + +type ShowKindedScope oo n ll = ShowScope oo n ll :<>: 'Text " : S" + +type ShowScope :: Atom d s -> Atom d s -> Atom d s -> ErrorMessage +type family ShowScope oo n ll where + ShowScope oo ll ll = 'Text "innerScope" + ShowScope oo oo ll = 'Text "outerScope" + ShowScope oo n ll = ShowScopeN 1 n + +type ShowScopeN :: Natural -> Atom d s -> ErrorMessage +type family ShowScopeN i n where + ShowScopeN i (Var VZ) = 'Text "scope" :<>: 'ShowType i + ShowScopeN i (Var (VS x)) = ShowScopeN (i + 1) (Var x) + +type ShowSaturatedPatternType pattern oo n l ll = + 'ShowType pattern :<>: 'Text " " :<>: ShowScope oo n ll :<>: 'Text " " :<>: ShowScope oo l ll + +type GInnerScopeOfAtom :: ErrorMessage -> Nat -> Nat -> (s -> s -> Type) -> Atom d Type -> Atom d s -> Atom d s -> Atom d s -> Atom d s +type family GInnerScopeOfAtom msg icon ifield pattern atom oo n ll where + GInnerScopeOfAtom msg icon ifield pattern (Kon a) oo n ll = n + GInnerScopeOfAtom msg icon ifield pattern (Kon f :@: n :@: l) oo n ll = l + GInnerScopeOfAtom msg icon ifield pattern (Kon f :@: o :@: i) oo n ll = + TypeError + ('Text "Unexpected Foil scope extension in the binder/pattern" + :$$: 'Text " " :<>: ShowSaturatedPatternType f oo o i ll + :$$: 'Text "the binder/pattern tries to extend scope" + :$$: 'Text " " :<>: ShowKindedScope oo o ll + :$$: 'Text "to scope" + :$$: 'Text " " :<>: ShowKindedScope oo i ll + :$$: 'Text "but it is expected to extend the current (outer) scope" + :$$: 'Text " " :<>: ShowKindedScope oo n ll + :$$: ShowLocalizeError msg icon ifield pattern oo ll + ) + GInnerScopeOfAtom msg icon ifield pattern atom oo n ll = + TypeError + ('Text "the following atom does not seem to be a valid part of a pattern/binder" + :$$: 'Text " " :<>: 'ShowType atom + :$$: ShowLocalizeError msg icon ifield pattern oo ll) + +type SameInnerScope :: ErrorMessage -> Nat -> (s -> s -> Type) -> Atom k s -> Atom k s -> Atom k s +type family SameInnerScope msg icon pattern n l where + SameInnerScope msg icon pattern l l = l + SameInnerScope msg icon pattern n l = + TypeError + ('Text "Unexpected extended (inner) Foil scope in the data type" + :$$: 'Text " " :<>: ShowSaturatedPatternType pattern n n l l + :$$: 'Text "expecting extended (inner) scope to be" + :$$: 'Text " " :<>: ShowKindedScope n l l + :$$: 'Text "but the inferred extended (inner) scope is" + :$$: 'Text " " :<>: ShowKindedScope n n l + :$$: ShowLocalizeError msg icon 0 pattern n l + ) + +type GValidNameBinders :: (s -> s -> Type) -> (LoT (s -> s -> Type) -> Type) -> Constraint +type family GValidNameBinders pattern f :: Constraint where + GValidNameBinders pattern (f :: LoT (s -> s -> Type) -> Type) = + (GInnerScopeOfRepK ('Text "") 0 0 pattern f Var0 Var0 Var1) + ~ (Var1 :: Atom (s -> s -> Type) s) + +type AtomSucc :: Atom d k1 -> Atom (k -> d) k1 +type family AtomSucc atom where + AtomSucc (Var i) = Var (VS i) + +type AtomUnSucc :: ErrorMessage -> Nat -> (s -> s -> Type) -> Atom d s -> Atom d s -> Atom (k -> d) k1 -> Atom d k1 +type family AtomUnSucc msg icon pattern oo ll atom where + AtomUnSucc msg icon pattern oo ll (Var (VS i)) = Var i + AtomUnSucc msg icon pattern oo ll (Var VZ) = TypeError + ('Text "Intermediate scope escapes existential quantification for data type" + :$$: ShowLocalizeError msg icon 0 pattern oo ll + ) + +type family First x y where + First (Var x) (Var y) = Var x + +type family AndShowFieldNumber ifield msg where + AndShowFieldNumber 0 msg = msg + AndShowFieldNumber n msg = + 'Text "when checking field number " :<>: 'ShowType n + :$$: msg + +type family AndShowConNumber icon msg where + AndShowConNumber 0 msg = msg + AndShowConNumber n msg = + 'Text "when checking constructor number " :<>: 'ShowType n + :$$: msg + +type AndShowDataType pattern n l msg = + 'Text "when tracking Foil scopes for the data type" + :$$: 'Text " " :<>: ShowSaturatedPatternType pattern n n l l + :$$: msg + +type ShowLocalizeError msg icon ifield pattern o l = + AndShowFieldNumber ifield + (AndShowConNumber icon + (AndShowDataType pattern o l + msg)) + +type family CountCons f where + CountCons (f :+: g) = CountCons f + CountCons g + CountCons (M1 GHC.C c f) = 1 + +type family CountFields f where + CountFields (f :*: g) = CountFields f + CountFields g + CountFields (M1 GHC.S c f) = 1 + +type GInnerScopeOfRepK :: ErrorMessage -> Nat -> Nat -> (s -> s -> Type) -> (LoT k -> Type) -> Atom k s -> Atom k s -> Atom k s -> Atom k s +type family GInnerScopeOfRepK msg icon ifield pattern f o n l where + GInnerScopeOfRepK msg icon ifield pattern V1 o n l = l + GInnerScopeOfRepK msg icon ifield pattern U1 o n l = n + GInnerScopeOfRepK msg icon ifield pattern (M1 GHC.C c f) o n l = + GInnerScopeOfRepK msg icon 1 pattern f o n l + GInnerScopeOfRepK msg icon ifield pattern (M1 GHC.D c f) o n l = + GInnerScopeOfRepK msg 1 ifield pattern f o n l + GInnerScopeOfRepK msg icon ifield pattern (M1 i c f) o n l = + GInnerScopeOfRepK msg icon ifield pattern f o n l + GInnerScopeOfRepK msg icon ifield pattern (f :+: g) o n l = First + (SameInnerScope msg icon pattern (GInnerScopeOfRepK msg icon ifield pattern f o n l) l) + (SameInnerScope msg icon pattern (GInnerScopeOfRepK msg (icon + CountCons f) ifield pattern g o n l) l) + GInnerScopeOfRepK msg icon ifield pattern (f :*: g) o n l = + GInnerScopeOfRepK msg icon (ifield + CountFields f) pattern g o + (GInnerScopeOfRepK msg icon ifield pattern f o n l) l + GInnerScopeOfRepK msg icon ifield pattern (Var i :~~: Var j :=>: f) o n l = + GInnerScopeOfRepK msg icon ifield pattern (SubstInRepK i (Var j) f) + (SubstInAtom i (Var j) o) (SubstInAtom i (Var j) n) (SubstInAtom i (Var j) l) + GInnerScopeOfRepK msg icon ifield pattern (Exists k f) o n l = + AtomUnSucc msg icon pattern o l + (GInnerScopeOfRepK msg icon ifield pattern f (AtomSucc o) (AtomSucc n) (AtomSucc l)) + GInnerScopeOfRepK msg icon ifield pattern (Field atom) o n l = GInnerScopeOfAtom msg icon ifield pattern atom o n l + GInnerScopeOfRepK msg icon ifield pattern f o n l = + TypeError + ('Text "Unsupported structure in a binder/pattern" + :$$: 'Text " " :<>: 'ShowType f + :$$: ShowLocalizeError msg icon 0 pattern n l)