From 1bd181a6ece1aa52e29738aad88db96c256f723a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Samuel=20G=C3=A9lineau?= Date: Thu, 31 Oct 2024 00:27:05 -0400 Subject: [PATCH 1/2] SchemeVar newtype --- src/Expander.hs | 51 ++++++++++++++++++++++---------------- src/Expander/Monad.hs | 2 +- src/Expander/Primitives.hs | 5 ++-- src/Expander/TC.hs | 25 ++++++++++++------- src/Pretty.hs | 12 +++++---- src/Type.hs | 11 ++++++-- src/Util/Key.hs | 6 +++++ src/Util/Store.hs | 10 ++++++++ 8 files changed, 80 insertions(+), 42 deletions(-) diff --git a/src/Expander.hs b/src/Expander.hs index 6854f5b8..1b26a963 100644 --- a/src/Expander.hs +++ b/src/Expander.hs @@ -539,15 +539,17 @@ initializeKernel outputChannel = do | (name, fun) <- [("<", (<)), ("<=", (<=)), (">", (>)), (">=", (>=)), ("=", (==)), ("/=", (/=))] ] ++ [ ("pure-IO" - , Scheme [KStar, KStar] $ tFun [tSchemaVar 0 []] (tIO (tSchemaVar 0 [])) + , let a = tSchemaVar firstSchemeVar [] + in Scheme [KStar, KStar] $ tFun [a] (tIO a) , ValueClosure $ HO $ \v -> ValueIOAction (pure v) ) , ("bind-IO" - , Scheme [KStar, KStar] $ - tFun [ tIO (tSchemaVar 0 []) - , tFun [tSchemaVar 0 []] (tIO (tSchemaVar 1 [])) - ] - (tIO (tSchemaVar 1 [])) + , let a:b:_ = [tSchemaVar i [] | i <- [firstSchemeVar..]] + in Scheme [KStar, KStar] $ + tFun [ tIO a + , tFun [a] (tIO b) + ] + (tIO b) , ValueClosure $ HO $ \(ValueIOAction mx) -> do ValueClosure $ HO $ \(ValueClosure f) -> do ValueIOAction $ do @@ -587,22 +589,25 @@ initializeKernel outputChannel = do , ("Unit", [], [("unit", [])]) , ("Bool", [], [("true", []), ("false", [])]) , ("Problem", [], [("module", []), ("declaration", []), ("type", []), ("expression", [tType]), ("pattern", []), ("type-pattern", [])]) - , ("Maybe", [KStar], [("nothing", []), ("just", [tSchemaVar 0 []])]) - , ("List" - , [KStar] - , [ ("nil", []) - , ("::", [tSchemaVar 0 [], Prims.primitiveDatatype "List" [tSchemaVar 0 []]]) - ] - ) + , let a = tSchemaVar firstSchemeVar [] + in ("Maybe", [KStar], [("nothing", []), ("just", [a])]) + , let a = tSchemaVar firstSchemeVar [] + in ("List" + , [KStar] + , [ ("nil", []) + , ("::", [a, Prims.primitiveDatatype "List" [a]]) + ] + ) , ("Syntax-Contents" , [KStar] - , [ ("list-contents", [Prims.primitiveDatatype "List" [tSchemaVar 0 []]]) - , ("integer-contents", [tInteger]) - , ("string-contents", [tString]) - , ("identifier-contents", [tString]) - -- if you add a constructor here, remember to also add a - -- corresponding pattern in close-syntax! - ] + , let a = tSchemaVar firstSchemeVar [] + in [ ("list-contents", [Prims.primitiveDatatype "List" [a]]) + , ("integer-contents", [tInteger]) + , ("string-contents", [tString]) + , ("identifier-contents", [tString]) + -- if you add a constructor here, remember to also add a + -- corresponding pattern in close-syntax! + ] ) ] @@ -1220,8 +1225,9 @@ expandOneForm prob stx case prob of ExprDest t dest -> do argTys <- traverse makeTypeMeta argKinds + let tyStore = S.fromList $ zip [firstSchemeVar..] argTys unify dest t $ tDatatype dt argTys - args' <- for args \a -> inst dest (Scheme argKinds a) argTys + args' <- for args \a -> inst dest (Scheme argKinds a) tyStore Stx _ _ (foundName, foundArgs) <- mustBeCons stx _ <- mustBeIdent foundName argDests <- @@ -1234,8 +1240,9 @@ expandOneForm prob stx PatternDest patTy dest -> do Stx _ loc (_cname, subPats) <- mustBeCons stx tyArgs <- traverse makeTypeMeta argKinds + let tyStore = S.fromList $ zip [firstSchemeVar..] tyArgs argTypes <- for args \ a -> - inst loc (Scheme argKinds a) tyArgs + inst loc (Scheme argKinds a) tyStore unify loc (tDatatype dt tyArgs) patTy if length subPats /= length argTypes then throwError $ WrongArgCount stx ctor (length argTypes) (length subPats) diff --git a/src/Expander/Monad.hs b/src/Expander/Monad.hs index 62f7ce3c..67c442f6 100644 --- a/src/Expander/Monad.hs +++ b/src/Expander/Monad.hs @@ -241,7 +241,7 @@ data EValue | EPrimPatternMacro (Either (Ty, PatternPtr) TypePatternPtr -> Syntax -> Expand ()) | EPrimUniversalMacro (MacroDest -> Syntax -> Expand ()) | EVarMacro !Var -- ^ For bound variables (the Unique is the binding site of the var) - | ETypeVar !Kind !Natural + | ETypeVar !Kind !SchemeVar -- ^ For bound type variables (user-written Skolem variables or in datatype definitions) | EUserMacro !MacroVar -- ^ For user-written macros | EIncompleteMacro !MacroVar !Ident !SplitCorePtr -- ^ Macros that are themselves not yet ready to go diff --git a/src/Expander/Primitives.hs b/src/Expander/Primitives.hs index b8c5b8f8..08657ae9 100644 --- a/src/Expander/Primitives.hs +++ b/src/Expander/Primitives.hs @@ -68,7 +68,6 @@ import Control.Monad.Except import Data.Text (Text) import qualified Data.Text as T import Data.Traversable -import Numeric.Natural import Binding import Core @@ -130,7 +129,7 @@ datatype dest outScopesDest stx = do Stx scs loc (_ :: Syntax, more) <- mustBeCons stx Stx _ _ (nameAndArgs, ctorSpecs) <- mustBeCons (Syntax (Stx scs loc (List more))) Stx _ _ (name, args) <- mustBeCons nameAndArgs - typeArgs <- for (zip [0..] args) $ \(i, a) -> + typeArgs <- for (zip [firstSchemeVar..] args) $ \(i, a) -> prepareTypeVar i a sc <- freshScope $ T.pack $ "For datatype at " ++ shortShow (stxLoc stx) let typeScopes = map (view _1) typeArgs ++ [sc] @@ -712,7 +711,7 @@ scheduleTypePattern exprTy (Stx _ _ (patStx, rhsStx@(Syntax (Stx _ loc _)))) = d forkExpanderTask $ AwaitingTypePattern dest exprTy rhsDest rhsStx return (dest, rhsDest) -prepareTypeVar :: Natural -> Syntax -> Expand (Scope, Ident, Kind) +prepareTypeVar :: SchemeVar -> Syntax -> Expand (Scope, Ident, Kind) prepareTypeVar i varStx = do (sc, α, b) <- varPrepHelper varStx k <- KMetaVar <$> liftIO newKindVar diff --git a/src/Expander/TC.hs b/src/Expander/TC.hs index f6fdf1b7..540444d6 100644 --- a/src/Expander/TC.hs +++ b/src/Expander/TC.hs @@ -14,6 +14,7 @@ import Control.Monad import Control.Monad.Except import Control.Monad.State import Data.Foldable +import Data.Traversable (for) import Numeric.Natural import Expander.Monad @@ -107,12 +108,14 @@ freshMeta kind = do return ptr -inst :: UnificationErrorBlame blame => blame -> Scheme Ty -> [Ty] -> Expand Ty +inst :: UnificationErrorBlame blame => blame -> Scheme Ty -> Store SchemeVar Ty -> Expand Ty inst blame (Scheme argKinds ty) ts | length ts /= length argKinds = throwError $ InternalError "Mismatch in number of type vars" | otherwise = do - traverse_ (uncurry $ checkKind blame) (zip argKinds ts) + let tys :: [Ty] + tys = fmap snd $ St.toAscList ts + traverse_ (uncurry $ checkKind blame) (zip argKinds tys) instTy ty where instTy :: Ty -> Expand Ty @@ -131,13 +134,17 @@ inst blame (Scheme argKinds ty) ts pure $ TyF ctor' (tArgsPrefix ++ tArgsSuffix) instCtor :: TypeConstructor -> TyF Ty - instCtor (TSchemaVar i) = unTy $ ts !! fromIntegral i + instCtor (TSchemaVar v) = unTy $ ts St.! v instCtor ctor = TyF ctor [] specialize :: UnificationErrorBlame blame => blame -> Scheme Ty -> Expand Ty specialize blame sch@(Scheme argKinds _) = do - freshVars <- traverse makeTypeMeta argKinds + pairs <- for (zip [firstSchemeVar..] argKinds) $ \(v, k) -> do + meta <- makeTypeMeta k + pure (v, meta) + let freshVars :: Store SchemeVar Ty + freshVars = St.fromList pairs inst blame sch freshVars varType :: Var -> Expand (Maybe (Scheme Ty)) @@ -162,35 +169,35 @@ notFreeInCtx var = do generalizeType :: Ty -> Expand (Scheme Ty) generalizeType ty = do canGeneralize <- filterM notFreeInCtx =<< metas ty - (body, (_, _, argKinds)) <- flip runStateT (0, mempty, []) $ do + (body, (_, _, argKinds)) <- flip runStateT (firstSchemeVar, mempty, []) $ do genTyVars canGeneralize ty pure $ Scheme argKinds body where genTyVars :: [MetaPtr] -> Ty -> - StateT (Natural, Store MetaPtr Natural, [Kind]) Expand Ty + StateT (SchemeVar, Store MetaPtr SchemeVar, [Kind]) Expand Ty genTyVars vars t = do (Ty t') <- lift $ normType t Ty <$> genVarsTyF vars t' genVarsTyF :: [MetaPtr] -> TyF Ty -> - StateT (Natural, Store MetaPtr Natural, [Kind]) Expand (TyF Ty) + StateT (SchemeVar, Store MetaPtr SchemeVar, [Kind]) Expand (TyF Ty) genVarsTyF vars (TyF ctor args) = TyF <$> genVarsCtor vars ctor <*> traverse (genTyVars vars) args genVarsCtor :: [MetaPtr] -> TypeConstructor -> - StateT (Natural, Store MetaPtr Natural, [Kind]) Expand TypeConstructor + StateT (SchemeVar, Store MetaPtr SchemeVar, [Kind]) Expand TypeConstructor genVarsCtor vars (TMetaVar v) | v `elem` vars = do (i, indices, argKinds) <- get case St.lookup v indices of Nothing -> do k <- lift $ typeVarKind v - put (i + 1, St.insert v i indices, argKinds ++ [k]) + put (succ i, St.insert v i indices, argKinds ++ [k]) pure $ TSchemaVar i Just j -> pure $ TSchemaVar j | otherwise = pure $ TMetaVar v diff --git a/src/Pretty.hs b/src/Pretty.hs index 86b409bd..d55f35da 100644 --- a/src/Pretty.hs +++ b/src/Pretty.hs @@ -311,14 +311,14 @@ instance Pretty VarInfo (Scheme Ty) where text "∀" <> (align $ group $ vsep [ group $ - vsep (zipWith ppArgKind typeVarNames argKinds) <> text "." + vsep (zipWith ppArgKind schemeVarNames argKinds) <> text "." , pp env t ]) where ppArgKind varName kind = parens (text varName <+> text ":" <+> pp env kind) -typeVarNames :: [Text] -typeVarNames = +schemeVarNames :: [Text] +schemeVarNames = greek ++ [ base <> T.pack (show i) | (base, i) <- greekNum @@ -332,6 +332,8 @@ typeVarNames = , base <- greek ] +schemeVarName :: SchemeVar -> Text +schemeVarName (SchemeVar n) = schemeVarNames !! fromIntegral n instance Pretty VarInfo TypeConstructor where pp _ TSyntax = text "Syntax" @@ -343,7 +345,7 @@ instance Pretty VarInfo TypeConstructor where pp _ TIO = text "IO" pp _ TType = text "Type" pp env (TDatatype t) = pp env t - pp _ (TSchemaVar n) = text $ typeVarNames !! fromIntegral n + pp _ (TSchemaVar v) = text $ schemeVarName v pp _ (TMetaVar v) = text "META" <> viaShow v -- TODO instance Pretty VarInfo a => Pretty VarInfo (TyF a) where @@ -390,7 +392,7 @@ instance (Pretty VarInfo s, Pretty VarInfo t, PrettyBinder VarInfo a, Pretty Var (hang 2 $ group $ vsep ( text "data" <+> text x <+> hsep [ parens (text α <+> ":" <+> pp env k) - | α <- typeVarNames + | α <- schemeVarNames | k <- argKinds ] <+> text "=" diff --git a/src/Type.hs b/src/Type.hs index cc5d377f..5b4de6e7 100644 --- a/src/Type.hs +++ b/src/Type.hs @@ -36,6 +36,13 @@ newMetaPtr = MetaPtr <$> newUnique instance Show MetaPtr where show (MetaPtr i) = "(MetaPtr " ++ show (hashUnique i) ++ ")" +newtype SchemeVar = SchemeVar Natural + deriving newtype (Enum, Eq, HasKey, Ord, Show) + deriving stock Data + +firstSchemeVar :: SchemeVar +firstSchemeVar = SchemeVar 0 + data TypeConstructor = TSyntax | TInteger @@ -46,7 +53,7 @@ data TypeConstructor | TIO | TType | TDatatype Datatype - | TSchemaVar Natural + | TSchemaVar SchemeVar | TMetaVar MetaPtr deriving (Data, Eq, Show) makePrisms ''TypeConstructor @@ -115,7 +122,7 @@ class TyLike a arg | a -> arg where tIO :: arg -> a tType :: a tDatatype :: Datatype -> [arg] -> a - tSchemaVar :: Natural -> [arg] -> a + tSchemaVar :: SchemeVar -> [arg] -> a tMetaVar :: MetaPtr -> a instance TyLike (TyF a) a where diff --git a/src/Util/Key.hs b/src/Util/Key.hs index fba1b3d2..9f010887 100644 --- a/src/Util/Key.hs +++ b/src/Util/Key.hs @@ -4,6 +4,8 @@ module Util.Key (HasKey(..) ) where +import Numeric.Natural + class HasKey a where getKey :: a -> Int fromKey :: Int -> a @@ -11,3 +13,7 @@ class HasKey a where instance HasKey Int where getKey = id fromKey = id + +instance HasKey Natural where + getKey = fromIntegral + fromKey = fromIntegral \ No newline at end of file diff --git a/src/Util/Store.hs b/src/Util/Store.hs index 26960169..b505c3dd 100644 --- a/src/Util/Store.hs +++ b/src/Util/Store.hs @@ -15,9 +15,11 @@ module Util.Store ( lookup + , (!) , singleton , insert , toList + , toAscList , fromList , Store , unionWith @@ -70,6 +72,11 @@ instance (c ~ d) => Each (Store c a) (Store d b) a b where lookup :: HasKey p => p -> Store p v -> Maybe v lookup ptr graph = getKey ptr `IM.lookup` unStore graph +(!) :: HasKey p => Store p v -> p -> v +graph ! ptr = case lookup ptr graph of + Just v -> v + Nothing -> error "Store.!!: key not found" + singleton :: HasKey p => p -> v -> Store p v singleton ptr val = Store $! IM.singleton (getKey ptr) val @@ -79,6 +86,9 @@ insert k v str = Store $! IM.insert (getKey k) v (unStore str) toList :: HasKey p => Store p v -> [(p,v)] toList str = map (first fromKey) $ IM.toList (unStore str) +toAscList :: HasKey p => Store p v -> [(p,v)] +toAscList str = map (first fromKey) $ IM.toAscList (unStore str) + fromList :: HasKey p => [(p,v)] -> Store p v fromList ps = Store $! IM.fromList $ map (first getKey) ps From 0c741b9f063de50ebd740afece47d3a88256d891 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Samuel=20G=C3=A9lineau?= Date: Thu, 31 Oct 2024 23:34:41 -0400 Subject: [PATCH 2/2] pure-IO only has one scheme var pure-IO :: forall a. a -> IO a not pure-IO :: forall a b. a -> IO a Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> --- src/Expander.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Expander.hs b/src/Expander.hs index 1b26a963..f27b8ee1 100644 --- a/src/Expander.hs +++ b/src/Expander.hs @@ -540,7 +540,7 @@ initializeKernel outputChannel = do ] ++ [ ("pure-IO" , let a = tSchemaVar firstSchemeVar [] - in Scheme [KStar, KStar] $ tFun [a] (tIO a) + in Scheme [KStar] $ tFun [a] (tIO a) , ValueClosure $ HO $ \v -> ValueIOAction (pure v) ) , ("bind-IO"