f96c9a1 · rowtype-yoga/purescript-native

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

Work on type synonyms and rank-N types

commitf96c9a14ab69b70da651e9fc21e0972322ea1273 authorPhil Freeman <paf31@cantab.net> dateSun 6 Oct 2013, 15:00 (13 years ago) parent294b01d

21 files changed+303−160

compare with golang

unifiedsplit

PureScript.cabal+8−6

@@ -11,15 +11,16 @@ synopsis: PureScript Programming Language Compiler

1111description: A small compile-to-JS language with extensible records and type-safe blocks

1212author: Phil Freeman <paf31@cantab.net>

1313data-dir: ""

14−

14+

1515library

16− build-depends: base -any, cmdtheline -any, containers -any,

16+ build-depends: base -any, syb -any, cmdtheline -any, containers -any,

1717 mtl -any, parsec -any, utf8-string -any

1818 exposed-modules: PureScript

1919 exposed: True

2020 buildable: True

2121 hs-source-dirs: src

22− other-modules: PureScript.CodeGen.Externs PureScript.CodeGen.JS

22+ other-modules: PureScript.TypeChecker.Synonyms

23+ PureScript.CodeGen.Externs PureScript.CodeGen.JS

2324 PureScript.CodeGen.Common.Gen PureScript.CodeGen.Common Main

2425 PureScript.CodeGen PureScript.Kinds PureScript.Parser

2526 PureScript.TypeChecker PureScript.Types PureScript.Values

@@ -27,13 +28,14 @@ library

2728 PureScript.Parser.Types PureScript.Parser.Values

2829 PureScript.TypeChecker.Kinds PureScript.TypeChecker.Monad

2930 PureScript.TypeChecker.Types

30−

31+

3132executable psc

3233 build-depends: base -any, cmdtheline -any, containers -any,

3334 mtl -any, parsec -any, utf8-string -any

3435 main-is: Main.hs

3536 buildable: True

3637 hs-source-dirs: src

37− other-modules: PureScript.CodeGen.Externs PureScript.CodeGen.JS

38+ other-modules: PureScript.TypeChecker.Synonyms

39+ PureScript.CodeGen.Externs PureScript.CodeGen.JS

3840 PureScript.CodeGen.Common.Gen PureScript.CodeGen.Common

39−

41+

examples/Assign.ps+5−5

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

11test = \ -> {

2− var x = [];

3− for (var i = 0; i < 10; i = i + 1) {

4− x[i] = i;

2+ var x = [];

3+ for (var i = 0; i < 10; i = i + 1) {

4+ x[i] = i;

5+ }

6+ return x;

57 }

6− return x;

7−}

examples/Match.psnew file+3

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

1+data Foo a = Foo

3+foo = \f -> case f of { Foo -> "foo" }

examples/Rank2.psnew file+2

@@ -0,0 +1,2 @@

1+test :: (forall a. (a) -> a) -> Boolean

2+test = \f -> f(f(1) < f(2))

examples/TypeDecl.ps+7−10

@@ -1,17 +1,14 @@

1−id :: (a) -> a

2−

1+id :: forall a. (a) -> a

32id = \x -> x

54k :: (String) -> (Number) -> String

6−

75k = \x -> \y -> x

9−iterate :: (Number) -> ((a) -> a) -> (a) -> a

10−

7+iterate :: forall a. (Number) -> ((a) -> a) -> (a) -> a

118iterate = \n -> \f -> \a -> {

12− var result = a;

13− for (var i = 0; i < n; i = i + 1) {

14− result = f(result);

9+ var result = a;

10+ for (var i = 0; i < n; i = i + 1) {

11+ result = f(result);

12+ }

13+ return result;

1514 }

16− return result;

17−}

examples/TypeSynonyms.psnew file+12

@@ -0,0 +1,12 @@

1+type Monad m =

2+ { ret :: forall a. (a) -> m a

3+ ; bind :: forall a b. (m a) -> ((a) -> m b) -> m b

4+ }

6+data List a = Nil | Cons { head :: a; tail :: List a }

8+replicateM :: forall m a. ((Number, Monad m, m a) -> m (List a))

9+replicateM = \n, m, x -> case n of

10+ { 0 -> (m.ret)(Nil)

11+ ; n -> (m.bind)(x)(\a -> (m.bind)(replicateM(n - 1, m, x))(\as -> (m.ret)(Cons({ head: a, tail: as }))))

12+ }

src/Main.hs+1−1

@@ -43,7 +43,7 @@ compile inputFiles outputFile externsFile = do

4343 Nothing -> U.putStrLn js

4444 case externsFile of

4545 Nothing -> return ()

46− Just filePath -> U.writeFile filePath $ intercalate "\n\n" $ map externToPs $ M.toList $ names env

46+ Just filePath -> U.writeFile filePath $ intercalate "\n" $ map (uncurry externToPs) $ M.toList $ names env

4747 exitSuccess

4848

4949inputFiles :: Term [FilePath]

src/PureScript/CodeGen/Externs.hs+14−3

@@ -26,10 +26,11 @@ import Control.Applicative

2626import PureScript.Values

2727import PureScript.Types

2828import PureScript.Declarations

29+import PureScript.TypeChecker.Monad

2930import PureScript.CodeGen.Common

3031

31−externToPs :: (String, Type) -> String

32−externToPs (name, ty) = "extern " ++ name ++ " :: " ++ typeToPs ty

32+externToPs :: String -> (Type, NameKind) -> String

33+externToPs name (ty, _) = "extern " ++ name ++ " :: " ++ typeToPs ty

3334

3435typeLiterals :: Pattern Type String

3536typeLiterals = Pattern $ A.Kleisli match

@@ -41,6 +42,7 @@ typeLiterals = Pattern $ A.Kleisli match

4142 match (Object row) = Just $ "{ " ++ rowToPs row ++ " }"

4243 match (TypeVar var) = Just var

4344 match (TypeConstructor ctor) = Just ctor

45+ match (TUnknown u) = Just $ show u

4446 match _ = Nothing

4547

4648rowToPs :: Row -> String

@@ -50,6 +52,7 @@ rowToPs = (\(tys, tail) -> intercalate "; " (map (uncurry nameAndTypeToPs) tys)

5052 nameAndTypeToPs name ty = name ++ " :: " ++ typeToPs ty

5153 tailToPs :: Row -> String

5254 tailToPs REmpty = ""

55+ tailToPs (RUnknown u) = show u

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

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

5558 toList (RCons name ty row) = let (tys, rest) = toList row

@@ -68,6 +71,12 @@ function = Pattern $ A.Kleisli match

6871 match (Function args ret) = Just (args, ret)

6972 match _ = Nothing

7073

74+forAll :: Pattern Type ([String], Type)

75+forAll = Pattern $ A.Kleisli match

76+ where

77+ match (ForAll args t) = Just (args, t)

78+ match _ = Nothing

79+

7180typeToPs :: Type -> String

7281typeToPs = fromMaybe (error "Incomplete pattern") . pattern matchType

7382 where

@@ -76,5 +85,7 @@ typeToPs = fromMaybe (error "Incomplete pattern") . pattern matchType

7685 operators :: OperatorTable Type String

7786 operators =

7887 OperatorTable $ [ AssocL typeApp $ \f x -> f ++ " " ++ x

79− , Split function $ \args ret -> "(" ++ intercalate ", " (map typeToPs args) ++ ") -> " ++ typeToPs ret ]

88+ , Split function $ \args ret -> "(" ++ intercalate ", " (map typeToPs args) ++ ") -> " ++ typeToPs ret

89+ , Wrap forAll $ \args t -> "forall " ++ intercalate " " args ++ ". " ++ t

90+ ]

8091

src/PureScript/CodeGen/JS.hs+1−1

@@ -29,7 +29,7 @@ import PureScript.CodeGen.Common.Gen

2929

3030declToJs :: Declaration -> Maybe String

3131declToJs (ValueDeclaration name val) = Just $ "var " ++ name ++ " = " ++ valueToJs val ++ ";"

32−declToJs (DataDeclaration dcs@(DataConstructors { dataConstructors = ctors })) =

32+declToJs (DataDeclaration _ _ ctors) =

3333 Just $ flip concatMap ctors $ \(ctor, maybeTy) ->

3434 case maybeTy of

3535 Nothing -> "var " ++ ctor ++ " = { ctor: '" ++ ctor ++ "' };"

src/PureScript/Declarations.hs+8−10

@@ -12,22 +12,20 @@

1212--

1313-----------------------------------------------------------------------------

1414

15+{-# LANGUAGE DeriveDataTypeable #-}

16+

1517module PureScript.Declarations (

16− Declaration (..),

17− DataConstructors (..)

18+ Declaration (..)

1819) where

1920

2021import PureScript.Values

2122import PureScript.Types

2223

24+import Data.Data

25+

2326data Declaration

24− = DataDeclaration DataConstructors

27+ = DataDeclaration String [String] [(String, Maybe Type)]

28+ | TypeSynonymDeclaration String [String] Type

2529 | TypeDeclaration String Type

2630 | ValueDeclaration String Value

27− | ExternDeclaration String Type deriving Show

28−

29−data DataConstructors = DataConstructors

30− { typeConstructorName :: String

31− , typeArguments :: [String]

32− , dataConstructors :: [(String, Maybe Type)]

33− } deriving Show

31+ | ExternDeclaration String Type deriving (Show, Data, Typeable)

src/PureScript/Kinds.hs+5−1

@@ -12,12 +12,16 @@

1212--

1313-----------------------------------------------------------------------------

1414

15+{-# LANGUAGE DeriveDataTypeable #-}

16+

1517module PureScript.Kinds (

1618 Kind (..)

1719) where

1820

21+import Data.Data

22+

1923data Kind

2024 = KUnknown Int

2125 | Star

2226 | Row

23− | FunKind Kind Kind deriving (Show, Eq)

27+ | FunKind Kind Kind deriving (Show, Eq, Data, Typeable)

src/PureScript/Parser/Common.hs+3−1

@@ -23,6 +23,7 @@ langDef = PL.haskellStyle

2323 { PT.identStart = P.lower <|> P.char '_'

2424 , PT.reservedNames = [ "case"

2525 , "data"

26+ , "type"

2627 , "var"

2728 , "while"

2829 , "for"

@@ -32,7 +33,8 @@ langDef = PL.haskellStyle

3233 , "return"

3334 , "true"

3435 , "false"

35− , "extern" ]

36+ , "extern"

37+ , "forall" ]

3638 }

3739

3840tokenParser = PT.makeTokenParser langDef

src/PureScript/Parser/Declarations.hs+22−3

@@ -19,6 +19,7 @@ module PureScript.Parser.Declarations (

1919

2020import Data.Char

2121import Data.List

22+import Data.Maybe

2223import Data.Function

2324import Control.Applicative

2425import qualified Text.Parsec as P

@@ -38,11 +39,14 @@ parseDataDeclaration = do

3839 tyArgs <- many identifier

3940 lexeme $ P.char '='

4041 ctors <- P.sepBy1 ((,) <$> properName <*> P.optionMaybe parseType) (lexeme $ P.char '|')

41− return $ DataDeclaration $ DataConstructors name tyArgs ctors

42+ return $ DataDeclaration name tyArgs ctors

4243

4344parseTypeDeclaration :: P.Parsec String () Declaration

4445parseTypeDeclaration = TypeDeclaration <$> identifier <*> (lexeme (P.string "::") *> parseType)

4546

47+parseTypeSynonymDeclaration :: P.Parsec String () Declaration

48+parseTypeSynonymDeclaration = TypeSynonymDeclaration <$> (reserved "type" *> properName) <*> many identifier <*> (lexeme (P.char '=') *> parseType)

49+

4650parseValueDeclaration :: P.Parsec String () Declaration

4751parseValueDeclaration = ValueDeclaration <$> identifier <*> (lexeme (P.char '=') *> parseValue)

4852

@@ -53,11 +57,26 @@ parseDeclaration :: P.Parsec String () Declaration

5357parseDeclaration = P.choice $ map P.try

5458 [ parseDataDeclaration

5559 , parseTypeDeclaration

60+ , parseTypeSynonymDeclaration

5661 , parseValueDeclaration

5762 , parseExternDeclaration ]

5863

5964parseDeclarations :: String -> Either P.ParseError [Declaration]

60−parseDeclarations = mapM (P.parse (parseDeclaration <* whiteSpace <* P.eof) "Declaration") . splitFileIntoDeclarations

65+parseDeclarations = fmap catMaybes . mapM (P.parse (whiteSpace *> (P.optionMaybe parseDeclaration <* whiteSpace) <* P.eof) "Declaration") . splitFileIntoDeclarations

66+

67+isIndented :: String -> Bool

68+isIndented = any isSpace . take 1

6169

6270splitFileIntoDeclarations :: String -> [String]

63−splitFileIntoDeclarations = map unlines . filter (not . all isSpace . head) . groupBy ((==) `on` (all isSpace)) . lines

71+splitFileIntoDeclarations = reverse . map (dropWhile isSpace . unlines . reverse) . go [] [] . lines

72+ where

73+ go [] sss [] = sss

74+ go ss sss [] = ss:sss

75+ go ss sss (s:rest)

76+ | all isSpace s = go ss sss rest

77+ | isIndented s = go (s:ss) sss rest

78+ | null ss = go [s] sss rest

79+ | otherwise = go [s] (ss:sss) rest

80+

81+

82+

src/PureScript/Parser/Types.hs+5

@@ -51,6 +51,10 @@ parseTypeVariable = TypeVar <$> identifier

5151parseTypeConstructor :: P.Parsec String () Type

5252parseTypeConstructor = TypeConstructor <$> properName

5353

54+parseForAllType :: P.Parsec String () Type

55+parseForAllType = ForAll <$> (reserved "forall" *> many identifier)

56+ <*> (dot *> parseType)

57+

5458parseTypeAtom :: P.Parsec String () Type

5559parseTypeAtom = P.choice $ map P.try

5660 [ parseNumber

@@ -59,6 +63,7 @@ parseTypeAtom = P.choice $ map P.try

5963 , parseArray

6064 , parseObject

6165 , parseFunction

66+ , parseForAllType

6267 , parseTypeVariable

6368 , parseTypeConstructor

6469 , parens parseType ]

src/PureScript/TypeChecker.hs+18−10

@@ -24,6 +24,7 @@ module PureScript.TypeChecker (

2424import PureScript.TypeChecker.Monad

2525import PureScript.TypeChecker.Kinds

2626import PureScript.TypeChecker.Types

27+import PureScript.TypeChecker.Synonyms

2728

2829import Data.List

2930import Data.Maybe

@@ -41,23 +42,28 @@ import qualified Data.Map as M

4142

4243typeCheckAll :: [Declaration] -> Check ()

4344typeCheckAll [] = return ()

44−typeCheckAll (DataDeclaration dcs@(DataConstructors

45− { typeConstructorName = name

46− , typeArguments = args

47− , dataConstructors = ctors

48− }) : rest) = do

45+typeCheckAll (DataDeclaration name args ctors : rest) = do

4946 rethrow (("Error in type constructor " ++ name ++ ": ") ++) $ do

5047 env <- getEnv

5148 guardWith (name ++ " is already defined") $ not $ M.member name (types env)

52− ctorKind <- kindsOf name args (catMaybes $ map snd ctors)

53− putEnv $ env { types = M.insert name ctorKind (types env) }

49+ ctorKind <- kindsOf (Just name) args (catMaybes $ map snd ctors)

50+ putEnv $ env { types = M.insert name (ctorKind, Data) (types env) }

5451 flip mapM_ ctors $ \(dctor, maybeTy) ->

5552 rethrow (("Error in data constructor " ++ name ++ ": ") ++) $ do

5653 env' <- getEnv

5754 guardWith (dctor ++ " is already defined") $ not $ flip M.member (names env') dctor

5855 let retTy = foldl TypeApp (TypeConstructor name) (map TypeVar args)

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

60− putEnv $ env' { names = M.insert dctor dctorTy (names env') }

57+ let quantified = ForAll args dctorTy

58+ putEnv $ env' { names = M.insert dctor (quantified, DataConstructor) (names env') }

59+ typeCheckAll rest

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

61+ rethrow (("Error in type synonym " ++ name ++ ": ") ++) $ do

62+ env <- getEnv

63+ guardWith (name ++ " is already defined") $ not $ M.member name (types env)

64+ kind <- kindsOf (Just name) args [ty]

65+ putEnv $ env { types = M.insert name (kind, TypeSynonym) (types env)

66+ , typeSynonyms = M.insert name (args, ty) (typeSynonyms env) }

6167 typeCheckAll rest

6268typeCheckAll (TypeDeclaration name ty : ValueDeclaration name' val : rest) | name == name' =

6369 typeCheckAll (ValueDeclaration name (TypedValue val ty) : rest)

@@ -69,12 +75,14 @@ typeCheckAll (ValueDeclaration name val : rest) = do

6975 Just ty -> throwError $ name ++ " is already defined"

7076 Nothing -> do

7177 ty <- typeOf name val

72− putEnv (env { names = M.insert name ty (names env) })

78+ putEnv (env { names = M.insert name (ty, Value) (names env) })

7379 typeCheckAll rest

7480typeCheckAll (ExternDeclaration name ty : rest) = do

7581 rethrow (("Error in extern declaration " ++ name ++ ": ") ++) $ do

7682 env <- getEnv

83+ kind <- kindOf ty

84+ guardWith "Expected kind *" $ kind == Star

7785 case M.lookup name (names env) of

7886 Just _ -> throwError $ name ++ " is already defined"

79− Nothing -> putEnv (env { names = M.insert name ty (names env) })

87+ Nothing -> putEnv (env { names = M.insert name (ty, Extern) (names env) })

8088 typeCheckAll rest

src/PureScript/TypeChecker/Kinds.hs+18−8

@@ -15,10 +15,12 @@

1515module PureScript.TypeChecker.Kinds (

1616 KindConstraint(..),

1717 KindSolution(..),

18− kindsOf

18+ kindsOf,

19+ kindOf

1920) where

2021

2122import Data.List

23+import Data.Maybe (fromMaybe)

2224import Data.Function

2325

2426import PureScript.Types

@@ -45,11 +47,17 @@ newtype KindSolution = KindSolution { runKindSolution :: Int -> Kind }

4547emptyKindSolution :: KindSolution

4648emptyKindSolution = KindSolution KUnknown

4749

48−kindsOf :: String -> [String] -> [Type] -> Check Kind

50+kindOf :: Type -> Check Kind

51+kindOf ty = do

52+ (cs, n, m) <- kindConstraints M.empty ty

53+ solution <- solveKindConstraints cs emptyKindSolution

54+ return $ starIfUnknown $ runKindSolution solution n

55+

56+kindsOf :: Maybe String -> [String] -> [Type] -> Check Kind

4957kindsOf name args ts = do

5058 tyCon <- fresh

5159 nargs <- replicateM (length args) fresh

52− (cs, ns, m) <- kindConstraintsAll (M.insert name tyCon $ M.fromList (zipWith (,) args nargs)) ts

60+ (cs, ns, m) <- kindConstraintsAll (maybe id (flip M.insert tyCon) name $ M.fromList (zipWith (,) args nargs)) ts

5361 let extraConstraints = KindConstraint tyCon (foldr FunKind Star (map KUnknown nargs)) : map (flip KindConstraint Star) ns

5462 solution <- solveKindConstraints (extraConstraints ++ cs) emptyKindSolution

5563 return $ starIfUnknown $ runKindSolution solution tyCon

@@ -81,17 +89,16 @@ kindConstraints m (Function args ret) = do

8189 (cs', retN, m'') <- kindConstraints m' ret

8290 return ((KindConstraint retN Star) : (KindConstraint me Star) : (map (flip KindConstraint Star) ns) ++ cs, me, m'')

8391kindConstraints m (TypeVar v) = do

84− me <- case M.lookup v m of

85− Just u -> return u

86− Nothing -> fresh

87− return ([], me, M.insert v me m)

92+ case M.lookup v m of

93+ Just u -> return ([], u, m)

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

8895kindConstraints m (TypeConstructor v) = do

8996 env <- getEnv

9097 me <- fresh

9198 case M.lookup v m of

9299 Nothing -> case M.lookup v (types env) of

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

94− Just kind -> return ([KindConstraint me kind], me, m)

101+ Just (kind, _) -> return ([KindConstraint me kind], me, m)

95102 Just u -> do

96103 return ([KindConstraint me (KUnknown u)], me, m)

97104kindConstraints m (TypeApp t1 t2) = do

@@ -99,6 +106,9 @@ kindConstraints m (TypeApp t1 t2) = do

99106 (cs1, n1, m1) <- kindConstraints m t1

100107 (cs2, n2, m2) <- kindConstraints m1 t2

101108 return ((KindConstraint n1 (FunKind (KUnknown n2) (KUnknown me))) : cs1 ++ cs2, me, m2)

109+kindConstraints m (ForAll idents ty) = do

110+ ns <- replicateM (length idents) fresh

111+ kindConstraints (m `M.union` M.fromList (zip idents ns)) ty

102112kindConstraints m _ = do

103113 me <- fresh

104114 return ([KindConstraint me Star], me, m)

src/PureScript/TypeChecker/Monad.hs+9−4

@@ -27,13 +27,18 @@ import Control.Arrow ((***))

2727

2828import qualified Data.Map as M

2929

30+data NameKind = Value | DataConstructor | Extern deriving Show

31+

32+data TypeDeclarationKind = Data | TypeSynonym deriving Show

33+

3034data Environment = Environment

31− { names :: M.Map String Type

32− , types :: M.Map String Kind

33− } deriving (Show)

35+ { names :: M.Map String (Type, NameKind)

36+ , types :: M.Map String (Kind, TypeDeclarationKind)

37+ , typeSynonyms :: M.Map String ([String], Type)

38+ }

3439

3540emptyEnvironment :: Environment

36−emptyEnvironment = Environment M.empty M.empty

41+emptyEnvironment = Environment M.empty M.empty M.empty

3742

3843newtype Check a = Check { unCheck :: StateT (Environment, Int) (Either String) a } deriving (Functor, Monad, Applicative, MonadPlus, MonadState (Environment, Int), MonadError String)

3944

src/PureScript/TypeChecker/Synonyms.hsnew file+58

@@ -0,0 +1,58 @@

1+-----------------------------------------------------------------------------

2+--

3+-- Module : PureScript.TypeChecker.Synonyms

4+-- Copyright : (c) Phil Freeman 2013

5+-- License : MIT

6+--

7+-- Maintainer : Phil Freeman <paf31@cantab.net>

8+-- Stability : experimental

9+-- Portability :

10+--

11+-- |

12+--

13+-----------------------------------------------------------------------------

14+

15+{-# LANGUAGE Rank2Types #-}

16+

17+module PureScript.TypeChecker.Synonyms (

18+ substituteTypeSynonym

19+) where

20+

21+import PureScript.Types

22+import PureScript.Declarations

23+

24+import Data.Maybe (fromMaybe)

25+import Data.Data

26+import Data.Generics

27+import Control.Arrow

28+import Control.Monad.Writer

29+import Control.Monad.Error

30+import qualified Data.Map as M

31+

32+replaceTypeVars :: M.Map String Type -> Type -> Type

33+replaceTypeVars m = everywhere (mkT replace)

34+ where

35+ replace :: Type -> Type

36+ replace t@(TypeVar var) = fromMaybe t (M.lookup var m)

37+ replace t = t

38+

39+buildTypeSubstitution :: String -> Type -> [String] -> Type -> WriterT Any (Either String) (Maybe Type)

40+buildTypeSubstitution name ty args = go (reverse args) M.empty

41+ where

42+ go :: [String] -> M.Map String Type -> Type -> WriterT Any (Either String) (Maybe Type)

43+ go [] m (TypeConstructor ctor) | name == ctor = tell (Any True) >> return (Just $ replaceTypeVars m ty)

44+ go (_:_) _ (TypeConstructor ctor) | name == ctor = lift . throwError $ "Partially applied type synonym " ++ name

45+ go (arg:args) m (TypeApp f x) = go args (M.insert arg x m) f

46+ go _ _ _ = return Nothing

47+

48+everywhereButM' :: (Monad m, Data d) => (forall d. (Data d) => d -> WriterT Any m d) -> d -> m d

49+everywhereButM' f x = do

50+ (y, halt) <- runWriterT $ f x

51+ case getAny halt of

52+ True -> return y

53+ _ -> gmapM (everywhereButM' f) y

54+

55+substituteTypeSynonym :: String -> [String] -> Type -> Type -> Either String Type

56+substituteTypeSynonym name args ty = everywhereButM' (mkM replace)

57+ where

58+ replace t = fmap (fromMaybe t) $ buildTypeSubstitution name ty args t

src/PureScript/TypeChecker/Types.hs+89−87

@@ -20,10 +20,15 @@ module PureScript.TypeChecker.Types (

2020

2121import Data.List

2222import Data.Function

23+import Data.Data (Data(..))

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

2325

2426import PureScript.Values

2527import PureScript.Types

28+import PureScript.Kinds

2629import PureScript.TypeChecker.Monad

30+import PureScript.TypeChecker.Kinds

31+import PureScript.TypeChecker.Synonyms

2732

2833import Control.Monad.State

2934import Control.Monad.Error

@@ -51,10 +56,14 @@ typeOf name val = do

5156 return $ varIfUnknown $ fst (runTypeSolution solution) n

5257

5358varIfUnknown :: Type -> Type

54−varIfUnknown = flip evalState M.empty . varIfUnknown'

59+varIfUnknown ty =

60+ let

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

62+ in

63+ ForAll (sort $ nub $ M.elems m) ty'

5564 where

56− varIfUnknown' :: Type -> State (M.Map Int String) Type

57− varIfUnknown' (TUnknown n) = do

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

66+ f (TUnknown n) = do

5867 m <- get

5968 case M.lookup n m of

6069 Nothing -> do

@@ -62,13 +71,9 @@ varIfUnknown = flip evalState M.empty . varIfUnknown'

6271 put $ M.insert n name m

6372 return $ TypeVar name

6473 Just name -> return $ TypeVar name

65− varIfUnknown' (Array t) = Array <$> varIfUnknown' t

66− varIfUnknown' (Object row) = Object <$> varIfUnknown'' row

67− varIfUnknown' (Function args ret) = Function <$> mapM varIfUnknown' args <*> varIfUnknown' ret

68− varIfUnknown' (TypeApp t1 t2) = TypeApp <$> varIfUnknown' t1 <*> varIfUnknown' t2

69− varIfUnknown' t = return t

70− varIfUnknown'' :: Row -> State (M.Map Int String) Row

71− varIfUnknown'' (RUnknown n) = do

74+ f t = return t

75+ g :: Row -> State (M.Map Int String) Row

76+ g (RUnknown n) = do

7277 m <- get

7378 case M.lookup n m of

7479 Nothing -> do

@@ -76,18 +81,13 @@ varIfUnknown = flip evalState M.empty . varIfUnknown'

7681 put $ M.insert n name m

7782 return $ RowVar name

7883 Just name -> return $ RowVar name

79− varIfUnknown'' (RCons name ty row) = RCons name ty <$> varIfUnknown'' row

80− varIfUnknown'' r = return r

84+ g r = return r

8185

82−replaceVarsWithUnknowns :: Type -> Check Type

83−replaceVarsWithUnknowns = flip evalStateT M.empty . replaceVarsWithUnknowns'

86+replaceVarsWithUnknowns :: [String] -> Type -> Check Type

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

8488 where

85− replaceVarsWithUnknowns' :: Type -> StateT (M.Map String Int) Check Type

86− replaceVarsWithUnknowns' (Array t) = Array <$> replaceVarsWithUnknowns' t

87− replaceVarsWithUnknowns' (Object row) = Object <$> replaceVarsWithUnknowns'' row

88− replaceVarsWithUnknowns' (Function args ret) = Function <$> mapM replaceVarsWithUnknowns' args <*> replaceVarsWithUnknowns' ret

89− replaceVarsWithUnknowns' (TypeApp t1 t2) = TypeApp <$> replaceVarsWithUnknowns' t1 <*> replaceVarsWithUnknowns' t2

90− replaceVarsWithUnknowns' (TypeVar var) = do

89+ f :: Type -> StateT (M.Map String Int) Check Type

90+ f (TypeVar var) | var `elem` idents = do

9191 m <- get

9292 n <- lift fresh

9393 case M.lookup var m of

@@ -95,9 +95,9 @@ replaceVarsWithUnknowns = flip evalStateT M.empty . replaceVarsWithUnknowns'

9595 put (M.insert var n m)

9696 return $ TUnknown n

9797 Just u -> return $ TUnknown u

98− replaceVarsWithUnknowns' t = return t

99− replaceVarsWithUnknowns'' :: Row -> StateT (M.Map String Int) Check Row

100− replaceVarsWithUnknowns'' (RowVar var) = do

98+ f t = return t

99+ g :: Row -> StateT (M.Map String Int) Check Row

100+ g (RowVar var) | var `elem` idents = do

101101 m <- get

102102 n <- lift fresh

103103 case M.lookup var m of

@@ -105,8 +105,35 @@ replaceVarsWithUnknowns = flip evalStateT M.empty . replaceVarsWithUnknowns'

105105 put (M.insert var n m)

106106 return $ RUnknown n

107107 Just u -> return $ RUnknown u

108− replaceVarsWithUnknowns'' (RCons name ty row) = RCons name <$> replaceVarsWithUnknowns' ty <*> replaceVarsWithUnknowns'' row

109− replaceVarsWithUnknowns'' r = return r

108+ g r = return r

109+

110+replaceType :: (Data d) => Int -> Type -> d -> d

111+replaceType n t = everywhere (mkT go)

112+ where

113+ go (TUnknown m) | m == n = t

114+ go t = t

115+

116+replaceRow :: (Data d) => Int -> Row -> d -> d

117+replaceRow n r = everywhere (mkT go)

118+ where

119+ go (RUnknown m) | m == n = r

120+ go r = r

121+

122+typeOccursCheck :: Int -> Type -> Check ()

123+typeOccursCheck u (TUnknown _) = return ()

124+typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ show t

125+

126+rowOccursCheck :: Int -> Row -> Check ()

127+rowOccursCheck u (RUnknown _) = return ()

128+rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ show r

129+

130+occursCheck :: (Data d) => Int -> d -> Bool

131+occursCheck u = everything (||) $ flip extQ g $ mkQ False f

132+ where

133+ f (TUnknown u') | u' == u = True

134+ f _ = False

135+ g (RUnknown u') | u' == u = True

136+ g _ = False

110137

111138typeConstraints :: M.Map String Int -> Value -> Check ([TypeConstraint], Int)

112139typeConstraints _ (NumericLiteral _) = do

@@ -169,10 +196,9 @@ typeConstraints m (Var var) =

169196 env <- getEnv

170197 case M.lookup var (names env) of

171198 Nothing -> throwError $ var ++ " is undefined"

172− Just ty -> do

199+ Just (ty, _) -> do

173200 me <- fresh

174− replaced <- replaceVarsWithUnknowns ty

175− return ([TypeConstraint me replaced], me)

201+ return ([TypeConstraint me ty], me)

176202 Just u -> do

177203 me <- fresh

178204 return ([TypeConstraint u (TUnknown me)], me)

@@ -185,19 +211,30 @@ typeConstraints m (Constructor c) = do

185211 env <- getEnv

186212 case M.lookup c (names env) of

187213 Nothing -> throwError $ c ++ " is undefined"

188− Just ty -> do

214+ Just (ty, _) -> do

189215 me <- fresh

190− replaced <- replaceVarsWithUnknowns ty

191− return ([TypeConstraint me replaced], me)

216+ return ([TypeConstraint me ty], me)

192217typeConstraints m (Case val binders) = do

193218 (cs1, n1) <- typeConstraints m val

194219 ret <- fresh

195220 cs2 <- typeConstraintsForBinders m n1 ret binders

196221 return (cs1 ++ cs2, ret)

197222typeConstraints m (TypedValue val ty) = do

223+ kind <- kindOf ty

224+ guardWith ("Expected type of kind *, was " ++ show kind) $ kind == Star

225+ ty' <- replaceAllTypeSynonyms ty

198226 (cs, n1) <- typeConstraints m val

199− return (TypeConstraint n1 ty : cs, n1)

200− -- TODO: Kind-check the type

227+ return (TypeConstraint n1 ty' : cs, n1)

228+

229+replaceAllTypeSynonyms :: Type -> Check Type

230+replaceAllTypeSynonyms ty = do

231+ env <- getEnv

232+ go (M.toList $ typeSynonyms env) ty

233+ where

234+ go [] ty = return ty

235+ go ((name, (args, repl)):rest) ty = do

236+ ty' <- either throwError return (substituteTypeSynonym name args repl ty)

237+ go rest ty'

201238

202239unaryOperatorConstraints :: UnaryOperator -> Int -> Int -> [TypeConstraint]

203240unaryOperatorConstraints Negate val result = [TypeConstraint val Number, TypeConstraint result Number]

@@ -245,18 +282,18 @@ typeConstraintsForBinder val (VarBinder name) = do

245282typeConstraintsForBinder val (NullaryBinder ctor) = do

246283 env <- getEnv

247284 case M.lookup ctor (names env) of

248− Just ret -> do

249− ret' <- replaceVarsWithUnknowns ret

285+ Just (ForAll args ret, DataConstructor) -> do

286+ ret' <- replaceVarsWithUnknowns args ret

250287 return ([TypeConstraint val ret'], M.empty)

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

252289typeConstraintsForBinder val (UnaryBinder ctor binder) = do

253290 env <- getEnv

254291 case M.lookup ctor (names env) of

255− Just f@(Function [ty] ret) -> do

292+ Just (ForAll args f@(Function [_] _), DataConstructor) -> do

256293 obj <- fresh

257− Function [ty'] ret' <- replaceVarsWithUnknowns f

294+ (Function [ty] ret) <- replaceVarsWithUnknowns args f

258295 (cs, m1) <- typeConstraintsForBinder obj binder

259− return ((TypeConstraint val ret') : (TypeConstraint obj ty') : cs, m1)

296+ return ((TypeConstraint val ret) : (TypeConstraint obj ty) : cs, m1)

260297 Just _ -> throwError $ ctor ++ " is not a unary constructor"

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

262299typeConstraintsForBinder val (ObjectBinder props) = do

@@ -361,64 +398,42 @@ typeConstraintsForBlock m mass ret (s:ss) = do

361398solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution

362399solveTypeConstraints [] s = return s

363400solveTypeConstraints all@(TypeConstraint n t:cs) s = do

364− guardWith "Occurs check failed" $ not $ typeOccursCheck False n t

401+ typeOccursCheck n t

365402 let s' = let (f, g) = runTypeSolution s

366− in TypeSolution (replaceTypeInType n t . f, replaceTypeInRow n t . g)

403+ in TypeSolution (replaceType n t . f, replaceType n t . g)

367404 cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs

368405 solveTypeConstraints cs' s'

369406solveTypeConstraints (RowConstraint n r:cs) s = do

370− guardWith "Occurs check failed" $ not $ rowOccursCheck False n r

407+ rowOccursCheck n r

371408 let s' = let (f, g) = runTypeSolution s

372− in TypeSolution $ (replaceRowInType n r . f, replaceRowInRow n r . g)

409+ in TypeSolution $ (replaceRow n r . f, replaceRow n r . g)

373410 cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs

374411 solveTypeConstraints cs' s'

375412

376413substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]

377414substituteTypeInConstraint n s (TypeConstraint m t)

378415 | n == m = unifyTypes s t

379− | otherwise = return [TypeConstraint m (replaceTypeInType n s t)]

416+ | otherwise = return [TypeConstraint m (replaceType n s t)]

380417substituteTypeInConstraint n s (RowConstraint m r)

381− = return [RowConstraint m (replaceTypeInRow n s r)]

418+ = return [RowConstraint m (replaceType n s r)]

382419

383420substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]

384421substituteRowInConstraint n r (TypeConstraint m t)

385− = return [TypeConstraint m (replaceRowInType n r t)]

422+ = return [TypeConstraint m (replaceRow n r t)]

386423substituteRowInConstraint n r (RowConstraint m r1)

387424 | m == n = unifyRows r r1

388− | otherwise = return [RowConstraint m (replaceRowInRow n r r1)]

389−

390−replaceTypeInType :: Int -> Type -> Type -> Type

391−replaceTypeInType n t (TUnknown m) | m == n = t

392−replaceTypeInType n t (Array t1) = Array $ replaceTypeInType n t t1

393−replaceTypeInType n t (Object row) = Object $ replaceTypeInRow n t row

394−replaceTypeInType n t (Function args ret) = Function (map (replaceTypeInType n t) args) (replaceTypeInType n t ret)

395−replaceTypeInType n t (TypeApp t1 t2) = TypeApp (replaceTypeInType n t t1) (replaceTypeInType n t t2)

396−replaceTypeInType _ _ other = other

397−

398−replaceTypeInRow :: Int -> Type -> Row -> Row

399−replaceTypeInRow n t (RCons name ty row) = RCons name (replaceTypeInType n t ty) (replaceTypeInRow n t row)

400−replaceTypeInRow n t other = other

401−

402−replaceRowInType :: Int -> Row -> Type -> Type

403−replaceRowInType n r (Array t1) = Array $ replaceRowInType n r t1

404−replaceRowInType n r (Object row) = Object $ replaceRowInRow n r row

405−replaceRowInType n r (Function args ret) = Function (map (replaceRowInType n r) args) (replaceRowInType n r ret)

406−replaceRowInType n r (TypeApp t1 t2) = TypeApp (replaceRowInType n r t1) (replaceRowInType n r t2)

407−replaceRowInType _ _ other = other

408−

409−replaceRowInRow :: Int -> Row -> Row -> Row

410−replaceRowInRow n r (RUnknown m) | m == n = r

411−replaceRowInRow n r (RCons name ty row) = RCons name (replaceRowInType n r ty) (replaceRowInRow n r row)

412−replaceRowInRow _ _ other = other

425+ | otherwise = return [RowConstraint m (replaceRow n r r1)]

413426

414427unifyTypes :: Type -> Type -> Check [TypeConstraint]

415428unifyTypes (TUnknown u1) (TUnknown u2) | u1 == u2 = return []

416429unifyTypes (TUnknown u) t = do

417− guardWith "Occurs check failed" $ not $ typeOccursCheck False u t

430+ typeOccursCheck u t

418431 return [TypeConstraint u t]

419432unifyTypes t (TUnknown u) = do

420− guardWith "Occurs check failed" $ not $ typeOccursCheck False u t

433+ typeOccursCheck u t

421434 return [TypeConstraint u t]

435+unifyTypes (ForAll idents t1) t2 = join $ flip unifyTypes t2 <$> replaceVarsWithUnknowns idents t1

436+unifyTypes t1 (ForAll idents t2) = join $ unifyTypes t1 <$> replaceVarsWithUnknowns idents t2

422437unifyTypes Number Number = return []

423438unifyTypes String String = return []

424439unifyTypes Boolean Boolean = return []

@@ -446,14 +461,14 @@ unifyRows r1 r2 =

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

447462 sd1 = [ (name, t1) | (name, t1) <- s1, not (elem name (map fst s2)) ]

448463 sd2 = [ (name, t2) | (name, t2) <- s2, not (elem name (map fst s1)) ]

449− in rethrow (const $ "Cannot unify " ++ show r1 ++ " with " ++ show r2) $ do

464+ in rethrow (\e -> "Cannot unify " ++ show r1 ++ " with " ++ show r2 ++ ": " ++ e) $ do

450465 cs1 <- fmap concat $ mapM (uncurry unifyTypes) int

451466 cs2 <- unifyRows' sd1 r1' sd2 r2'

452467 return $ cs1 ++ cs2

453468 where

454469 unifyRows' :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]

455470 unifyRows' [] (RUnknown u) sd r = do

456− guardWith "Occurs check failed" $ not $ rowOccursCheck False u r

471+ rowOccursCheck u r

457472 return [RowConstraint u (fromList (sd, r))]

458473 unifyRows' ((name, ty):row) r others (RUnknown u) = do

459474 u' <- fresh

@@ -468,16 +483,3 @@ unifyRows r1 r2 =

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

469484 fromList ([], r) = r

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

471−

472−typeOccursCheck :: Bool -> Int -> Type -> Bool

473−typeOccursCheck b u (TUnknown u') | u == u' = b

474−typeOccursCheck _ u (Array t) = typeOccursCheck True u t

475−typeOccursCheck _ u (Object row) = rowOccursCheck True u row

476−typeOccursCheck _ u (Function args ret) = any (typeOccursCheck True u) args || typeOccursCheck True u ret

477−typeOccursCheck _ u (TypeApp s t) = typeOccursCheck True u s || typeOccursCheck True u t

478−typeOccursCheck _ _ _ = False

479−

480−rowOccursCheck :: Bool -> Int -> Row -> Bool

481−rowOccursCheck b u (RUnknown u') | u == u' = b

482−rowOccursCheck _ u (RCons name ty row) = typeOccursCheck True u ty || rowOccursCheck True u row

483−rowOccursCheck _ _ _ = False

src/PureScript/Types.hs+5−4

@@ -12,14 +12,14 @@

1212--

1313-----------------------------------------------------------------------------

1414

15−{-# LANGUAGE DeriveFunctor #-}

15+{-# LANGUAGE DeriveDataTypeable #-}

1616

1717module PureScript.Types (

1818 Type (..),

1919 Row(..)

2020) where

2121

22−import Data.List (intercalate)

22+import Data.Data

2323

2424data Type

2525 = TUnknown Int

@@ -31,10 +31,11 @@ data Type

3131 | Function [Type] Type

3232 | TypeVar String

3333 | TypeConstructor String

34− | TypeApp Type Type deriving Show

34+ | TypeApp Type Type

35+ | ForAll [String] Type deriving (Show, Data, Typeable)

3536

3637data Row

3738 = RUnknown Int

3839 | RowVar String

3940 | REmpty

40− | RCons String Type Row deriving Show

41+ | RCons String Type Row deriving (Show, Data, Typeable)

src/PureScript/Values.hs+10−6

@@ -12,6 +12,8 @@

1212--

1313-----------------------------------------------------------------------------

1414

15+{-# LANGUAGE DeriveDataTypeable #-}

16+

1517module PureScript.Values (

1618 UnaryOperator (..),

1719 BinaryOperator (..),

@@ -23,10 +25,12 @@ module PureScript.Values (

2325

2426import PureScript.Types

2527

28+import Data.Data

29+

2630data UnaryOperator

2731 = Negate

2832 | Not

29− | BitwiseNot deriving (Show, Eq)

33+ | BitwiseNot deriving (Show, Eq, Data, Typeable)

3034

3135data BinaryOperator

3236 = Add

@@ -48,7 +52,7 @@ data BinaryOperator

4852 | ShiftLeft

4953 | ShiftRight

5054 | ZeroFillShiftRight

51− | Concat deriving (Show, Eq)

55+ | Concat deriving (Show, Eq, Data, Typeable)

5256

5357data Value

5458 = NumericLiteral (Either Integer Double)

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

6670 | Block [Statement]

6771 | Constructor String

6872 | Case Value [(Binder, Value)]

69− | TypedValue Value Type deriving Show

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

7074

7175data Statement

7276 = VariableIntroduction String Value

@@ -74,7 +78,7 @@ data Statement

7478 | While Value [Statement]

7579 | For (Statement, Value, Statement) [Statement]

7680 | IfThenElse (Value) [Statement] (Maybe [Statement])

77− | Return Value deriving Show

81+ | Return Value deriving (Show, Data, Typeable)

7882

7983data Binder

8084 = BooleanBinder Bool

@@ -84,9 +88,9 @@ data Binder

8488 | NullaryBinder String

8589 | UnaryBinder String Binder

8690 | ObjectBinder [(String, Binder)]

87− | ArrayBinder [Binder] (Maybe Binder) deriving Show

91+ | ArrayBinder [Binder] (Maybe Binder) deriving (Show, Data, Typeable)

8892

8993data AssignmentTarget

9094 = AssignVariable String

9195 | AssignObjectProperty String AssignmentTarget

92− | AssignArrayIndex Value AssignmentTarget deriving Show

96+ | AssignArrayIndex Value AssignmentTarget deriving (Show, Data, Typeable)