@@ -1,622 +0,0 @@
1−-----------------------------------------------------------------------------
3−-- Module : Language.PureScript.TypeChecker.Types
4−-- Copyright : (c) Phil Freeman 2013
7−-- Maintainer : Phil Freeman <paf31@cantab.net>
8−-- Stability : experimental
13−-----------------------------------------------------------------------------
15−{-# LANGUAGE DeriveDataTypeable #-}
17−module Language.PureScript.TypeChecker.Types (
25−import qualified Data.Data as D
26−import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)
28−import Language.PureScript.Values
29−import Language.PureScript.Types
30−import Language.PureScript.Kinds
31−import Language.PureScript.Names
32−import Language.PureScript.TypeChecker.Monad
33−import Language.PureScript.TypeChecker.Kinds
34−import Language.PureScript.TypeChecker.Synonyms
35−import Language.PureScript.Pretty
36−import Language.PureScript.Unknown
38−import Control.Monad.State
39−import Control.Monad.Error
41−import Control.Applicative
42−import Control.Arrow (Arrow(..), Kleisli(..), (***), (&&&), second)
43−import qualified Control.Category as C
45−import qualified Data.Map as M
47−instance Unifiable Type where
49− isUnknown (TUnknown u) = Just u
50− isUnknown _ = Nothing
51− TUnknown u1 ~~ TUnknown u2 | u1 == u2 = return ()
52− TUnknown u ~~ t = replace u t
53− t ~~ TUnknown u = replace u t
54− SaturatedTypeSynonym name1 args1 ~~ SaturatedTypeSynonym name2 args2 | name1 == name2 =
55− zipWithM_ (~~) args1 args2
56− SaturatedTypeSynonym name args ~~ ty = do
58− modulePath <- checkModulePath `fmap` lift get
59− case M.lookup (qualify modulePath name) (typeSynonyms env) of
60− Just (synArgs, body) -> do
61− let m = M.fromList $ zip synArgs args
62− let replaced = replaceTypeVars m body
64− Nothing -> error "Type synonym was not defined"
65− ty ~~ s@(SaturatedTypeSynonym _ _) = s ~~ ty
66− ForAll idents ty1 ~~ ty2 = do
67− sk <- skolemize idents ty1
69− ty ~~ f@(ForAll _ _) = f ~~ ty
70− Number ~~ Number = return ()
71− String ~~ String = return ()
72− Boolean ~~ Boolean = return ()
73− Array s ~~ Array t = s ~~ t
74− Object row1 ~~ Object row2 = row1 ~~ row2
75− Function args1 ret1 ~~ Function args2 ret2 = do
76− guardWith "Function applied to incorrect number of args" $ length args1 == length args2
77− zipWithM_ (~~) args1 args2
79− TypeVar v1 ~~ TypeVar v2 | v1 == v2 = return ()
80− TypeConstructor c1 ~~ TypeConstructor c2 = do
81− modulePath <- checkModulePath `fmap` lift get
82− guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (qualify modulePath c1 == qualify modulePath c2)
83− TypeApp t1 t2 ~~ TypeApp t3 t4 = do
86− Skolem s1 ~~ Skolem s2 | s1 == s2 = return ()
87− t1 ~~ t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
88− apply s (TUnknown u) = runSubstitution s u
89− apply s (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name $ map (apply s) tys
90− apply s (ForAll idents ty) = ForAll idents $ apply s ty
91− apply s (Array t) = Array (apply s t)
92− apply s (Object r) = Object (apply s r)
93− apply s (Function args ret) = Function (map (apply s) args) (apply s ret)
94− apply s (TypeApp t1 t2) = TypeApp (apply s t1) (apply s t2)
96− unknowns (TUnknown (Unknown u)) = [u]
97− unknowns (SaturatedTypeSynonym _ tys) = concatMap unknowns tys
98− unknowns (ForAll idents ty) = unknowns ty
99− unknowns (Array t) = unknowns t
100− unknowns (Object r) = unknowns r
101− unknowns (Function args ret) = concatMap unknowns args ++ unknowns ret
102− unknowns (TypeApp t1 t2) = unknowns t1 ++ unknowns t2
105−instance Unifiable Row where
107− isUnknown (RUnknown u) = Just u
108− isUnknown _ = Nothing
111− (s1, r1') = rowToList r1
112− (s2, r2') = rowToList r2
113− int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
114− sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
115− sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
117− forM_ int (uncurry (~~))
118− unifyRows sd1 r1' sd2 r2'
120− unifyRows :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Subst Check ()
121− unifyRows [] (RUnknown u) sd r = replace u (rowFromList (sd, r))
122− unifyRows sd r [] (RUnknown u) = replace u (rowFromList (sd, r))
123− unifyRows ns@((name, ty):row) r others u@(RUnknown un) = do
125− forM row $ \(_, ty) -> occursCheck un ty
127− u ~~ RCons name ty u'
128− unifyRows row r others u'
129− unifyRows [] REmpty [] REmpty = return ()
130− unifyRows [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return ()
131− 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
133− apply s (RCons name ty r) = RCons name (apply s ty) (apply s r)
135− unknowns (RUnknown (Unknown u)) = [u]
136− unknowns (RCons _ ty r) = unknowns ty ++ unknowns r
139−isFunction :: Value -> Bool
140−isFunction (Abs _ _) = True
141−isFunction (TypedValue untyped _) = isFunction untyped
144−typeOf :: Maybe Ident -> Value -> Check Type
146− ty <- runSubst $ case name of
147− Just ident -> do me <- fresh
148− ty <- infer (M.singleton ident me) val
151− Nothing -> infer M.empty val
152− --desugared <- replaceAllTypeSynonyms cs
153− --TODO: allUnknownsBecameQuantified desugared solution ty
154− return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty
157−allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
158−allUnknownsBecameQuantified cs solution ty = do
160− typesMentioned = findUnknownTypes ty
161− unknownTypes = nub $ flip concatMap cs $ \c -> case c of
162− TypeConstraint u t _ -> u : findUnknownTypes t
163− RowConstraint _ r _ -> findUnknownTypes r
164− unsolvedTypes = filter (\n -> TUnknown n == fst (runTypeSolution solution) n) unknownTypes
165− guardWith "Unsolved type variable" $ null $ unsolvedTypes \\ typesMentioned
167− rowsMentioned = findUnknownRows ty
168− unknownRows = nub $ flip concatMap cs $ \c -> case c of
169− TypeConstraint _ t _ -> findUnknownRows t
170− RowConstraint u r _ -> u : findUnknownRows r
171− unsolvedRows = filter (\n -> RUnknown n == snd (runTypeSolution solution) n) unknownRows
172− guardWith "Unsolved row variable" $ null $ unsolvedRows \\ rowsMentioned
174−findUnknownTypes :: (D.Data d) => d -> [Unknown Type]
175−findUnknownTypes = everything (++) (mkQ [] f)
177− f :: Type -> [Unknown Type]
178− f (TUnknown n) = [n]
181−findUnknownRows :: (D.Data d) => d -> [Unknown Row]
182−findUnknownRows = everything (++) (mkQ [] f)
184− f :: Row -> [Unknown Row]
185− f (RUnknown n) = [n]
190−setify = rowFromList . first (M.toList . M.fromList) . rowToList
192−setifyAll :: (D.Data d) => d -> d
193−setifyAll = everywhere (mkT setify)
195−findTypeVars :: (D.Data d) => d -> [String]
196−findTypeVars = everything (++) (mkQ [] f)
198− f :: Type -> [String]
202−varIfUnknown :: Type -> Type
205− (ty', m) = flip runState M.empty $ everywhereM (flip extM g $ mkM f) ty
207− ForAll (sort $ nub $ M.elems m ++ findTypeVars ty) ty'
209− f :: Type -> State (M.Map Int String) Type
210− f (TUnknown (Unknown n)) = do
212− case M.lookup n m of
214− let name = 't' : show (M.size m)
215− put $ M.insert n name m
216− return $ TypeVar name
217− Just name -> return $ TypeVar name
219− g :: Row -> State (M.Map Int String) Row
220− g (RUnknown (Unknown n)) = do
222− case M.lookup n m of
224− let name = 'r' : show (M.size m)
225− put $ M.insert n name m
226− return $ RowVar name
227− Just name -> return $ RowVar name
230−replaceTypeVars :: M.Map String Type -> Type -> Type
231−replaceTypeVars m = everywhere (mkT replace)
233− replace (TypeVar v) = case M.lookup v m of
238−replaceVarsWithUnknowns :: [String] -> Type -> Subst Check Type
239−replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
241− f :: Type -> StateT (M.Map String Int) (Subst Check) Type
242− f (TypeVar var) | var `elem` idents = do
245− case M.lookup var m of
247− put (M.insert var n m)
248− return $ TUnknown (Unknown n)
249− Just u -> return $ TUnknown (Unknown u)
251− g :: Row -> StateT (M.Map String Int) (Subst Check) Row
252− g (RowVar var) | var `elem` idents = do
255− case M.lookup var m of
257− put (M.insert var n m)
258− return $ RUnknown (Unknown n)
259− Just u -> return $ RUnknown (Unknown u)
262−replaceAllTypeSynonyms :: (D.Data d) => d -> Check d
263−replaceAllTypeSynonyms d = do
265− let syns = map (\((path, name), (args, _)) -> (Qualified path name, length args)) . M.toList $ typeSynonyms env
266− either throwError return $ saturateAllTypeSynonyms syns d
268−desaturateAllTypeSynonyms :: (D.Data d) => d -> d
269−desaturateAllTypeSynonyms = everywhere (mkT replace)
271− replace (SaturatedTypeSynonym name args) = foldl TypeApp (TypeConstructor name) args
274−ensureNoDuplicateProperties :: [(String, Value)] -> Check ()
275−ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (nub . map fst $ ps) == length ps
277−infer :: M.Map Ident Type -> Value -> Subst Check Type
278−infer _ (NumericLiteral _) = return Number
279−infer _ (StringLiteral _) = return String
280−infer _ (BooleanLiteral _) = return Boolean
281−infer m (ArrayLiteral vals) = do
282− ts <- mapM (infer m) vals
284− forM_ ts $ \t -> arr ~~ Array t
286−infer m (Unary op val) = do
289−infer m (Binary op left right) = do
292− inferBinary op t1 t2
293−infer m (ObjectLiteral ps) = do
294− lift $ ensureNoDuplicateProperties ps
295− ts <- mapM (infer m . snd) ps
296− let fields = zipWith (\(name, _) t -> (name, t)) ps ts
297− return $ Object $ typesToRow fields
298−infer m (ObjectUpdate o ps) = do
299− lift $ ensureNoDuplicateProperties ps
302− ts <- mapM (infer m . snd) ps
303− let tys = zipWith (\(name, _) t -> (name, t)) ps ts
304− obj ~~ Object (rowFromList (tys, row))
306−infer m (Indexer index val) = do
313−infer m (Accessor prop val) = do
317− obj ~~ Object (RCons prop field rest)
319−infer m v@(Abs args ret) = do
320− ts <- replicateM (length args) fresh
321− let m' = m `M.union` M.fromList (zip args ts)
322− body <- infer m' ret
323− return $ Function ts body
324−infer m v@(App f xs) = do
326− ts <- mapM (infer m) xs
328− t1 ~~ Function ts me
330−infer m v@(Var var@(Qualified mp name)) = do
333− case M.lookup name m of
334− Just ty -> lift $ replaceAllTypeSynonyms ty
335− Nothing -> lookupGlobal
340− modulePath <- checkModulePath `fmap` lift get
341− case M.lookup (qualify modulePath var) (names env) of
342− Nothing -> throwError $ show var ++ " is undefined"
343− Just (ty, _) -> lift $ replaceAllTypeSynonyms ty
344−infer m (Block ss) = do
346− (allCodePathsReturn, _) <- checkBlock m M.empty ret ss
347− guardWith "Block is missing a return statement" allCodePathsReturn
349−infer m v@(Constructor c) = do
351− modulePath <- checkModulePath `fmap` lift get
352− case M.lookup (qualify modulePath c) (dataConstructors env) of
353− Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
354− Just (ForAll idents ty) -> replaceVarsWithUnknowns idents ty
355−infer m (Case val binders) = do
358− cs2 <- checkBinders m t1 ret binders
360−infer m v@(IfThenElse cond th el) = do
367−infer m v@(TypedValue val ty) = do
368− kind <- lift $ kindOf ty
369− guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
370− ty' <- lift $ replaceAllTypeSynonyms ty
371− cs <- check m val ty'
374−inferUnary :: UnaryOperator -> Type -> Subst Check Type
375−inferUnary Negate val = do
378−inferUnary Not val = do
381−inferUnary BitwiseNot val = do
385−inferBinary :: BinaryOperator -> Type -> Type -> Subst Check Type
386−inferBinary Add = inferSymBinary Number
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
407−inferEqBinary :: Type -> Type -> Subst Check Type
408−inferEqBinary left right = do
412−inferSymBinary :: Type -> Type -> Type -> Subst Check Type
413−inferSymBinary ty = inferAsymBinary ty ty
415−inferAsymBinary :: Type -> Type -> Type -> Type -> Subst Check Type
416−inferAsymBinary input output left right = do
421−inferBinder :: Type -> Binder -> Subst Check (M.Map Ident Type)
422−inferBinder _ NullBinder = return M.empty
423−inferBinder val (StringBinder _) = val ~~ String >> return M.empty
424−inferBinder val (NumberBinder _) = val ~~ Number >> return M.empty
425−inferBinder val (BooleanBinder _) = val ~~ Boolean >> return M.empty
426−inferBinder val (VarBinder name) = return $ M.singleton name val
427−inferBinder val (NullaryBinder ctor) = do
429− modulePath <- checkModulePath `fmap` lift get
430− case M.lookup (qualify modulePath ctor) (dataConstructors env) of
431− Just (ForAll args ret) -> do
432− ret' <- replaceVarsWithUnknowns args ret
435− _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
436−inferBinder val b@(UnaryBinder ctor binder) = do
438− modulePath <- checkModulePath `fmap` lift get
439− case M.lookup (qualify modulePath ctor) (dataConstructors env) of
440− Just (ForAll idents f@(Function [_] _)) -> do
442− (Function [ty] ret) <- replaceVarsWithUnknowns idents f
443− m1 <- inferBinder obj binder
447− Just _ -> throwError $ show ctor ++ " is not a unary constructor"
448− _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
449−inferBinder val b@(ObjectBinder props) = do
452− m1 <- inferRowProperties row rest props
456− inferRowProperties :: Row -> Row -> [(String, Binder)] -> Subst Check (M.Map Ident Type)
457− inferRowProperties nrow row [] = nrow ~~ row >> return M.empty
458− inferRowProperties nrow row ((name, binder):binders) = do
460− m1 <- inferBinder propTy binder
461− m2 <- inferRowProperties nrow (RCons name propTy row) binders
462− return $ m1 `M.union` m2
463−inferBinder val (ArrayBinder binders rest) = do
465− m1 <- M.unions <$> mapM (inferBinder el) binders
468− Nothing -> return m1
470− m2 <- inferBinder val binder
471− return $ m1 `M.union` m2
472−inferBinder val (NamedBinder name binder) = do
473− m <- inferBinder val binder
474− return $ M.insert name val m
476−inferGuardedBinder :: M.Map Ident Type -> Type -> Binder -> Subst Check (M.Map Ident Type)
477−inferGuardedBinder m val b@(GuardedBinder cond binder) = do
478− m1 <- inferBinder val binder
479− ty <- infer (m `M.union` m1) cond
482−inferGuardedBinder m val b = inferBinder val b >>= return
484−checkBinders :: M.Map Ident Type -> Type -> Type -> [(Binder, Value)] -> Subst Check ()
485−checkBinders _ _ _ [] = return ()
486−checkBinders m nval ret ((binder, val):bs) = do
487− m1 <- inferGuardedBinder m nval binder
488− t <- infer (m `M.union` m1) val
490− checkBinders m nval ret bs
492−assignVariable :: Ident -> M.Map Ident Type -> Subst Check ()
493−assignVariable name m =
494− case M.lookup name m of
495− Nothing -> return ()
496− Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
498−checkStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> Statement -> Subst Check (Bool, M.Map Ident Type)
499−checkStatement m mass ret (VariableIntroduction name val) = do
500− assignVariable name (m `M.union` mass)
502− return (False, M.insert name t mass)
503−checkStatement m mass ret (Assignment ident val) = do
505− case M.lookup ident mass of
506− Nothing -> throwError $ "No local variable with name " ++ show ident
507− Just ty -> do t ~~ ty
508− return (False, mass)
509−checkStatement m mass ret (While val inner) = do
512− (allCodePathsReturn, _) <- checkBlock m mass ret inner
513− return (allCodePathsReturn, mass)
514−checkStatement m mass ret (If ifst) = do
515− allCodePathsReturn <- checkIfStatement m mass ret ifst
516− return (allCodePathsReturn, mass)
517−checkStatement m mass ret (For ident start end inner) = do
518− assignVariable ident (m `M.union` mass)
519− t1 <- infer (m `M.union` mass) start
521− t2 <- infer (m `M.union` mass) end
523− let mass1 = M.insert ident Number mass
524− (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner
525− return (allCodePathsReturn, mass)
526−checkStatement m mass ret (ForEach ident vals inner) = do
527− assignVariable ident (m `M.union` mass)
529− t1 <- infer (m `M.union` mass) vals
531− let mass1 = M.insert ident val mass
532− (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner
533− guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn
534− return (False, mass)
535−checkStatement m mass ret (Return val) = do
536− check (m `M.union` mass) val ret
539−checkIfStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> IfStatement -> Subst Check Bool
540−checkIfStatement m mass ret (IfStatement val thens Nothing) = do
543− _ <- checkBlock m mass ret thens
545−checkIfStatement m mass ret (IfStatement val thens (Just elses)) = do
548− (allCodePathsReturn1, _) <- checkBlock m mass ret thens
549− allCodePathsReturn2 <- checkElseStatement m mass ret elses
550− return $ allCodePathsReturn1 && allCodePathsReturn2
552−checkElseStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> ElseStatement -> Subst Check Bool
553−checkElseStatement m mass ret (Else elses) = fst <$> checkBlock m mass ret elses
554−checkElseStatement m mass ret (ElseIf ifst) = checkIfStatement m mass ret ifst
556−checkBlock :: M.Map Ident Type -> M.Map Ident Type -> Type -> [Statement] -> Subst Check (Bool, M.Map Ident Type)
557−checkBlock _ mass _ [] = return (False, mass)
558−checkBlock m mass ret (s:ss) = do
559− (b1, mass1) <- checkStatement (m `M.union` mass) mass ret s
561− (True, []) -> return (True, mass1)
562− (True, _) -> throwError "Unreachable code"
564− (b2, mass2) <- checkBlock m mass1 ret ss
567−skolemize :: [String] -> Type -> Subst Check Type
568−skolemize idents ty = do
569− sks <- replicateM (length idents) fresh'
570− let m = M.fromList (zip idents (map Skolem sks))
571− return $ replaceTypeVars m ty
573−check :: M.Map Ident Type -> Value -> Type -> Subst Check ()
574−check m (NumericLiteral _) Number = return ()
575−check m (StringLiteral _) String = return ()
576−check m (BooleanLiteral _) Boolean = return ()
577−check m (Unary Negate val) Number = check m val Number
578−check m (Unary Not val) Boolean = check m val Boolean
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
581−check m (ArrayLiteral vals) (Array ty) = forM_ vals (\val -> check m val ty)
582−check m (Indexer index vals) ty = check m index Number >> check m vals (Array ty)
583−check m (Abs args ret) (Function argTys retTy) = do
584− guardWith "Incorrect number of function arguments" (length args == length argTys)
585− let bindings = M.fromList (zip args argTys)
586− check (bindings `M.union` m) ret retTy
587−check m (App f xs) ret = do
589− checkFunctionApplication m ft xs ret
590−check m val (ForAll idents ty) = do
591− sk <- skolemize idents ty
593−check m val u@(TUnknown _) = do
596−check _ val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty
598−checkFunctionApplication :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()
599−checkFunctionApplication m (Function argTys retTy) args ret = do
600− guardWith "Incorrect number of function arguments" (length args == length argTys)
601− zipWithM (check m) args argTys
603−checkFunctionApplication m (ForAll idents ty) args ret = do
604− replaced <- replaceVarsWithUnknowns idents ty
605− checkFunctionApplication m replaced args ret
606−checkFunctionApplication _ fnTy args ret = throwError $ "Cannot apply function of type "
607− ++ prettyPrintType fnTy
608− ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)
609− ++ ". Expecting value of type " ++ prettyPrintType ret ++ "."
612− | Binary BinaryOperator Value Value
613− | ObjectLiteral [(String, Value)]
614− | Accessor String Value
615− | ObjectUpdate Value [(String, Value)]
616− | Var (Qualified Ident)
617− | IfThenElse Value Value Value
619− | Constructor (Qualified ProperName)
620− | Case Value [(Binder, Value)]
621− | TypedValue Value PolyType