git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Mutually recursive data types, part 2
commit2992586416c6ba33e82aa8b2fbcef73f2df7a273 authorPhil Freeman <paf31@cantab.net> dateFri 3 Jan 2014, 22:17 (13 years ago) parent9994812
4 files changed+155−79
compare with golang
unifiedsplit
examples/passing/MutRec.purs−2 src/Language/PureScript/TypeChecker.hs+73−36 src/Language/PureScript/TypeChecker/Kinds.hs+50−37 src/Language/PureScript/TypeChecker/Monad.hs+32−4
examples/passing/MutRec.purs−2
@@ -9,9 +9,7 @@ module MutRec where
99
1010 data Odd = Odd Even
1111
12− evenToNumber :: Even -> Number
1312 evenToNumber Zero = 0
1413 evenToNumber (Even n) = oddToNumber n + 1
1514
16− oddToNumber :: Odd -> Number
1715 oddToNumber (Odd n) = evenToNumber n + 1
src/Language/PureScript/TypeChecker.hs+73−36
@@ -35,53 +35,90 @@ import Language.PureScript.Names
3535import Language.PureScript.Kinds
3636import Language.PureScript.Declarations
3737
38+addDataType :: ModuleName -> ProperName -> [String] -> [(ProperName, Maybe Type)] -> Kind -> Check ()
39+addDataType moduleName name args dctors ctorKind = do
40+ env <- getEnv
41+ putEnv $ env { types = M.insert (moduleName, name) (ctorKind, Data) (types env) }
42+ forM_ dctors $ \(dctor, maybeTy) ->
43+ rethrow (("Error in data constructor " ++ show name ++ ":\n") ++) $
44+ addDataConstructor moduleName name args dctor maybeTy
45+
46+addDataConstructor :: ModuleName -> ProperName -> [String] -> ProperName -> Maybe Type -> Check ()
47+addDataConstructor moduleName name args dctor maybeTy = do
48+ env <- getEnv
49+ dataConstructorIsNotDefined moduleName dctor
50+ let retTy = foldl TypeApp (TypeConstructor (Qualified (Just moduleName) name)) (map TypeVar args)
51+ let dctorTy = maybe retTy (\ty -> Function [ty] retTy) maybeTy
52+ let polyType = mkForAll args dctorTy
53+ putEnv $ env { dataConstructors = M.insert (moduleName, dctor) polyType (dataConstructors env) }
54+
55+addTypeSynonym :: ModuleName -> ProperName -> [String] -> Type -> Kind -> Check ()
56+addTypeSynonym moduleName name args ty kind = do
57+ env <- getEnv
58+ putEnv $ env { types = M.insert (moduleName, name) (kind, TypeSynonym) (types env)
59+ , typeSynonyms = M.insert (moduleName, name) (args, ty) (typeSynonyms env) }
60+
61+typeIsNotDefined :: ModuleName -> ProperName -> Check ()
62+typeIsNotDefined moduleName name = do
63+ env <- getEnv
64+ guardWith (show name ++ " is already defined") $
65+ not $ M.member (moduleName, name) (types env)
66+
67+dataConstructorIsNotDefined :: ModuleName -> ProperName -> Check ()
68+dataConstructorIsNotDefined moduleName dctor = do
69+ env <- getEnv
70+ guardWith (show dctor ++ " is already defined") $
71+ not $ M.member (moduleName, dctor) (dataConstructors env)
72+
73+valueIsNotDefined :: ModuleName -> Ident -> Check ()
74+valueIsNotDefined moduleName name = do
75+ env <- getEnv
76+ case M.lookup (moduleName, name) (names env) of
77+ Just _ -> throwError $ show name ++ " is already defined"
78+ Nothing -> return ()
79+
80+addValue :: ModuleName -> Ident -> Type -> Check ()
81+addValue moduleName name ty = do
82+ env <- getEnv
83+ putEnv (env { names = M.insert (moduleName, name) (ty, Value) (names env) })
84+
3885typeCheckAll :: ModuleName -> [Declaration] -> Check ()
3986typeCheckAll _ [] = return ()
4087typeCheckAll moduleName (DataDeclaration name args dctors : rest) = do
4188 rethrow (("Error in type constructor " ++ show name ++ ":\n") ++) $ do
42− env <- getEnv
43− guardWith (show name ++ " is already defined") $ not $ M.member (moduleName, name) (types env)
44− ctorKind <- kindsOf moduleName (Just name) args (mapMaybe snd dctors)
45− putEnv $ env { types = M.insert (moduleName, name) (ctorKind, Data) (types env) }
46− forM_ dctors $ \(dctor, maybeTy) ->
47− rethrow (("Error in data constructor " ++ show name ++ ":\n") ++) $ do
48− env' <- getEnv
49− guardWith (show dctor ++ " is already defined") $ not $ M.member (moduleName, dctor) (dataConstructors env')
50− let retTy = foldl TypeApp (TypeConstructor (Qualified (Just moduleName) name)) (map TypeVar args)
51− let dctorTy = maybe retTy (\ty -> Function [ty] retTy) maybeTy
52− let polyType = mkForAll args dctorTy
53− putEnv $ env' { dataConstructors = M.insert (moduleName, dctor) polyType (dataConstructors env') }
89+ typeIsNotDefined moduleName name
90+ ctorKind <- kindsOf moduleName name args (mapMaybe snd dctors)
91+ addDataType moduleName name args dctors ctorKind
92+ typeCheckAll moduleName rest
93+typeCheckAll moduleName (DataBindingGroupDeclaration tys : rest) = do
94+ rethrow (("Error in data binding group " ++ show (map (\(name, _, _) -> name) tys) ++ ":\n") ++) $ do
95+ forM_ tys $ \(name, _, _) ->
96+ typeIsNotDefined moduleName name
97+ ks <- kindsOfAll moduleName (map (\(name, args, dctors) -> (name, args, mapMaybe snd dctors)) tys)
98+ forM (zip tys ks) $ \((name, args, dctors), ctorKind) ->
99+ addDataType moduleName name args dctors ctorKind
54100 typeCheckAll moduleName rest
55−typeCheckAll moduleName (DataBindingGroupDeclaration tys : rest) = error (show tys)
56101typeCheckAll moduleName (TypeSynonymDeclaration name args ty : rest) = do
57102 rethrow (("Error in type synonym " ++ show name ++ ":\n") ++) $ do
58− env <- getEnv
59− guardWith (show name ++ " is already defined") $ not $ M.member (moduleName, name) (types env)
60− kind <- kindsOf moduleName (Just name) args [ty]
61− putEnv $ env { types = M.insert (moduleName, name) (kind, TypeSynonym) (types env)
62− , typeSynonyms = M.insert (moduleName, name) (args, ty) (typeSynonyms env) }
103+ typeIsNotDefined moduleName name
104+ kind <- kindsOf moduleName name args [ty]
105+ addTypeSynonym moduleName name args ty kind
63106 typeCheckAll moduleName rest
64107typeCheckAll _ (TypeDeclaration _ _ : _) = error "Type declarations should have been removed"
65108typeCheckAll moduleName (ValueDeclaration name [] Nothing val : rest) = do
66109 rethrow (("Error in declaration " ++ show name ++ ":\n") ++) $ do
67− env <- getEnv
68− case M.lookup (moduleName, name) (names env) of
69− Just _ -> throwError $ show name ++ " is already defined"
70− Nothing -> do
71− [ty] <- typesOf moduleName [(name, val)]
72− putEnv (env { names = M.insert (moduleName, name) (ty, Value) (names env) })
110+ valueIsNotDefined moduleName name
111+ [ty] <- typesOf moduleName [(name, val)]
112+ addValue moduleName name ty
73113 typeCheckAll moduleName rest
74114typeCheckAll _ (ValueDeclaration _ _ _ _ : _) = error "Binders were not desugared"
75115typeCheckAll moduleName (BindingGroupDeclaration vals : rest) = do
76116 rethrow (("Error in binding group " ++ show (map fst vals) ++ ":\n") ++) $ do
77− forM_ (map fst vals) $ \name -> do
78− env <- getEnv
79− case M.lookup (moduleName, name) (names env) of
80− Just _ -> throwError $ show name ++ " is already defined"
81− Nothing -> return ()
117+ forM_ (map fst vals) $ \name ->
118+ valueIsNotDefined moduleName name
82119 tys <- typesOf moduleName vals
83120 forM (zip (map fst vals) tys) $ \(name, ty) ->
84− modifyEnv $ \env -> env { names = M.insert (moduleName, name) (ty, Value) (names env) }
121+ addValue moduleName name ty
85122 typeCheckAll moduleName rest
86123typeCheckAll moduleName (ExternDataDeclaration name kind : rest) = do
87124 env <- getEnv
@@ -124,22 +161,22 @@ typeCheckAll currentModule (ImportDeclaration moduleName idents : rest) = do
124161 guardWith ("Module " ++ show moduleName ++ " does not exist") $ moduleExists env
125162 case idents of
126163 Nothing -> do
127− bindIdents (map snd $ filterModule (names env)) env
128− bindTypes (map snd $ filterModule (types env)) env
164+ shadowIdents (map snd $ filterModule (names env)) env
165+ shadowTypes (map snd $ filterModule (types env)) env
129166 Just idents' -> do
130− bindIdents (lefts idents') env
131− bindTypes (rights idents') env
167+ shadowIdents (lefts idents') env
168+ shadowTypes (rights idents') env
132169 typeCheckAll currentModule rest
133170 where errorMessage = (("Error in import declaration " ++ show moduleName ++ ":\n") ++)
134171 filterModule = filter ((== moduleName) . fst) . M.keys
135172 moduleExists env = not (null (filterModule (names env))) || not (null (filterModule (types env)))
136− bindIdents idents' env =
173+ shadowIdents idents' env =
137174 forM_ idents' $ \ident -> do
138175 guardWith (show currentModule ++ "." ++ show ident ++ " is already defined") $ (currentModule, ident) `M.notMember` names env
139176 case (moduleName, ident) `M.lookup` names env of
140177 Just (pt, _) -> modifyEnv (\e -> e { names = M.insert (currentModule, ident) (pt, Alias moduleName ident) (names e) })
141178 Nothing -> throwError (show moduleName ++ "." ++ show ident ++ " is undefined")
142− bindTypes pns env =
179+ shadowTypes pns env =
143180 forM_ pns $ \pn -> do
144181 guardWith (show currentModule ++ "." ++ show pn ++ " is already defined") $ (currentModule, pn) `M.notMember` types env
145182 case (moduleName, pn) `M.lookup` types env of
src/Language/PureScript/TypeChecker/Kinds.hs+50−37
@@ -15,8 +15,9 @@
1515{-# LANGUAGE DeriveDataTypeable #-}
1616
1717module Language.PureScript.TypeChecker.Kinds (
18+ kindOf,
1819 kindsOf,
19− kindOf
20+ kindsOfAll
2021) where
2122
2223import Language.PureScript.Types
@@ -55,13 +56,30 @@ instance Unifiable Kind where
5556 unknowns _ = []
5657
5758kindOf :: ModuleName -> Type -> Check Kind
58−kindOf moduleName ty = fmap (\(k, _, _) -> k) . runSubst (SubstContext moduleName) $ starIfUnknown <$> infer Nothing M.empty ty
59+kindOf moduleName ty = fmap (\(k, _, _) -> k) . runSubst (SubstContext moduleName) $ starIfUnknown <$> infer ty
5960
60−kindsOf :: ModuleName -> Maybe ProperName -> [String] -> [Type] -> Check Kind
61+kindsOf :: ModuleName -> ProperName -> [String] -> [PolyType] -> Check Kind
6162kindsOf moduleName name args ts = fmap (starIfUnknown . (\(k, _, _) -> k)) . runSubst (SubstContext moduleName) $ do
6263 tyCon <- fresh
6364 kargs <- replicateM (length args) fresh
64− ks <- inferAll (fmap (\pn -> (pn, tyCon)) name) (M.fromList (zip args kargs)) ts
65+ let dict = (name, tyCon) : zip (map ProperName args) kargs
66+ bindLocalTypeVariables moduleName dict $
67+ solveTypes ts kargs tyCon
68+
69+kindsOfAll :: ModuleName -> [(ProperName, [String], [PolyType])] -> Check [Kind]
70+kindsOfAll moduleName tys = fmap (map starIfUnknown . (\(ks, _, _) -> ks)) . runSubst (SubstContext moduleName) $ do
71+ tyCons <- replicateM (length tys) fresh
72+ let dict = zipWith (\(name, _, _) tyCon -> (name, tyCon)) tys tyCons
73+ bindLocalTypeVariables moduleName dict $
74+ zipWithM (\tyCon (_, args, ts) -> do
75+ kargs <- replicateM (length args) fresh
76+ let argDict = zip (map ProperName args) kargs
77+ bindLocalTypeVariables moduleName argDict $
78+ solveTypes ts kargs tyCon) tyCons tys
79+
80+solveTypes :: [Type] -> [Kind] -> Kind -> Subst Kind
81+solveTypes ts kargs tyCon = do
82+ ks <- mapM infer ts
6583 tyCon ~~ foldr FunKind Star kargs
6684 forM_ ks $ \k -> k ~~ Star
6785 return tyCon
@@ -71,56 +89,51 @@ starIfUnknown (KUnknown _) = Star
7189starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
7290starIfUnknown k = k
7391
74−inferAll :: Maybe (ProperName, Kind) -> M.Map String Kind -> [Type] -> Subst [Kind]
75−inferAll name m = mapM (infer name m)
76−
77−infer :: Maybe (ProperName, Kind) -> M.Map String Kind -> Type -> Subst Kind
78−infer name m (Array t) = do
79− k <- infer name m t
92+infer :: Type -> Subst Kind
93+infer (Array t) = do
94+ k <- infer t
8095 k ~~ Star
8196 return Star
82−infer name m (Object row) = do
83− k <- inferRow name m row
97+infer (Object row) = do
98+ k <- inferRow row
8499 k ~~ Row
85100 return Star
86−infer name m (Function args ret) = do
87− ks <- inferAll name m args
88− k <- infer name m ret
101+infer (Function args ret) = do
102+ ks <- mapM infer args
103+ k <- infer ret
89104 k ~~ Star
90105 forM ks (~~ Star)
91106 return Star
92−infer _ m (TypeVar v) =
93− case M.lookup v m of
94− Just k -> return k
95− Nothing -> throwError $ "Unbound type variable " ++ v
96−infer (Just (name, k)) _ (TypeConstructor (Qualified Nothing pn)) | name == pn = return k
97−infer _ _ (TypeConstructor v) = do
107+infer (TypeVar v) = do
108+ moduleName <- substCurrentModule <$> ask
109+ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
110+infer (TypeConstructor v) = do
98111 env <- liftCheck getEnv
99112 moduleName <- substCurrentModule `fmap` ask
100113 case M.lookup (qualify moduleName v) (types env) of
101114 Nothing -> throwError $ "Unknown type constructor '" ++ show v ++ "'"
102115 Just (kind, _) -> return kind
103−infer name m (TypeApp t1 t2) = do
116+infer (TypeApp t1 t2) = do
104117 k0 <- fresh
105− k1 <- infer name m t1
106− k2 <- infer name m t2
118+ k1 <- infer t1
119+ k2 <- infer t2
107120 k1 ~~ FunKind k2 k0
108121 return k0
109−infer name m (ForAll ident ty) = do
122+infer (ForAll ident ty) = do
110123 k <- fresh
111− infer name (M.insert ident k m) ty
112−infer _ _ _ = return Star
124+ moduleName <- substCurrentModule <$> ask
125+ bindLocalTypeVariables moduleName [(ProperName ident, k)] $ infer ty
126+infer _ = return Star
113127
114−inferRow :: Maybe (ProperName, Kind) -> M.Map String Kind -> Row -> Subst Kind
115−inferRow _ m (RowVar v) = do
116− case M.lookup v m of
117− Just k -> return k
118− Nothing -> throwError $ "Unbound row variable " ++ v
119−inferRow _ _ REmpty = return Row
120−inferRow name m (RCons _ ty row) = do
121− k1 <- infer name m ty
122− k2 <- inferRow name m row
128+inferRow :: Row -> Subst Kind
129+inferRow (RowVar v) = do
130+ moduleName <- substCurrentModule <$> ask
131+ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
132+inferRow REmpty = return Row
133+inferRow (RCons _ ty row) = do
134+ k1 <- infer ty
135+ k2 <- inferRow row
123136 k1 ~~ Star
124137 k2 ~~ Row
125138 return Row
126−inferRow _ _ _ = error "Invalid row in inferRow"
139+inferRow _ = error "Invalid row in inferRow"
src/Language/PureScript/TypeChecker/Monad.hs+32−4
@@ -32,9 +32,18 @@ import Control.Monad.Reader
3232
3333import qualified Data.Map as M
3434
35−data NameKind = Value | Extern | Alias ModuleName Ident | LocalVariable deriving Show
36−
37−data TypeDeclarationKind = Data | ExternData | TypeSynonym | DataAlias ModuleName ProperName deriving Show
35+data NameKind
36+ = Value
37+ | Extern
38+ | Alias ModuleName Ident
39+ | LocalVariable deriving Show
40+
41+data TypeDeclarationKind
42+ = Data
43+ | ExternData
44+ | TypeSynonym
45+ | DataAlias ModuleName ProperName
46+ | LocalTypeVariable deriving Show
3847
3948data Environment = Environment
4049 { names :: M.Map (ModuleName, Ident) (Type, NameKind)
@@ -49,16 +58,28 @@ emptyEnvironment = Environment M.empty M.empty M.empty M.empty M.empty
4958
5059bindNames :: (MonadState CheckState m) => M.Map (ModuleName, Ident) (Type, NameKind) -> m a -> m a
5160bindNames newNames action = do
52− orig <- get
61+ orig <- get
5362 modify $ \st -> st { checkEnv = (checkEnv st) { names = newNames `M.union` (names . checkEnv $ st) } }
5463 a <- action
5564 modify $ \st -> st { checkEnv = (checkEnv st) { names = names . checkEnv $ orig } }
5665 return a
5766
67+bindTypes :: (MonadState CheckState m) => M.Map (ModuleName, ProperName) (Kind, TypeDeclarationKind) -> m a -> m a
68+bindTypes newNames action = do
69+ orig <- get
70+ modify $ \st -> st { checkEnv = (checkEnv st) { types = newNames `M.union` (types . checkEnv $ st) } }
71+ a <- action
72+ modify $ \st -> st { checkEnv = (checkEnv st) { types = types . checkEnv $ orig } }
73+ return a
74+
5875bindLocalVariables :: (Functor m, MonadState CheckState m) => ModuleName -> [(Ident, Type)] -> m a -> m a
5976bindLocalVariables moduleName bindings action =
6077 bindNames (M.fromList $ flip map bindings $ \(name, ty) -> ((moduleName, name), (ty, LocalVariable))) action
6178
79+bindLocalTypeVariables :: (Functor m, MonadState CheckState m) => ModuleName -> [(ProperName, Kind)] -> m a -> m a
80+bindLocalTypeVariables moduleName bindings action =
81+ bindTypes (M.fromList $ flip map bindings $ \(name, k) -> ((moduleName, name), (k, LocalTypeVariable))) action
82+
6283lookupVariable :: (Functor m, MonadState CheckState m, MonadError String m) => ModuleName -> Qualified Ident -> m Type
6384lookupVariable currentModule (Qualified moduleName var) = do
6485 env <- getEnv
@@ -66,6 +87,13 @@ lookupVariable currentModule (Qualified moduleName var) = do
6687 Nothing -> throwError $ show var ++ " is undefined"
6788 Just (ty, _) -> return ty
6889
90+lookupTypeVariable :: (Functor m, MonadState CheckState m, MonadError String m) => ModuleName -> Qualified ProperName -> m Kind
91+lookupTypeVariable currentModule (Qualified moduleName name) = do
92+ env <- getEnv
93+ case M.lookup (fromMaybe currentModule moduleName, name) (types env) of
94+ Nothing -> throwError $ "Type variable " ++ show name ++ " is undefined"
95+ Just (k, _) -> return k
96+
6997data AnyUnifiable where
7098 AnyUnifiable :: forall t. (Unifiable t) => t -> AnyUnifiable
7199