From 00e085135c21faafcb6a6f5e7a21a9935466dff9 Mon Sep 17 00:00:00 2001 From: crumbtoo Date: Tue, 27 Feb 2024 14:48:02 -0700 Subject: [PATCH] almost done --- src/Core/Parse.y | 3 +- src/Core/Syntax.hs | 39 ++++++--- src/Core/SystemF.hs | 189 ++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 218 insertions(+), 13 deletions(-) diff --git a/src/Core/Parse.y b/src/Core/Parse.y index d6aecf8..71d0879 100644 --- a/src/Core/Parse.y +++ b/src/Core/Parse.y @@ -128,7 +128,8 @@ TypeApp :: { Type } Type1 :: { Type } Type1 : '(' Type ')' { $2 } | varname { TyVar $1 } - | conname { TyCon $1 } + | conname { if $1 == "Type" + then TyKindType else TyCon $1 } ParList :: { [Name] } ParList : varname ParList { $1 : $2 } diff --git a/src/Core/Syntax.hs b/src/Core/Syntax.hs index 59bec87..56bf9f4 100644 --- a/src/Core/Syntax.hs +++ b/src/Core/Syntax.hs @@ -16,13 +16,13 @@ module Core.Syntax , ScDef(..), ScDef' , Program(..), Program' , Type(..), Kind, pattern (:->), pattern TyInt - , Alter(..), Alter', AltCon(..) + , AlterF(..), Alter(..), Alter', AltCon(..) , pattern Binding, pattern Alter , Rec(..), Lit(..) , Pragma(..) -- ** Variables and identifiers - , Name, Var(..), Tag - , Binding(..), pattern (:=), pattern (:$) + , Name, Var(..), Tag, pattern (:^) + , Binding, BindingF(..), pattern (:=), pattern (:$) , type Binding' -- ** Working with the fixed point of ExprF , Expr, Expr' @@ -36,7 +36,7 @@ module Core.Syntax , programScDefs, programTypeSigs, programDataTags , formalising , HasRHS(_rhs), HasLHS(_lhs) - , applicants + , _BindingF, _MkVar -- ** Classy optics , HasBinders(..), HasArrowStops(..) ) @@ -110,6 +110,9 @@ type Kind = Type data Var = MkVar Name Type deriving (Eq, Show, Lift) +pattern (:^) :: Name -> Type -> Var +pattern n :^ t = MkVar n t + instance Hashable Var where hashWithSalt s (MkVar n _) = hashWithSalt s n @@ -284,14 +287,16 @@ formalising :: Iso (Expr a) (Expr b) (Expr a) (Expr b) formalising = iso sa bt where sa :: Expr a -> Expr a sa = ana \case - Lam [b] e -> LamF [b] e - Lam (b:bs) e -> LamF [b] (Lam bs e) - x -> project x + Lam [b] e -> LamF [b] e + Lam (b:bs) e -> LamF [b] (Lam bs e) + Let r (b:bs) e -> LetF r [b] (Let r bs e) + x -> project x bt :: Expr b -> Expr b bt = cata \case - LamF [b] (Lam bs e) -> Lam (b:bs) e - x -> embed x + LamF [b] (Lam bs e) -> Lam (b:bs) e + LetF r [b] (Let r' bs e) | r == r' -> Let r (b:bs) e + x -> embed x -------------------------------------------------------------------------------- @@ -386,6 +391,9 @@ instance Pretty Type where hsep [prettyPrec appPrec a, "->", prettyPrec (appPrec-1) b] prettyPrec p (TyApp f x) = maybeParens (p>appPrec) $ prettyPrec appPrec f <+> prettyPrec appPrec1 x + prettyPrec p (TyForall a m) = maybeParens (p>appPrec-2) $ + "∀" <+> (prettyPrec appPrec1 a <> ".") <+> pretty m + prettyPrec _ TyKindType = "Type" instance (Pretty b, Pretty (AsTerse b), MakeTerse b) => Pretty (WithTerseBinds (ScDef b)) where @@ -569,6 +577,9 @@ deriving instance Lift b => Lift (Program b) -------------------------------------------------------------------------------- +-- class HasApplicants s t a b | s -> a, t -> b, s b -> t, t a -> s where +-- applicants :: Traversal s t a b + -- instance HasApplicants (ExprF b (Fix (ExprF b))) (ExprF b (Fix (ExprF b))) -- (Fix (ExprF b)) (Fix (ExprF b)) where -- applicants k (AppF f x) = AppF <$> applicants k f <*> k x @@ -580,9 +591,9 @@ deriving instance Lift b => Lift (Program b) -- => LensLike' g (Fix f) (Fix f) -- applicants k (Fix f) = Fix <$> applicants k f -applicants :: Traversal' (Expr b) (Expr b) -applicants k (App f x) = App <$> applicants k f <*> k x -applicants k x = k x +-- applicants :: Traversal' (Expr b) (Expr b) +-- applicants k (App f x) = App <$> applicants k f <*> k x +-- applicants k x = k x class HasBinders s t a b | s -> a, t -> b, s b -> t, t a -> s where binders :: Traversal s t a b @@ -635,6 +646,7 @@ class HasArrowStops s t a b | s -> a, t -> b, s b -> t, t a -> s where instance HasArrowStops Type Type Type Type where arrowStops k (s :-> t) = (:->) <$> k s <*> arrowStops k t + arrowStops k t = k t -------------------------------------------------------------------------------- @@ -667,3 +679,6 @@ deriveEq1 ''ExprF deriving instance (Eq b, Eq a) => Eq (ExprF b a) +makePrisms ''BindingF +makePrisms ''Var + diff --git a/src/Core/SystemF.hs b/src/Core/SystemF.hs index b375fc7..5b79fca 100644 --- a/src/Core/SystemF.hs +++ b/src/Core/SystemF.hs @@ -1,15 +1,204 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE OverloadedLists #-} module Core.SystemF ( lintCoreProgR ) where -------------------------------------------------------------------------------- +import GHC.Generics (Generic, Generically(..)) +import Data.HashMap.Strict (HashMap) +import Data.HashMap.Strict qualified as H +import Data.Function (on) +import Data.Traversable +import Data.Foldable +import Data.List.Extra +import Control.Monad.Utils +import Control.Monad + +import Control.Comonad +import Control.Comonad.Cofree +import Data.Fix +import Data.Functor + +import Control.Lens hiding ((:<)) +import Control.Lens.Unsound + import Compiler.RLPC import Core -------------------------------------------------------------------------------- +data Gamma = Gamma + { _gammaVars :: HashMap Name Type + , _gammaTyVars :: HashMap Name Kind + , _gammaTyCons :: HashMap Name Kind + } + deriving (Generic) + deriving (Semigroup, Monoid) + via (Generically Gamma) + +makeLenses ''Gamma + lintCoreProgR :: (Monad m) => Program Var -> RLPCT m (Program Name) lintCoreProgR = undefined lint :: Program Var -> Program Name lint = undefined +type ET = Cofree (ExprF Var) Type + +type SysF = Either TypeError + +data TypeError = TypeErrorUndefinedVariable Name + | TypeErrorKindMismatch Kind Kind + | TypeErrorCouldNotMatch Type Type + deriving Show + +lintE :: Gamma -> Expr Var -> SysF ET +lintE g = \case + Var n -> lookupVar g n <&> (:< VarF n) + Lit (IntL n) -> pure $ TyInt :< LitF (IntL n) + + Type t -> kindOf g t <&> (:< TypeF t) + + App f x + -- type application + | Right (TyForall (a :^ k) m :< f') <- lintE g f + , Right (k' :< TypeF t) <- lintE g x + , k == k' + -> pure $ subst a t m :< f' + + -- value application + | Right fw@((s :-> t) :< _) <- lintE g f + , Right xw@(s' :< _) <- lintE g x + , s == s' + -> pure $ t :< AppF fw xw + + Lam bs e -> do + e'@(t :< _) <- lintE g' e + pure $ foldr arrowify t bs :< LamF bs e' + where + g' = foldMap suppl bs <> g + + suppl (MkVar n t) + | isKind t = mempty & gammaTyVars %~ H.insert n t + | otherwise = mempty & gammaVars %~ H.insert n t + + arrowify (MkVar n s) s' + | isKind s = TyForall (n :^ s) s' + | otherwise = s :-> s' + + Let Rec bs e -> do + e'@(t :< _) <- lintE g' e + bs' <- (uncurry checkBind . (_2 %~ wrapFix)) `traverse` binds + pure $ t :< LetF Rec bs' e' + where + binds = bs ^.. each . _BindingF + vs = binds ^.. each . _1 . _MkVar + g' = supplementVars vs g + checkBind v@(MkVar n t) e = case lintE g' e of + Right (t' :< e') | t == t' -> Right (BindingF v e') + | otherwise -> Left (TypeErrorCouldNotMatch t t') + Left e -> Left e + Let NonRec bs e -> do + (g',bs') <- mapAccumLM checkBind g bs + e'@(t :< _) <- lintE g' e + pure $ t :< LetF NonRec bs' e' + where + checkBind :: Gamma -> BindingF Var (Expr Var) + -> SysF (Gamma, BindingF Var ET) + checkBind g (BindingF v@(n :^ t) e) = case lintE g (wrapFix e) of + Right (t' :< e') + | t == t' -> Right (supplementVar n t g, BindingF v e') + | otherwise -> Left (TypeErrorCouldNotMatch t t') + Left e -> Left e + + Case e as -> do + (ts,as') <- unzip <$> checkAlt `traverse` as + unless (allSame ts) $ + Left (error "unifica oh my god fix this later") + e' <- lintE g e + pure $ head ts :< CaseF e' as' + where + checkAlt :: Alter Var -> SysF (Type, AlterF Var ET) + checkAlt (AlterF (AltData con) bs e) = do + ct <- lookupVar g con + zipWithM_ fzip bs (ct ^.. arrowStops) + (t :< e') <- lintE (supplementVars (varsToPairs bs) g) (wrapFix e) + pure (t, AlterF (AltData con) bs e') + where + fzip (MkVar _ t) t' + | t == t' = Right () + | otherwise = Left (TypeErrorCouldNotMatch t t') + +unforall :: Type -> Type +unforall (TyForall _ m) = m +unforall m = m + +varsToPairs :: [Var] -> [(Name, Type)] +varsToPairs = toListOf (each . _MkVar) + +checkAgainst :: Gamma -> Var -> Expr Var -> SysF ET +checkAgainst g v@(MkVar n t) e = case lintE g e of + Right e'@(t' :< _) | t == t' -> Right e' + | otherwise -> Left (TypeErrorCouldNotMatch t t') + Left a -> Left a + +supplementVars :: [(Name, Type)] -> Gamma -> Gamma +supplementVars vs = gammaVars <>~ H.fromList vs + +supplementVar :: Name -> Type -> Gamma -> Gamma +supplementVar n t = gammaVars %~ H.insert n t + +supplementTyVar :: Name -> Kind -> Gamma -> Gamma +supplementTyVar n t = gammaTyVars %~ H.insert n t + +subst :: Name -> Type -> Type -> Type +subst k v (TyVar n) | k == n = v +subst k v (TyForall (MkVar n k') t) + | k /= n = TyForall (MkVar n k') (subst k v t) + | otherwise = TyForall (MkVar n k') t +subst k v (TyApp f x) = (TyApp `on` subst k v) f x +subst _ _ x = x + +isKind :: Type -> Bool +isKind (s :-> t) = isKind s && isKind t +isKind TyKindType = True +isKind _ = False + +kindOf :: Gamma -> Type -> SysF Kind +kindOf g (TyVar n) = lookupTyVar g n +kindOf _ TyKindType = pure TyKindType +kindOf g (TyCon n) = lookupCon g n +kindOf _ e = error (show e) + +lookupCon :: Gamma -> Name -> SysF Kind +lookupCon g n = case g ^. gammaTyCons . at n of + Just k -> Right k + Nothing -> Left (TypeErrorUndefinedVariable n) + +lookupVar :: Gamma -> Name -> SysF Type +lookupVar g n = case g ^. gammaVars . at n of + Just t -> Right t + Nothing -> Left (TypeErrorUndefinedVariable n) + +lookupTyVar :: Gamma -> Name -> SysF Kind +lookupTyVar g n = case g ^. gammaTyVars . at n of + Just k -> Right k + Nothing -> Left (TypeErrorUndefinedVariable n) + +demoContext :: Gamma +demoContext = Gamma + { _gammaVars = + [ ("id", TyForall ("a" :^ TyKindType) $ TyVar "a" :-> TyVar "a") + , ("Just", TyForall ("a" :^ TyKindType) $ + TyVar "a" :-> (TyCon "Maybe" `TyApp` TyVar "a")) + , ("Nothing", TyForall ("a" :^ TyKindType) $ + TyCon "Maybe" `TyApp` TyVar "a") + ] + , _gammaTyVars = [] + , _gammaTyCons = + [ ("Int#", TyKindType) + , ("Maybe", TyKindType :-> TyKindType) + ] + } +