9aa9339 · rowtype-yoga/purescript-native

git.iko.soy/rowtype-yoga/purescript-native

Combine Type and Row types to facilitate kind-checking effects later.

commit9aa93398256a9b01c310a8106bd1183657967078 authorPhil Freeman <paf31@cantab.net> dateSun 5 Jan 2014, 16:22 (13 years ago) parent3b68926

9 files changed+78−104

compare with golang

unifiedsplit

src/Language/PureScript/BindingGroups.hs+1−1 src/Language/PureScript/Declarations.hs+6−6 src/Language/PureScript/Parser/Types.hs+5−5 src/Language/PureScript/Pretty/Types.hs+6−6 src/Language/PureScript/Pretty/Values.hs+1−1 src/Language/PureScript/TypeChecker/Kinds.hs+10−13 src/Language/PureScript/TypeChecker/Types.hs+41−57 src/Language/PureScript/Types.hs+7−14 src/Language/PureScript/Values.hs+1−1

src/Language/PureScript/BindingGroups.hs+1−1

@@ -93,6 +93,6 @@ fromValueDecl (ValueDeclaration ident [] Nothing val) = (ident, val)

9393fromValueDecl (ValueDeclaration _ _ _ _) = error "Binders should have been desugared"

9494fromValueDecl _ = error "Expected ValueDeclaration"

9595

96−fromDataDecl :: Declaration -> (ProperName, [String], [(ProperName, Maybe PolyType)])

96+fromDataDecl :: Declaration -> (ProperName, [String], [(ProperName, Maybe Type)])

9797fromDataDecl (DataDeclaration pn args ctors) = (pn, args, ctors)

9898fromDataDecl _ = error "Expected DataDeclaration"

src/Language/PureScript/Declarations.hs+6−6

@@ -32,14 +32,14 @@ data Fixity = Fixity Associativity Precedence deriving (Show, D.Data, D.Typeable

3232data Module = Module ProperName [Declaration] deriving (Show, D.Data, D.Typeable)

3333

3434data Declaration

35− = DataDeclaration ProperName [String] [(ProperName, Maybe PolyType)]

36− | DataBindingGroupDeclaration [(ProperName, [String], [(ProperName, Maybe PolyType)])]

37− | TypeSynonymDeclaration ProperName [String] PolyType

38− | TypeDeclaration Ident PolyType

35+ = DataDeclaration ProperName [String] [(ProperName, Maybe Type)]

36+ | DataBindingGroupDeclaration [(ProperName, [String], [(ProperName, Maybe Type)])]

37+ | TypeSynonymDeclaration ProperName [String] Type

38+ | TypeDeclaration Ident Type

3939 | ValueDeclaration Ident [[Binder]] (Maybe Guard) Value

4040 | BindingGroupDeclaration [(Ident, Value)]

41− | ExternDeclaration Ident PolyType

42− | ExternMemberDeclaration String Ident PolyType

41+ | ExternDeclaration Ident Type

42+ | ExternMemberDeclaration String Ident Type

4343 | ExternDataDeclaration ProperName Kind

4444 | FixityDeclaration Fixity String

4545 | ImportDeclaration ModuleName (Maybe [Either Ident ProperName])

src/Language/PureScript/Parser/Types.hs+5−5

@@ -84,7 +84,7 @@ parseType = do

8484 unless (isMonoType ty) $ P.unexpected "polymorphic type"

8585 return ty

8686

87−parsePolyType :: P.Parsec String ParseState PolyType

87+parsePolyType :: P.Parsec String ParseState Type

8888parsePolyType = do

8989 ty <- parseAnyType

9090 unless (isPolyType ty) $ P.unexpected "polymorphic type"

@@ -93,12 +93,12 @@ parsePolyType = do

9393parseNameAndType :: P.Parsec String ParseState (String, Type)

9494parseNameAndType = (,) <$> (indented *> identifier <* indented <* lexeme (P.string "::")) <*> parsePolyType

9595

96−parseRowEnding :: P.Parsec String ParseState Row

97−parseRowEnding = P.option REmpty (RowVar <$> (lexeme (indented *> P.char '|') *> indented *> identifier))

96+parseRowEnding :: P.Parsec String ParseState Type

97+parseRowEnding = P.option REmpty (TypeVar <$> (lexeme (indented *> P.char '|') *> indented *> identifier))

9898

99−parseRow :: P.Parsec String ParseState Row

99+parseRow :: P.Parsec String ParseState Type

100100parseRow = (fromList <$> (commaSep parseNameAndType) <*> parseRowEnding) P.<?> "row"

101101 where

102− fromList :: [(String, Type)] -> Row -> Row

102+ fromList :: [(String, Type)] -> Type -> Type

103103 fromList [] r = r

104104 fromList ((name, t):ts) r = RCons name t (fromList ts r)

src/Language/PureScript/Pretty/Types.hs+6−6

@@ -41,18 +41,18 @@ typeLiterals = mkPattern match

4141 match (ForAll ident ty) = Just $ "forall " ++ ident ++ ". " ++ prettyPrintType ty

4242 match _ = Nothing

4343

44−prettyPrintRow :: Row -> String

44+prettyPrintRow :: Type -> String

4545prettyPrintRow = (\(tys, rest) -> intercalate ", " (map (uncurry nameAndTypeToPs) tys) ++ tailToPs rest) . toList []

4646 where

4747 nameAndTypeToPs :: String -> Type -> String

4848 nameAndTypeToPs name ty = name ++ " :: " ++ prettyPrintType ty

49− tailToPs :: Row -> String

49+ tailToPs :: Type -> String

5050 tailToPs REmpty = ""

51− tailToPs (RUnknown (Unknown u)) = " | u" ++ show u

52− tailToPs (RowVar var) = " | " ++ var

53− tailToPs (RSkolem s) = " | s" ++ show s

51+ tailToPs (TUnknown (Unknown u)) = " | u" ++ show u

52+ tailToPs (TypeVar var) = " | " ++ var

53+ tailToPs (Skolem s) = " | s" ++ show s

5454 tailToPs _ = error "Invalid row tail"

55− toList :: [(String, Type)] -> Row -> ([(String, Type)], Row)

55+ toList :: [(String, Type)] -> Type -> ([(String, Type)], Type)

5656 toList tys (RCons name ty row) = toList ((name, ty):tys) row

5757 toList tys r = (tys, r)

5858

src/Language/PureScript/Pretty/Values.hs+1−1

@@ -82,7 +82,7 @@ lam = mkPattern match

8282 match (Abs args val) = Just (map show args, val)

8383 match _ = Nothing

8484

85−typed :: Pattern () Value (PolyType, Value)

85+typed :: Pattern () Value (Type, Value)

8686typed = mkPattern match

8787 where

8888 match (TypedValue val ty) = Just (ty, val)

src/Language/PureScript/TypeChecker/Kinds.hs+10−13

@@ -59,7 +59,7 @@ instance Unifiable Kind where

5959kindOf :: ModuleName -> Type -> Check Kind

6060kindOf moduleName ty = fmap (\(k, _, _) -> k) . runSubst (SubstContext moduleName) $ starIfUnknown <$> infer ty

6161

62−kindsOf :: ModuleName -> ProperName -> [String] -> [PolyType] -> Check Kind

62+kindsOf :: ModuleName -> ProperName -> [String] -> [Type] -> Check Kind

6363kindsOf moduleName name args ts = fmap (starIfUnknown . (\(k, _, _) -> k)) . runSubst (SubstContext moduleName) $ do

6464 tyCon <- fresh

6565 kargs <- replicateM (length args) fresh

@@ -67,7 +67,7 @@ kindsOf moduleName name args ts = fmap (starIfUnknown . (\(k, _, _) -> k)) . run

6767 bindLocalTypeVariables moduleName dict $

6868 solveTypes ts kargs tyCon

6969

70−kindsOfAll :: ModuleName -> [(ProperName, [String], [PolyType])] -> Check [Kind]

70+kindsOfAll :: ModuleName -> [(ProperName, [String], [Type])] -> Check [Kind]

7171kindsOfAll moduleName tys = fmap (map starIfUnknown . (\(ks, _, _) -> ks)) . runSubst (SubstContext moduleName) $ do

7272 tyCons <- replicateM (length tys) fresh

7373 let dict = zipWith (\(name, _, _) tyCon -> (name, tyCon)) tys tyCons

@@ -91,12 +91,15 @@ starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)

9191starIfUnknown k = k

9292

9393infer :: Type -> Subst Kind

94+infer Number = return Star

95+infer String = return Star

96+infer Boolean = return Star

9497infer (Array t) = do

9598 k <- infer t

9699 k ~~ Star

97100 return Star

98101infer (Object row) = do

99− k <- inferRow row

102+ k <- infer row

100103 k ~~ Row

101104 return Star

102105infer (Function args ret) = do

@@ -124,17 +127,11 @@ infer (ForAll ident ty) = do

124127 k <- fresh

125128 moduleName <- substCurrentModule <$> ask

126129 bindLocalTypeVariables moduleName [(ProperName ident, k)] $ infer ty

127−infer _ = return Star

128−

129−inferRow :: Row -> Subst Kind

130−inferRow (RowVar v) = do

131− moduleName <- substCurrentModule <$> ask

132− lookupTypeVariable moduleName (Qualified Nothing (ProperName v))

133−inferRow REmpty = return Row

134−inferRow (RCons _ ty row) = do

130+infer REmpty = return Row

131+infer (RCons _ ty row) = do

135132 k1 <- infer ty

136− k2 <- inferRow row

133+ k2 <- infer row

137134 k1 ~~ Star

138135 k2 ~~ Row

139136 return Row

140−inferRow _ = error "Invalid row in inferRow"

137+infer _ = error "Invalid argument to infer"

src/Language/PureScript/TypeChecker/Types.hs+41−57

@@ -57,6 +57,7 @@ instance Unifiable Type where

5757 apply s (Object r) = Object (apply s r)

5858 apply s (Function args ret) = Function (map (apply s) args) (apply s ret)

5959 apply s (TypeApp t1 t2) = TypeApp (apply s t1) (apply s t2)

60+ apply s (RCons name ty r) = RCons name (apply s ty) (apply s r)

6061 apply _ t = t

6162 unknowns (TUnknown (Unknown u)) = [u]

6263 unknowns (SaturatedTypeSynonym _ tys) = concatMap unknowns tys

@@ -65,40 +66,6 @@ instance Unifiable Type where

6566 unknowns (Object r) = unknowns r

6667 unknowns (Function args ret) = concatMap unknowns args ++ unknowns ret

6768 unknowns (TypeApp t1 t2) = unknowns t1 ++ unknowns t2

68− unknowns _ = []

69−

70−instance Unifiable Row where

71− unknown = RUnknown

72− isUnknown (RUnknown u) = Just u

73− isUnknown _ = Nothing

74− r1 ~~ r2 =

75− let

76− (s1, r1') = rowToList r1

77− (s2, r2') = rowToList r2

78− int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]

79− sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]

80− sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]

81− in do

82− forM_ int (uncurry (~~))

83− unifyRows sd1 r1' sd2 r2'

84− where

85− unifyRows :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Subst ()

86− unifyRows [] (RUnknown u) sd r = replace u (rowFromList (sd, r))

87− unifyRows sd r [] (RUnknown u) = replace u (rowFromList (sd, r))

88− unifyRows ((name, ty):row) r others u@(RUnknown un) = do

89− occursCheck un ty

90− forM row $ \(_, t) -> occursCheck un t

91− u' <- fresh

92− u ~~ RCons name ty u'

93− unifyRows row r others u'

94− unifyRows [] REmpty [] REmpty = return ()

95− unifyRows [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return ()

96− unifyRows [] (RSkolem s1) [] (RSkolem s2) | s1 == s2 = return ()

97− unifyRows sd3 r3 sd4 r4 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd3, r3)) ++ " with " ++ prettyPrintRow (rowFromList (sd4, r4)) ++ "."

98− apply s (RUnknown u) = runSubstitution s u

99− apply s (RCons name ty r) = RCons name (apply s ty) (apply s r)

100− apply _ r = r

101− unknowns (RUnknown (Unknown u)) = [u]

10269 unknowns (RCons _ ty r) = unknowns ty ++ unknowns r

10370 unknowns _ = []

10471

@@ -141,8 +108,38 @@ unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 +

141108 t3 `unifyTypes` t5

142109 t4 `unifyTypes` t6

143110 unifyTypes' (Skolem s1) (Skolem s2) | s1 == s2 = return ()

111+ unifyTypes' r1@(RCons _ _ _) r2 = unifyRows r1 r2

112+ unifyTypes' r1 r2@(RCons _ _ _) = unifyRows r1 r2

113+ unifyTypes' r1@REmpty r2 = unifyRows r1 r2

114+ unifyTypes' r1 r2@REmpty = unifyRows r1 r2

144115 unifyTypes' t3 t4 = throwError $ "Cannot unify " ++ prettyPrintType t3 ++ " with " ++ prettyPrintType t4 ++ "."

145116

117+unifyRows :: Type -> Type -> Subst ()

118+unifyRows r1 r2 =

119+ let

120+ (s1, r1') = rowToList r1

121+ (s2, r2') = rowToList r2

122+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]

123+ sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]

124+ sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]

125+ in do

126+ forM_ int (uncurry (~~))

127+ unifyRows' sd1 r1' sd2 r2'

128+ where

129+ unifyRows' :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Subst ()

130+ unifyRows' [] (TUnknown u) sd r = replace u (rowFromList (sd, r))

131+ unifyRows' sd r [] (TUnknown u) = replace u (rowFromList (sd, r))

132+ unifyRows' ((name, ty):row) r others u@(TUnknown un) = do

133+ occursCheck un ty

134+ forM row $ \(_, t) -> occursCheck un t

135+ u' <- fresh

136+ u ~~ RCons name ty u'

137+ unifyRows' row r others u'

138+ unifyRows' [] REmpty [] REmpty = return ()

139+ unifyRows' [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = return ()

140+ unifyRows' [] (Skolem s1) [] (Skolem s2) | s1 == s2 = return ()

141+ unifyRows' sd3 r3 sd4 r4 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd3, r3)) ++ " with " ++ prettyPrintRow (rowFromList (sd4, r4)) ++ "."

142+

146143typeConstructorsAreEqual :: Environment -> ModuleName -> Qualified ProperName -> Qualified ProperName -> Bool

147144typeConstructorsAreEqual env moduleName c1 c2 =

148145 let

@@ -198,16 +195,14 @@ escapeCheck checks ty sub =

198195

199196skolemEscapeCheck :: Type -> Check ()

200197skolemEscapeCheck ty =

201− case something (extQ (mkQ Nothing findSkolems) findRSkolems) ty of

198+ case something (mkQ Nothing findSkolems) ty of

202199 Nothing -> return ()

203200 Just _ -> throwError "Skolem variables cannot escape. Consider adding a type signature."

204201 where

205202 findSkolems (Skolem _) = return ()

206203 findSkolems _ = mzero

207− findRSkolems (RSkolem _) = return ()

208− findRSkolems _ = mzero

209204

210−setify :: Row -> Row

205+setify :: Type -> Type

211206setify = rowFromList . first (M.toList . M.fromList) . rowToList

212207

213208setifyAll :: (D.Data d) => d -> d

@@ -217,13 +212,10 @@ varIfUnknown :: Type -> Type

217212varIfUnknown ty =

218213 let unks = nub $ unknowns ty

219214 toName = (:) 't' . show

220− ty' = everywhere (mkT rowToVar) . everywhere (mkT typeToVar) $ ty

215+ ty' = everywhere (mkT typeToVar) $ ty

221216 typeToVar :: Type -> Type

222217 typeToVar (TUnknown (Unknown u)) = TypeVar (toName u)

223218 typeToVar t = t

224− rowToVar :: Row -> Row

225− rowToVar (RUnknown (Unknown u)) = RowVar (toName u)

226− rowToVar t = t

227219 in mkForAll (sort . map toName $ unks) ty'

228220

229221replaceAllTypeVars :: (D.Data d) => [(String, Type)] -> d -> d

@@ -237,12 +229,6 @@ replaceTypeVars name t = everywhereBut (mkQ False isShadowed) (mkT replaceTypeVa

237229 isShadowed (ForAll v _) | v == name = True

238230 isShadowed _ = False

239231

240−replaceRowVars :: (D.Data d) => String -> Row -> d -> d

241−replaceRowVars name r = everywhere (mkT replaceRowVar)

242− where

243− replaceRowVar (RowVar v) | v == name = r

244− replaceRowVar other = other

245−

246232replaceAllVarsWithUnknowns :: Type -> Subst Type

247233replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns

248234replaceAllVarsWithUnknowns ty = return ty

@@ -250,8 +236,7 @@ replaceAllVarsWithUnknowns ty = return ty

250236replaceVarWithUnknown :: String -> Type -> Subst Type

251237replaceVarWithUnknown ident ty = do

252238 tu <- fresh

253− ru <- fresh

254− return $ replaceRowVars ident ru . replaceTypeVars ident tu $ ty

239+ return $ replaceTypeVars ident tu $ ty

255240

256241replaceAllTypeSynonyms :: (Functor m, MonadState CheckState m, MonadReader SubstContext m, MonadError String m) => (D.Data d) => d -> m d

257242replaceAllTypeSynonyms d = do

@@ -488,7 +473,7 @@ inferBinder val (ObjectBinder props) = do

488473 val ~~ Object row

489474 return m1

490475 where

491− inferRowProperties :: Row -> Row -> [(String, Binder)] -> Subst (M.Map Ident Type)

476+ inferRowProperties :: Type -> Type -> [(String, Binder)] -> Subst (M.Map Ident Type)

492477 inferRowProperties nrow row [] = nrow ~~ row >> return M.empty

493478 inferRowProperties nrow row ((name, binder):binders) = do

494479 propTy <- fresh

@@ -598,8 +583,7 @@ checkBlock mass ret (s:ss) = do

598583skolemize :: String -> Type -> Subst Type

599584skolemize ident ty = do

600585 tsk <- Skolem <$> fresh'

601− rsk <- RSkolem <$> fresh'

602− return $ replaceRowVars ident rsk $ replaceTypeVars ident tsk ty

586+ return $ replaceTypeVars ident tsk ty

603587

604588check :: Value -> Type -> Subst ()

605589check val ty = rethrow errorMessage $ check' val ty

@@ -684,15 +668,15 @@ check' val (SaturatedTypeSynonym name args) = do

684668 check val ty

685669check' val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty

686670

687−checkProperties :: [(String, Value)] -> Row -> Bool -> Subst ()

671+checkProperties :: [(String, Value)] -> Type -> Bool -> Subst ()

688672checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where

689673 go [] [] REmpty = return ()

690− go [] [] u@(RUnknown _) = u ~~ REmpty

691− go [] [] (RSkolem _) | lax = return ()

674+ go [] [] u@(TUnknown _) = u ~~ REmpty

675+ go [] [] (Skolem _) | lax = return ()

692676 go [] ((p, _): _) _ | lax = return ()

693677 | otherwise = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have property " ++ p

694678 go ((p,_):_) [] REmpty = throwError $ "Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row

695− go ((p,v):ps') [] u@(RUnknown _) = do

679+ go ((p,v):ps') [] u@(TUnknown _) = do

696680 ty <- infer v

697681 rest <- fresh

698682 u ~~ RCons p ty rest

src/Language/PureScript/Types.hs+7−14

@@ -26,30 +26,23 @@ data Type

2626 | String

2727 | Boolean

2828 | Array Type

29− | Object Row

30− | Function [PolyType] Type

29+ | Object Type

30+ | Function [Type] Type

3131 | TypeVar String

3232 | TypeConstructor (Qualified ProperName)

3333 | TypeApp Type Type

3434 | SaturatedTypeSynonym (Qualified ProperName) [Type]

3535 | ForAll String Type

36− | Skolem Int deriving (Show, Eq, Data, Typeable)

37−

38−type PolyType = Type

39−

40−data Row

41− = RUnknown (Unknown Row)

42− | RowVar String

36+ | Skolem Int

4337 | REmpty

44− | RCons String Type Row

45− | RSkolem Int deriving (Show, Eq, Data, Typeable)

38+ | RCons String Type Type deriving (Show, Eq, Data, Typeable)

4639

47−rowToList :: Row -> ([(String, Type)], Row)

40+rowToList :: Type -> ([(String, Type)], Type)

4841rowToList (RCons name ty row) = let (tys, rest) = rowToList row

49− in ((name, ty):tys, rest)

42+ in ((name, ty):tys, rest)

5043rowToList r = ([], r)

5144

52−rowFromList :: ([(String, Type)], Row) -> Row

45+rowFromList :: ([(String, Type)], Type) -> Type

5346rowFromList ([], r) = r

5447rowFromList ((name, t):ts, r) = RCons name t (rowFromList (ts, r))

5548

src/Language/PureScript/Values.hs+1−1

@@ -70,7 +70,7 @@ data Value

7070 | Block [Statement]

7171 | Constructor (Qualified ProperName)

7272 | Case [Value] [([Binder], Maybe Guard, Value)]

73− | TypedValue Value PolyType deriving (Show, Data, Typeable)

73+ | TypedValue Value Type deriving (Show, Data, Typeable)

7474

7575data Statement

7676 = VariableIntroduction Ident Value