b3b0317 · rowtype-yoga/purescript-native

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

on golang help sign in

More work on RankNTypes

b3b0317Phil Freeman13 years ago

examples/failing/Rank2Types.psnew file+3

compare with golang

unifiedsplit

@@ -0,0 +1,3 @@

1+foreign import test :: (forall a. a -> a) -> Number

3+test1 = test (\n -> n + 1)

examples/passing/ObjectUpdate.ps+4−1

@@ -1,4 +1,7 @@

1+update1 = \o -> o { foo = "Foo" }

3+update2 :: forall r. { foo :: String | r } -> { foo :: String | r }

1−update = \o -> o { foo = "Foo" }

4+update2 = \o -> o { foo = "Foo" }

3replace = \o -> case o of

6replace = \o -> case o of

4 { foo = "Foo" } -> o { foo = "Bar" }

7 { foo = "Foo" } -> o { foo = "Bar" }

examples/passing/Objects.ps+3

@@ -7,3 +7,6 @@ apTest = append({foo : "Foo", baz: "Baz"})

7f = (\a -> a.b.c) { b: { c: 1, d: "Hello" }, e: "World" }

9g = (\a -> a.f { x: 1, y: "y" }) { f: \o -> o.x + 1 }

10+

11+typed :: { foo :: Number }

12+typed = { foo: 0 }

purescript.cabal+1

@@ -36,6 +36,7 @@ library

36 Language.PureScript.TypeChecker.Monad

37 Language.PureScript.TypeChecker.Types

38 Language.PureScript.TypeChecker.Synonyms

39+ Language.PureScript.Unknown

39 exposed: True

40 exposed: True

40 buildable: True

41 buildable: True

41 hs-source-dirs: src

42 hs-source-dirs: src

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

@@ -56,8 +56,8 @@ parseTypeConstructor :: P.Parsec String ParseState Type

56parseTypeConstructor = TypeConstructor <$> parseQualified properName

58parseForAll :: P.Parsec String ParseState Type

59−parseForAll = (ForAll <$> (P.try (reserved "forall") *> many (indented *> identifier) <* indented <* dot)

59+parseForAll = (mkForAll <$> (P.try (reserved "forall") *> P.many1 (indented *> identifier) <* indented <* dot)

60− <*> parseType)

60+ <*> parseType)

62parseTypeAtom :: P.Parsec String ParseState Type

63parseTypeAtom = indented *> P.choice (map P.try

src/Language/PureScript/Pretty/Kinds.hs+2−1

@@ -25,13 +25,14 @@ import Control.Applicative

26import Language.PureScript.Kinds

27import Language.PureScript.Pretty.Common

28+import Language.PureScript.Unknown

29typeLiterals :: Pattern () Kind String

30typeLiterals :: Pattern () Kind String

30typeLiterals = mkPattern match

31typeLiterals = mkPattern match

31 where

32 where

32 match Star = Just "*"

33 match Star = Just "*"

33 match Row = Just "#"

34 match Row = Just "#"

34− match (KUnknown u) = Just $ 'u' : show u

35+ match (KUnknown (Unknown u)) = Just $ 'u' : show u

35 match _ = Nothing

36 match _ = Nothing

37funKind :: Pattern () Kind (Kind, Kind)

38funKind :: Pattern () Kind (Kind, Kind)

src/Language/PureScript/Pretty/Types.hs+5−4

@@ -30,6 +30,7 @@ import Language.PureScript.Names

30import Language.PureScript.Declarations

31import Language.PureScript.TypeChecker.Monad

32import Language.PureScript.Pretty.Common

33+import Language.PureScript.Unknown

34typeLiterals :: Pattern () Type String

35typeLiterals :: Pattern () Type String

35typeLiterals = mkPattern match

36typeLiterals = mkPattern match

@@ -41,11 +42,10 @@ typeLiterals = mkPattern match

41 match (Object row) = Just $ "{ " ++ prettyPrintRow row ++ " }"

42 match (Object row) = Just $ "{ " ++ prettyPrintRow row ++ " }"

42 match (TypeVar var) = Just var

43 match (TypeVar var) = Just var

43 match (TypeConstructor ctor) = Just $ show ctor

44 match (TypeConstructor ctor) = Just $ show ctor

44− match (TUnknown u) = Just $ 'u' : show u

45+ match (TUnknown (Unknown u)) = Just $ 'u' : show u

45 match (Skolem s) = Just $ 's' : show s

46 match (Skolem s) = Just $ 's' : show s

46 match (SaturatedTypeSynonym name args) = Just $ show name ++ "<" ++ intercalate "," (map prettyPrintType args) ++ ">"

47 match (SaturatedTypeSynonym name args) = Just $ show name ++ "<" ++ intercalate "," (map prettyPrintType args) ++ ">"

47− match (ForAll idents ty) | not (null idents) = Just $ "forall " ++ unwords idents ++ ". " ++ prettyPrintType ty

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

48− | otherwise = match ty

49 match _ = Nothing

51prettyPrintRow :: Row -> String

@@ -55,8 +55,9 @@ prettyPrintRow = (\(tys, tail) -> intercalate ", " (map (uncurry nameAndTypeToPs

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

56 tailToPs :: Row -> String

57 tailToPs REmpty = ""

58− tailToPs (RUnknown u) = " | " ++ show u

58+ tailToPs (RUnknown (Unknown u)) = " | u" ++ show u

59 tailToPs (RowVar var) = " | " ++ var

60+ tailToPs (RSkolem s) = " | s" ++ show s

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

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

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

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

62 toList tys r = (tys, r)

63 toList tys r = (tys, r)

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

@@ -54,7 +54,7 @@ typeCheckAll (DataDeclaration name args dctors : rest) = do

54 guardWith (show dctor ++ " is already defined") $ not $ M.member (modulePath, dctor) (dataConstructors env')

55 let retTy = foldl TypeApp (TypeConstructor (Qualified modulePath name)) (map TypeVar args)

56 let dctorTy = maybe retTy (\ty -> Function [ty] retTy) maybeTy

57− let polyType = ForAll args dctorTy

57+ let polyType = mkForAll args dctorTy

58 putEnv $ env' { dataConstructors = M.insert (modulePath, dctor) polyType (dataConstructors env') }

59 typeCheckAll rest

60typeCheckAll (TypeSynonymDeclaration name args ty : rest) = do

src/Language/PureScript/TypeChecker/Kinds.hs+11−15

@@ -65,13 +65,13 @@ kindOf :: Type -> Check Kind

65kindOf ty = runSubst $ starIfUnknown <$> infer Nothing M.empty ty

67kindsOf :: Maybe ProperName -> [String] -> [Type] -> Check Kind

68−kindsOf name args ts = runSubst $ do

68+kindsOf name args ts = fmap starIfUnknown $ runSubst $ do

69 tyCon <- fresh

70 kargs <- replicateM (length args) fresh

71 ks <- inferAll (fmap (\pn -> (pn, tyCon)) name) (M.fromList (zip args kargs)) ts

72 tyCon ~~ foldr FunKind Star kargs

73 forM_ ks $ \k -> k ~~ Star

74− return $ starIfUnknown tyCon

74+ return tyCon

76starIfUnknown :: Kind -> Kind

77starIfUnknown (KUnknown _) = Star

@@ -79,22 +79,18 @@ starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)

79starIfUnknown k = k

81inferAll :: Maybe (ProperName, Kind) -> M.Map String Kind -> [Type] -> Subst Check [Kind]

82−inferAll _ _ [] = return []

83−inferAll name m (t:ts) = do

84− k <- infer name m t

82+inferAll name m = mapM (infer name m)

85− ks <- inferAll name m ts

86− return (k:ks)

88infer :: Maybe (ProperName, Kind) -> M.Map String Kind -> Type -> Subst Check Kind

84infer :: Maybe (ProperName, Kind) -> M.Map String Kind -> Type -> Subst Check Kind

89−infer name m a@(Array t) = do

85+infer name m (Array t) = do

90 k <- infer name m t

86 k <- infer name m t

91 k ~~ Star

87 k ~~ Star

92 return Star

88 return Star

93−infer name m o@(Object row) = do

89+infer name m (Object row) = do

94 k <- inferRow name m row

90 k <- inferRow name m row

95 k ~~ Row

91 k ~~ Row

96 return Star

92 return Star

97−infer name m f@(Function args ret) = do

93+infer name m (Function args ret) = do

98 ks <- inferAll name m args

94 ks <- inferAll name m args

99 k <- infer name m ret

95 k <- infer name m ret

100 k ~~ Star

96 k ~~ Star

@@ -105,21 +101,21 @@ infer _ m (TypeVar v) =

105 Just k -> return k

101 Just k -> return k

106 Nothing -> throwError $ "Unbound type variable " ++ v

102 Nothing -> throwError $ "Unbound type variable " ++ v

107infer (Just (name, k)) m c@(TypeConstructor v@(Qualified (ModulePath []) pn)) | name == pn = return k

103infer (Just (name, k)) m c@(TypeConstructor v@(Qualified (ModulePath []) pn)) | name == pn = return k

108−infer name m c@(TypeConstructor v) = do

104+infer name m (TypeConstructor v) = do

109 env <- lift getEnv

105 env <- lift getEnv

110 modulePath <- checkModulePath `fmap` lift get

106 modulePath <- checkModulePath `fmap` lift get

111 case M.lookup (qualify modulePath v) (types env) of

107 case M.lookup (qualify modulePath v) (types env) of

112 Nothing -> throwError $ "Unknown type constructor '" ++ show v ++ "'"

108 Nothing -> throwError $ "Unknown type constructor '" ++ show v ++ "'"

113 Just (kind, _) -> return kind

109 Just (kind, _) -> return kind

114−infer name m a@(TypeApp t1 t2) = do

110+infer name m (TypeApp t1 t2) = do

115 k0 <- fresh

111 k0 <- fresh

116 k1 <- infer name m t1

112 k1 <- infer name m t1

117 k2 <- infer name m t2

113 k2 <- infer name m t2

118 k1 ~~ FunKind k2 k0

114 k1 ~~ FunKind k2 k0

119 return k0

115 return k0

120−infer name m (ForAll idents ty) = do

116+infer name m (ForAll ident ty) = do

121− ks <- replicateM (length idents) fresh

117+ k <- fresh

122− infer name (M.fromList (zip idents ks) `M.union` m) ty

118+ infer name (M.insert ident k m) ty

123infer _ m t = return Star

119infer _ m t = return Star

124

120

125inferRow :: Maybe (ProperName, Kind) -> M.Map String Kind -> Row -> Subst Check Kind

121inferRow :: Maybe (ProperName, Kind) -> M.Map String Kind -> Row -> Subst Check Kind

src/Language/PureScript/TypeChecker/Types.hs+196−92

@@ -18,9 +18,8 @@ module Language.PureScript.TypeChecker.Types (

18 typeOf

19) where

21−import Debug.Trace

22−

23import Data.List

21import Data.List

22+import Data.Maybe (fromMaybe)

24import Data.Function

23import Data.Function

25import qualified Data.Data as D

24import qualified Data.Data as D

26import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)

25import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)

@@ -63,8 +62,12 @@ instance Unifiable Type where

63 replaced ~~ ty

62 replaced ~~ ty

64 Nothing -> error "Type synonym was not defined"

63 Nothing -> error "Type synonym was not defined"

65 ty ~~ s@(SaturatedTypeSynonym _ _) = s ~~ ty

64 ty ~~ s@(SaturatedTypeSynonym _ _) = s ~~ ty

65+ ForAll ident1 ty1 ~~ ForAll ident2 ty2 = do

66+ sk <- skolemize ident1 ty1

67+ replaced <- replaceVarsWithUnknowns [ident2] ty2

68+ sk ~~ replaced

66− ForAll idents ty1 ~~ ty2 = do

69+ ForAll ident ty1 ~~ ty2 = do

67− sk <- skolemize idents ty1

70+ sk <- skolemize ident ty1

68 sk ~~ ty2

71 sk ~~ ty2

69 ty ~~ f@(ForAll _ _) = f ~~ ty

72 ty ~~ f@(ForAll _ _) = f ~~ ty

70 Number ~~ Number = return ()

73 Number ~~ Number = return ()

@@ -128,6 +131,7 @@ instance Unifiable Row where

128 unifyRows row r others u'

131 unifyRows row r others u'

129 unifyRows [] REmpty [] REmpty = return ()

132 unifyRows [] REmpty [] REmpty = return ()

130 unifyRows [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return ()

133 unifyRows [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return ()

134+ unifyRows [] (RSkolem s1) [] (RSkolem s2) | s1 == s2 = return ()

131 unifyRows sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd1, r1)) ++ " with " ++ prettyPrintRow (rowFromList (sd2, r2)) ++ "."

135 unifyRows sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd1, r1)) ++ " with " ++ prettyPrintRow (rowFromList (sd2, r2)) ++ "."

132 apply s (RUnknown u) = runSubstitution s u

136 apply s (RUnknown u) = runSubstitution s u

133 apply s (RCons name ty r) = RCons name (apply s ty) (apply s r)

137 apply s (RCons name ty r) = RCons name (apply s ty) (apply s r)

@@ -204,7 +208,7 @@ varIfUnknown ty =

204 let

208 let

205 (ty', m) = flip runState M.empty $ everywhereM (flip extM g $ mkM f) ty

209 (ty', m) = flip runState M.empty $ everywhereM (flip extM g $ mkM f) ty

206 in

210 in

207− ForAll (sort $ nub $ M.elems m ++ findTypeVars ty) ty'

211+ mkForAll (sort $ nub $ M.elems m ++ findTypeVars ty) ty'

208 where

212 where

209 f :: Type -> State (M.Map Int String) Type

213 f :: Type -> State (M.Map Int String) Type

210 f (TUnknown (Unknown n)) = do

214 f (TUnknown (Unknown n)) = do

@@ -235,6 +239,14 @@ replaceTypeVars m = everywhere (mkT replace)

235 _ -> TypeVar v

239 _ -> TypeVar v

236 replace t = t

240 replace t = t

237

241

242+replaceRowVars :: M.Map String Row -> Type -> Type

243+replaceRowVars m = everywhere (mkT replace)

244+ where

245+ replace (RowVar v) = case M.lookup v m of

246+ Just r -> r

247+ _ -> RowVar v

248+ replace t = t

249+

238replaceVarsWithUnknowns :: [String] -> Type -> Subst Check Type

250replaceVarsWithUnknowns :: [String] -> Type -> Subst Check Type

239replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)

251replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)

240 where

252 where

@@ -305,9 +317,8 @@ infer m (ObjectUpdate o ps) = do

305 return obj

317 return obj

306infer m (Indexer index val) = do

318infer m (Indexer index val) = do

307 el <- fresh

319 el <- fresh

308− t1 <- infer m index

320+ check m index Number

309 t2 <- infer m val

321 t2 <- infer m val

310− t1 ~~ Number

311 t2 ~~ Array el

322 t2 ~~ Array el

312 return el

323 return el

313infer m (Accessor prop val) = do

324infer m (Accessor prop val) = do

@@ -323,10 +334,9 @@ infer m v@(Abs args ret) = do

323 return $ Function ts body

334 return $ Function ts body

324infer m v@(App f xs) = do

335infer m v@(App f xs) = do

325 t1 <- infer m f

336 t1 <- infer m f

326− ts <- mapM (infer m) xs

337+ ret <- fresh

327− me <- fresh

338+ checkFunctionApplication m t1 xs ret

328− t1 ~~ Function ts me

329− return me

339+ return ret

330infer m v@(Var var@(Qualified mp name)) = do

340infer m v@(Var var@(Qualified mp name)) = do

331 case mp of

341 case mp of

332 ModulePath [] ->

342 ModulePath [] ->

@@ -351,72 +361,94 @@ infer m v@(Constructor c) = do

351 modulePath <- checkModulePath `fmap` lift get

361 modulePath <- checkModulePath `fmap` lift get

352 case M.lookup (qualify modulePath c) (dataConstructors env) of

362 case M.lookup (qualify modulePath c) (dataConstructors env) of

353 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"

363 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"

354− Just (ForAll idents ty) -> replaceVarsWithUnknowns idents ty

364+ Just ty -> return ty

355infer m (Case val binders) = do

365infer m (Case val binders) = do

356 t1 <- infer m val

366 t1 <- infer m val

357 ret <- fresh

367 ret <- fresh

358− cs2 <- checkBinders m t1 ret binders

368+ checkBinders m t1 ret binders

359 return ret

369 return ret

360infer m v@(IfThenElse cond th el) = do

370infer m v@(IfThenElse cond th el) = do

361− t1 <- infer m cond

371+ check m cond Boolean

362 t2 <- infer m th

372 t2 <- infer m th

363 t3 <- infer m el

373 t3 <- infer m el

364− t1 ~~ Boolean

365 t2 ~~ t3

374 t2 ~~ t3

366 return t2

375 return t2

367infer m v@(TypedValue val ty) = do

376infer m v@(TypedValue val ty) = do

368 kind <- lift $ kindOf ty

377 kind <- lift $ kindOf ty

369 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

378 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

370 ty' <- lift $ replaceAllTypeSynonyms ty

379 ty' <- lift $ replaceAllTypeSynonyms ty

371− cs <- check m val ty'

380+ check m val ty'

372 return ty'

381 return ty'

373

382

374inferUnary :: UnaryOperator -> Type -> Subst Check Type

383inferUnary :: UnaryOperator -> Type -> Subst Check Type

375−inferUnary Negate val = do

384+inferUnary op val =

376− val ~~ Number

385+ case fromMaybe (error "Invalid operator") $ lookup op unaryOps of

377− return Number

386+ (valTy, resTy) -> do

378−inferUnary Not val = do

387+ val ~~ valTy

388+ return resTy

389+

390+checkUnary :: M.Map Ident Type -> UnaryOperator -> Value -> Type -> Subst Check ()

391+checkUnary m op val res =

392+ case fromMaybe (error "Invalid operator") $ lookup op unaryOps of

393+ (valTy, resTy) -> do

394+ res ~~ resTy

395+ check m val valTy

396+

397+unaryOps :: [(UnaryOperator, (Type, Type))]

398+unaryOps = [ (Negate, (Number, Number))

379− val ~~ Boolean

399+ , (Not, (Boolean, Boolean))

380− return Boolean

381−inferUnary BitwiseNot val = do

400+ , (BitwiseNot, (Number, Number))

382− val ~~ Number

401+ ]

383− return Number

384

402

385inferBinary :: BinaryOperator -> Type -> Type -> Subst Check Type

403inferBinary :: BinaryOperator -> Type -> Type -> Subst Check Type

386−inferBinary Add = inferSymBinary Number

404+inferBinary op left right | isEqualityTest op = do

387−inferBinary Subtract = inferSymBinary Number

388−inferBinary Multiply = inferSymBinary Number

389−inferBinary Divide = inferSymBinary Number

390−inferBinary Modulus = inferSymBinary Number

391−inferBinary LessThan = inferAsymBinary Number Boolean

392−inferBinary LessThanOrEqualTo = inferAsymBinary Number Boolean

393−inferBinary GreaterThan = inferAsymBinary Number Boolean

394−inferBinary GreaterThanOrEqualTo = inferAsymBinary Number Boolean

395−inferBinary BitwiseAnd = inferSymBinary Number

396−inferBinary BitwiseOr = inferSymBinary Number

397−inferBinary BitwiseXor = inferSymBinary Number

398−inferBinary ShiftLeft = inferSymBinary Number

399−inferBinary ShiftRight = inferSymBinary Number

400−inferBinary ZeroFillShiftRight = inferSymBinary Number

401−inferBinary EqualTo = inferEqBinary

402−inferBinary NotEqualTo = inferEqBinary

403−inferBinary And = inferSymBinary Boolean

404−inferBinary Or = inferSymBinary Boolean

405−inferBinary Concat = inferSymBinary String

406−

407−inferEqBinary :: Type -> Type -> Subst Check Type

408−inferEqBinary left right = do

409 left ~~ right

405 left ~~ right

410 return Boolean

406 return Boolean

411−

407+inferBinary op left right =

412−inferSymBinary :: Type -> Type -> Type -> Subst Check Type

408+ case fromMaybe (error "Invalid operator") $ lookup op binaryOps of

413−inferSymBinary ty = inferAsymBinary ty ty

409+ (valTy, resTy) -> do

414−

415−inferAsymBinary :: Type -> Type -> Type -> Type -> Subst Check Type

416−inferAsymBinary input output left right = do

417− left ~~ input

410+ left ~~ valTy

418− right ~~ input

411+ right ~~ valTy

419− return output

412+ return resTy

413+

414+checkBinary :: M.Map Ident Type -> BinaryOperator -> Value -> Value -> Type -> Subst Check ()

415+checkBinary m op left right res | isEqualityTest op = do

416+ res ~~ Boolean

417+ t1 <- infer m left

418+ t2 <- infer m right

419+ t1 ~~ t2

420+checkBinary m op left right res =

421+ case fromMaybe (error "Invalid operator") $ lookup op binaryOps of

422+ (valTy, resTy) -> do

423+ res ~~ resTy

424+ check m left valTy

425+ check m right valTy

426+

427+isEqualityTest :: BinaryOperator -> Bool

428+isEqualityTest EqualTo = True

429+isEqualityTest NotEqualTo = True

430+isEqualityTest _ = False

431+

432+binaryOps :: [(BinaryOperator, (Type, Type))]

433+binaryOps = [ (Add, (Number, Number))

434+ , (Subtract, (Number, Number))

435+ , (Multiply, (Number, Number))

436+ , (Divide, (Number, Number))

437+ , (Modulus, (Number, Number))

438+ , (BitwiseAnd, (Number, Number))

439+ , (BitwiseOr, (Number, Number))

440+ , (BitwiseXor, (Number, Number))

441+ , (ShiftRight, (Number, Number))

442+ , (ZeroFillShiftRight, (Number, Number))

443+ , (And, (Boolean, Boolean))

444+ , (Or, (Boolean, Boolean))

445+ , (Concat, (String, String))

446+ , (Modulus, (Number, Number))

447+ , (LessThan, (Number, Boolean))

448+ , (LessThanOrEqualTo, (Number, Boolean))

449+ , (GreaterThan, (Number, Boolean))

450+ , (GreaterThanOrEqualTo, (Number, Boolean))

451+ ]

420

452

421inferBinder :: Type -> Binder -> Subst Check (M.Map Ident Type)

453inferBinder :: Type -> Binder -> Subst Check (M.Map Ident Type)

422inferBinder _ NullBinder = return M.empty

454inferBinder _ NullBinder = return M.empty

@@ -428,23 +460,18 @@ inferBinder val (NullaryBinder ctor) = do

428 env <- lift getEnv

460 env <- lift getEnv

429 modulePath <- checkModulePath `fmap` lift get

461 modulePath <- checkModulePath `fmap` lift get

430 case M.lookup (qualify modulePath ctor) (dataConstructors env) of

462 case M.lookup (qualify modulePath ctor) (dataConstructors env) of

431− Just (ForAll args ret) -> do

463+ Just ty -> do

432− ret' <- replaceVarsWithUnknowns args ret

464+ ty `subsumes` val

433− val ~~ ret'

434 return M.empty

465 return M.empty

435 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"

466 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"

436inferBinder val b@(UnaryBinder ctor binder) = do

467inferBinder val b@(UnaryBinder ctor binder) = do

437 env <- lift getEnv

468 env <- lift getEnv

438 modulePath <- checkModulePath `fmap` lift get

469 modulePath <- checkModulePath `fmap` lift get

439 case M.lookup (qualify modulePath ctor) (dataConstructors env) of

470 case M.lookup (qualify modulePath ctor) (dataConstructors env) of

440− Just (ForAll idents f@(Function [_] _)) -> do

471+ Just ty -> do

441 obj <- fresh

472 obj <- fresh

442− (Function [ty] ret) <- replaceVarsWithUnknowns idents f

473+ ty `subsumes` (Function [obj] val)

443− m1 <- inferBinder obj binder

474+ inferBinder obj binder

444− val ~~ ret

445− obj ~~ ty

446− return m1

447− Just _ -> throwError $ show ctor ++ " is not a unary constructor"

448 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"

475 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"

449inferBinder val b@(ObjectBinder props) = do

476inferBinder val b@(ObjectBinder props) = do

450 row <- fresh

477 row <- fresh

@@ -564,20 +591,18 @@ checkBlock m mass ret (s:ss) = do

564 (b2, mass2) <- checkBlock m mass1 ret ss

591 (b2, mass2) <- checkBlock m mass1 ret ss

565 return (b2, mass2)

592 return (b2, mass2)

566

593

567−skolemize :: [String] -> Type -> Subst Check Type

594+skolemize :: String -> Type -> Subst Check Type

568−skolemize idents ty = do

595+skolemize ident ty = do

569− sks <- replicateM (length idents) fresh'

596+ tsk <- Skolem <$> fresh'

570− let m = M.fromList (zip idents (map Skolem sks))

597+ rsk <- RSkolem <$> fresh'

571− return $ replaceTypeVars m ty

598+ return $ replaceRowVars (M.singleton ident rsk) $ replaceTypeVars (M.singleton ident tsk) ty

572

599

573check :: M.Map Ident Type -> Value -> Type -> Subst Check ()

600check :: M.Map Ident Type -> Value -> Type -> Subst Check ()

574check m (NumericLiteral _) Number = return ()

601check m (NumericLiteral _) Number = return ()

575check m (StringLiteral _) String = return ()

602check m (StringLiteral _) String = return ()

576check m (BooleanLiteral _) Boolean = return ()

603check m (BooleanLiteral _) Boolean = return ()

577−check m (Unary Negate val) Number = check m val Number

604+check m (Unary op val) ty = checkUnary m op val ty

578−check m (Unary Not val) Boolean = check m val Boolean

605+check m (Binary op left right) ty = checkBinary m op left right ty

579−check m (Unary BitwiseNot val) Number = check m val Number

580−check m (Binary _ t1 t2) Number = check m t1 Number >> check m t2 Number

581check m (ArrayLiteral vals) (Array ty) = forM_ vals (\val -> check m val ty)

606check m (ArrayLiteral vals) (Array ty) = forM_ vals (\val -> check m val ty)

582check m (Indexer index vals) ty = check m index Number >> check m vals (Array ty)

607check m (Indexer index vals) ty = check m index Number >> check m vals (Array ty)

583check m (Abs args ret) (Function argTys retTy) = do

608check m (Abs args ret) (Function argTys retTy) = do

@@ -590,33 +615,112 @@ check m (App f xs) ret = do

590check m val (ForAll idents ty) = do

615check m val (ForAll idents ty) = do

591 sk <- skolemize idents ty

616 sk <- skolemize idents ty

592 check m val sk

617 check m val sk

618+check m v@(Var var@(Qualified mp name)) ty = do

619+ case mp of

620+ ModulePath [] ->

621+ case M.lookup name m of

622+ Just ty1 -> ty1 `subsumes` ty

623+ Nothing -> lookupGlobal

624+ _ -> lookupGlobal

625+ where

626+ lookupGlobal = do

627+ env <- lift getEnv

628+ modulePath <- checkModulePath `fmap` lift get

629+ case M.lookup (qualify modulePath var) (names env) of

630+ Nothing -> throwError $ show var ++ " is undefined"

631+ Just (ty1, _) -> ty1 `subsumes` ty

593check m val u@(TUnknown _) = do

632check m val u@(TUnknown _) = do

594− t <- infer m val

633+ ty <- infer m val

595− t ~~ u

634+ ty ~~ u

635+ return ()

636+check m (TypedValue val ty1) ty2 = do

637+ kind <- lift $ kindOf ty1

638+ guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

639+ ty1 `subsumes` ty2

640+ check m val ty1

641+check m (Case val binders) ret = do

642+ t1 <- infer m val

643+ checkBinders m t1 ret binders

644+check m (IfThenElse cond th el) ty = do

645+ check m cond Boolean

646+ check m th ty

647+ check m el ty

648+check m (ObjectLiteral ps) (Object row) = do

649+ lift $ ensureNoDuplicateProperties ps

650+ checkProperties m ps row False

651+check m (ObjectUpdate obj ps) objTy@(Object row) = do

652+ lift $ ensureNoDuplicateProperties ps

653+ check m obj objTy

654+ checkProperties m ps row True

655+check m (Accessor prop val) ty = do

656+ rest <- fresh

657+ check m val (Object (RCons prop ty rest))

658+check m (Block ss) ret = do

659+ (allCodePathsReturn, _) <- checkBlock m M.empty ret ss

660+ guardWith "Block is missing a return statement" allCodePathsReturn

661+check m (Constructor c) ty = do

662+ env <- lift getEnv

663+ modulePath <- checkModulePath `fmap` lift get

664+ case M.lookup (qualify modulePath c) (dataConstructors env) of

665+ Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"

666+ Just ty1 -> ty1 `subsumes` ty

667+check m val (SaturatedTypeSynonym name args) = do

668+ env <- lift getEnv

669+ modulePath <- checkModulePath `fmap` lift get

670+ case M.lookup (qualify modulePath name) (typeSynonyms env) of

671+ Just (synArgs, body) -> do

672+ let replaced = replaceTypeVars (M.fromList (zip synArgs args)) body

673+ check m val replaced

674+ Nothing -> error "Type synonym was not defined"

596check _ val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty

675check _ val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty

597

676

677+checkProperties :: M.Map Ident Type -> [(String, Value)] -> Row -> Bool -> Subst Check ()

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

679+ go [] [] REmpty = return ()

680+ go [] [] u@(RUnknown _) = u ~~ REmpty

681+ go [] [] (RSkolem _) | lax = return ()

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

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

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

685+ go ((p,v):ps) [] u@(RUnknown _) = do

686+ ty <- infer m v

687+ rest <- fresh

688+ u ~~ RCons p ty rest

689+ go ps [] rest

690+ go ((p,v):ps) ts r =

691+ case lookup p ts of

692+ Nothing -> do

693+ ty <- infer m v

694+ rest <- fresh

695+ r ~~ RCons p ty rest

696+ go ps ts rest

697+ Just ty -> do

698+ check m v ty

699+ go ps (delete (p, ty) ts) r

700+ go _ _ _ = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have type " ++ prettyPrintType (Object row)

701+

598checkFunctionApplication :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()

702checkFunctionApplication :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()

599checkFunctionApplication m (Function argTys retTy) args ret = do

703checkFunctionApplication m (Function argTys retTy) args ret = do

600 guardWith "Incorrect number of function arguments" (length args == length argTys)

704 guardWith "Incorrect number of function arguments" (length args == length argTys)

601 zipWithM (check m) args argTys

705 zipWithM (check m) args argTys

602 ret ~~ retTy

706 ret ~~ retTy

603−checkFunctionApplication m (ForAll idents ty) args ret = do

707+checkFunctionApplication m (ForAll ident ty) args ret = do

604− replaced <- replaceVarsWithUnknowns idents ty

708+ replaced <- replaceVarsWithUnknowns [ident] ty

605 checkFunctionApplication m replaced args ret

709 checkFunctionApplication m replaced args ret

710+checkFunctionApplication m u@(TUnknown _) args ret = do

711+ tyArgs <- replicateM (length args) fresh

712+ u ~~ Function tyArgs ret

606checkFunctionApplication _ fnTy args ret = throwError $ "Cannot apply function of type "

713checkFunctionApplication _ fnTy args ret = throwError $ "Cannot apply function of type "

607 ++ prettyPrintType fnTy

714 ++ prettyPrintType fnTy

608 ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)

715 ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)

609 ++ ". Expecting value of type " ++ prettyPrintType ret ++ "."

716 ++ ". Expecting value of type " ++ prettyPrintType ret ++ "."

610

717

611−{-

718+subsumes :: Type -> Type -> Subst Check ()

612− | Binary BinaryOperator Value Value

719+subsumes (ForAll ident ty1) ty2 = do

613− | ObjectLiteral [(String, Value)]

720+ replaced <- replaceVarsWithUnknowns [ident] ty1

614− | Accessor String Value

721+ replaced `subsumes` ty2

615− | ObjectUpdate Value [(String, Value)]

722+subsumes (Function args1 ret1) (Function args2 ret2) = do

616− | Var (Qualified Ident)

723+ zipWithM subsumes args2 args1

617− | IfThenElse Value Value Value

724+ ret1 `subsumes` ret2

618− | Block [Statement]

725+subsumes ty1 ty2 = ty1 ~~ ty2

619− | Constructor (Qualified ProperName)

726+

620− | Case Value [(Binder, Value)]

621− | TypedValue Value PolyType

622−-}

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

@@ -32,7 +32,7 @@ data Type

32 | TypeConstructor (Qualified ProperName)

33 | TypeApp Type Type

34 | SaturatedTypeSynonym (Qualified ProperName) [Type]

35− | ForAll [String] Type

35+ | ForAll String Type

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

38type PolyType = Type

@@ -41,7 +41,8 @@ data Row

41 = RUnknown (Unknown Row)

42 | RowVar String

43 | REmpty

44+ | RCons String Type Row

44− | RCons String Type Row deriving (Show, Eq, Data, Typeable)

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

46typesToRow :: [(String, Type)] -> Row

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

47typesToRow [] = REmpty

48typesToRow [] = REmpty

@@ -68,3 +69,6 @@ isPolyType (TypeApp t1 t2) = isMonoType t1 && isMonoType t2

68isPolyType (SaturatedTypeSynonym _ args) = all isMonoType args

69isPolyType (SaturatedTypeSynonym _ args) = all isMonoType args

69isPolyType (ForAll idents ty) = isPolyType ty

70isPolyType (ForAll idents ty) = isPolyType ty

70isPolyType _ = True

71isPolyType _ = True

72+

73+mkForAll :: [String] -> Type -> Type

74+mkForAll = flip . foldl . flip $ ForAll