packages feed

purescript 0.3.8.1 → 0.3.9

raw patch · 13 files changed

+343/−132 lines, 13 files

Files

libraries/prelude/prelude.purs view
@@ -61,10 +61,37 @@     read "true" = true     read _ = false +  infixl 4 <$>++  class Functor f where+    (<$>) :: forall a b. (a -> b) -> f a -> f b++  infixl 4 <*>++  class Applicative f where+    pure :: forall a. a -> f a+    (<*>) :: forall a b. f (a -> b) -> f a -> f b++  instance (Applicative f) => Functor f where+    (<$>) f a = pure f <*> a++  infixl 3 <|>++  class Alternative f where+    empty :: forall a. f a+    (<|>) :: forall a. f a -> f a -> f a+   class Monad m where     ret :: forall a. a -> m a     (>>=) :: forall a b. m a -> (a -> m b) -> m b +  instance (Monad m) => Applicative m where+    pure = ret+    (<*>) f a = do+      f' <- f+      a' <- a+      ret (f' a')+   infixl 5 *   infixl 5 /   infixl 5 %@@ -326,6 +353,74 @@                       \  };\                       \}" :: String -> String -> String +module Monoid where++  import Prelude++  infixr 6 <>++  class Monoid m where+    mempty :: m+    (<>) :: m -> m -> m+  +  instance Monoid String where+    mempty = ""+    (<>) = (++)++  mconcat :: forall m. (Monoid m) => [m] -> m+  mconcat [] = mempty+  mconcat (m:ms) = m <> mconcat ms++module Monad where++  import Prelude+  import Arrays++  replicateM :: forall m a. (Monad m) => Number -> m a -> m [a]+  replicateM 0 _ = ret []+  replicateM n m = do+    a <- m+    as <- replicateM (n - 1) m+    ret (a : as) ++  mapM :: forall m a b. (Monad m) => (a -> m b) -> [a] -> m [b]+  mapM _ [] = ret []+  mapM f (a:as) = do+    b <- f a+    bs <- mapM f as+    ret (b : bs)++  infixr 1 >=>+  infixr 1 <=<++  (>=>) :: forall m a b c. (Monad m) => (a -> m b) -> (b -> m c) -> a -> m c+  (>=>) f g a = do+    b <- f a+    g b+    +  (<=<) :: forall m a b c. (Monad m) => (b -> m c) -> (a -> m b) -> a -> m c +  (<=<) = flip (>=>)++  sequence :: forall m a. (Monad m) => [m a] -> m [a]+  sequence [] = ret []+  sequence (m:ms) = do+    a <- m+    as <- sequence ms+    ret (a : as)++  join :: forall m a. (Monad m) => m (m a) -> m a+  join mm = do+    m <- mm+    m++  foldM :: forall m a b. (Monad m) => (a -> b -> m a) -> a -> [b] -> m a+  foldM _ a [] = ret a+  foldM f a (b:bs) = f a b >>= \a' -> foldM f a' bs++  when :: forall m. (Monad m) => Boolean -> m {} -> m {}+  when true m = m+  when false _ = ret {}+ module Maybe where    import Prelude@@ -408,9 +503,9 @@                         \  };\                         \}" :: forall a. [a] -> [a] -> [a] -  foreign import join "function join(l) {\-                      \  return l.join();\-                      \}" :: [String] -> String+  foreign import joinS "function joinS(l) {\+                       \  return l.join();\+                       \}" :: [String] -> String    foreign import joinWith "function joinWith(l) {\                           \  return function (s) {\@@ -467,6 +562,9 @@   (:) :: forall a. a -> [a] -> [a]   (:) a = concat [a] +  singleton :: forall a. a -> [a]+  singleton a = [a]+   concatMap :: forall a b. [a] -> (a -> [b]) -> [b]   concatMap [] f = []   concatMap (a:as) f = f a `concat` concatMap as f@@ -476,9 +574,9 @@   filter p (x:xs) | p x = x : filter p xs   filter p (_:xs) = filter p xs -  empty :: forall a. [a] -> Boolean-  empty [] = true-  empty _ = false+  isEmpty :: forall a. [a] -> Boolean+  isEmpty [] = true+  isEmpty _ = false    range :: Number -> Number -> [Number]   range lo hi = {@@ -505,6 +603,14 @@     show [] = "[]"     show (x:xs) = show x ++ " : " ++ show xs +  instance Prelude.Monad [] where+    ret = singleton+    (>>=) = concatMap++  instance Prelude.Alternative [] where+    empty = []+    (<|>) = concat+ module Tuple where    import Prelude@@ -783,6 +889,46 @@     ret = retEff     (>>=) = bindEff +  foreign import untilE "function untilE(f) {\+			\  return function() {\+			\    while (!f()) { }\+			\    return {};\+			\  };\+                        \}" :: forall e. Eff e Boolean -> Eff e {}++  foreign import whileE "function whileE(f) {\+			\  return function(a) {\+			\    return function() {\+			\      while (f()) {\+                        \        a();\+                        \      }\+			\      return {};\+                        \    };\+                        \  };\+                        \}" :: forall e. Eff e Boolean -> Eff e {} -> Eff e {}+ +  foreign import forE "function forE(lo) {\+	              \  return function(hi) {\+	              \    return function(f) {\+	              \      return function() {\+	              \        for (var i = lo; i < hi; i++) {\+		      \          f(i)();\+                      \        }\+                      \      };\+                      \    };\+                      \  };\+                      \}" :: forall e. Number -> Number -> (Number -> Eff e {}) -> Eff e {}+++  foreign import foreachE "function foreachE(as) {\+	                  \  return function(f) {\+	                  \    for (var i = 0; i < as.length; i++) {\+		          \      f(as[i])();\+                          \    }\+                          \  };\+                          \}" :: forall e a. [a] -> (a -> Eff e {}) -> Eff e {}++ module Random where    import Eff@@ -790,9 +936,7 @@   foreign import data Random :: !    foreign import random "function random() {\-                        \  return function() {\-                        \    return Math.random();\-                        \  };\+                        \  return Math.random();\                         \}" :: forall e. Eff (random :: Random | e) Number  module Errors where
psc/Main.hs view
@@ -28,10 +28,10 @@ preludeFilename = Paths.getDataFileName "libraries/prelude/prelude.purs"  readInput :: Maybe [FilePath] -> IO (Either ParseError [P.Module])-readInput Nothing = getContents >>= return . P.runIndentParser P.parseModules+readInput Nothing = getContents >>= return . P.runIndentParser "" P.parseModules readInput (Just input) = fmap (fmap concat . sequence) $ forM input $ \inputFile -> do   text <- U.readFile inputFile-  return $ P.runIndentParser P.parseModules text+  return $ P.runIndentParser inputFile P.parseModules text  compile :: P.Options -> Maybe [FilePath] -> Maybe FilePath -> Maybe FilePath -> IO () compile opts input output externs = do
psci/Main.hs view
@@ -106,7 +106,7 @@ loadModule moduleFile = do   print moduleFile   moduleText <- U.readFile moduleFile-  return . either (Left . show) Right $ P.runIndentParser P.parseModules moduleText+  return . either (Left . show) Right $ P.runIndentParser "" P.parseModules moduleText  main :: IO () main = do@@ -128,7 +128,7 @@     case cmd of       Empty -> go imports loadedModules       Expression ls -> do-        case P.runIndentParser (P.whiteSpace *> P.parseValue <* Parsec.eof) (unlines ls) of+        case P.runIndentParser "" (P.whiteSpace *> P.parseValue <* Parsec.eof) (unlines ls) of           Left err -> outputStrLn (show err)           Right decl -> handleDeclaration loadedModules imports decl         go imports loadedModules
purescript.cabal view
@@ -1,5 +1,5 @@ name: purescript-version: 0.3.8.1+version: 0.3.9 cabal-version: >=1.8 build-type: Simple license: MIT
src/Language/PureScript/CodeGen/JS.hs view
@@ -128,7 +128,7 @@   where   getFunctionArgumentType :: Type -> Maybe Type   getFunctionArgumentType (TypeApp (TypeApp t funArg) _) | t == tyFunction = Just funArg-  getFunctionArgumentType (ForAll _ ty') = getFunctionArgumentType ty'+  getFunctionArgumentType (ForAll _ ty' _) = getFunctionArgumentType ty'   getFunctionArgumentType _ = Nothing   argumentCheck :: JS -> Type -> [JS]   argumentCheck val t | t == tyNumber = [typeCheck val "number"]@@ -141,7 +141,7 @@     in       typeCheck val "object" : concatMap (\(prop, ty') -> argumentCheck (JSAccessor prop val) ty') pairs   argumentCheck val (TypeApp (TypeApp t _) _) | t == tyFunction = [typeCheck val "function"]-  argumentCheck val (ForAll _ ty') = argumentCheck val ty'+  argumentCheck val (ForAll _ ty' _) = argumentCheck val ty'   argumentCheck _ _ = []   typeCheck :: JS -> String -> JS   typeCheck js ty' = JSIfElse (JSBinary NotEqualTo (JSTypeOf js) (JSStringLiteral ty')) (JSBlock [JSThrow (JSStringLiteral $ ty' ++ " expected")]) Nothing@@ -253,7 +253,7 @@   where   numConstructors ty = length $ filter (\(ty1, _) -> ((==) `on` typeConstructor) ty ty1) $ M.elems $ dataConstructors e   typeConstructor (TypeConstructor qual) = qualify m qual-  typeConstructor (ForAll _ ty) = typeConstructor ty+  typeConstructor (ForAll _ ty _) = typeConstructor ty   typeConstructor (TypeApp (TypeApp t _) ty) | t == tyFunction = typeConstructor ty   typeConstructor (TypeApp ty _) = typeConstructor ty   typeConstructor fn = error $ "Invalid arguments to typeConstructor: " ++ show fn
src/Language/PureScript/Parser/Common.hs view
@@ -399,5 +399,5 @@ -- | -- Run a parser which supports indentation ---runIndentParser :: P.Parsec String ParseState a -> String -> Either P.ParseError a-runIndentParser p = P.runParser p (ParseState 0) ""+runIndentParser :: FilePath -> P.Parsec String ParseState a -> String -> Either P.ParseError a+runIndentParser filePath p = P.runParser p (ParseState 0) filePath
src/Language/PureScript/Pretty/Types.hs view
@@ -36,10 +36,10 @@   match (TypeApp arr ty) | arr == tyArray = Just $ "[" ++ prettyPrintType ty ++ "]"   match (TypeConstructor ctor) = Just $ show ctor   match (TUnknown (Unknown u)) = Just $ 'u' : show u-  match (Skolem s) = Just $ 's' : show s+  match (Skolem s _) = Just $ 's' : show s   match (ConstrainedType deps ty) = Just $ "(" ++ intercalate "," (map (\(pn, ty') -> show pn ++ " (" ++ prettyPrintType ty' ++ ")") deps) ++ ") => " ++ prettyPrintType ty   match (SaturatedTypeSynonym name args) = Just $ show name ++ "<" ++ intercalate "," (map prettyPrintType args) ++ ">"-  match (ForAll ident ty) = Just $ "forall " ++ ident ++ ". " ++ prettyPrintType ty+  match (ForAll ident ty _) = Just $ "forall " ++ ident ++ ". " ++ prettyPrintType ty   match REmpty = Just $ prettyPrintRow REmpty   match row@(RCons _ _ _) = Just $ prettyPrintRow row   match _ = Nothing@@ -56,7 +56,7 @@   tailToPs REmpty = ""   tailToPs (TUnknown (Unknown u)) = " | u" ++ show u   tailToPs (TypeVar var) = " | " ++ var-  tailToPs (Skolem s) = " | s" ++ show s+  tailToPs (Skolem s _) = " | s" ++ show s   tailToPs _ = error "Invalid row tail"   toList :: [(String, Type)] -> Type -> ([(String, Type)], Type)   toList tys (RCons name ty row) = toList ((name, ty):tys) row
src/Language/PureScript/Sugar/TypeClasses.hs view
@@ -74,7 +74,7 @@ typeClassMemberToDictionaryAccessor name arg (TypeDeclaration ident ty) =   ExternDeclaration TypeClassAccessorImport ident     (Just (JSFunction (Just $ identToJs ident) ["dict"] (JSBlock [JSReturn (JSAccessor (identToJs ident) (JSVar "dict"))])))-    (ForAll arg (ConstrainedType [(Qualified Nothing name, TypeVar arg)] ty))+    (ForAll arg (ConstrainedType [(Qualified Nothing name, TypeVar arg)] ty) Nothing) typeClassMemberToDictionaryAccessor _ _ _ = error "Invalid declaration in type class definition"  typeInstanceDictionaryDeclaration :: ModuleName -> [(Qualified ProperName, Type)] -> Qualified ProperName -> Type -> [Declaration] -> Desugar Declaration@@ -120,7 +120,7 @@ qualifiedToString _ (Qualified (Just (ModuleName mn)) pn) = runProperName mn ++ "_" ++ runProperName pn  quantify :: Type -> Type-quantify ty' = foldr ForAll ty' tyVars+quantify ty' = foldr (\arg t -> ForAll arg t Nothing) ty' tyVars   where   tyVars = nub $ everything (++) (mkQ [] collect) ty'   collect (TypeVar v) = [v]
src/Language/PureScript/TypeChecker.hs view
@@ -230,7 +230,7 @@       addTypeClassDictionaries [tcd { tcdName = (Qualified (Just currentModule) ident), tcdType = TCDAlias (tcdName tcd) }]   constructs (TypeConstructor (Qualified (Just mn) pn')) pn     = mn == moduleName && pn' == pn-  constructs (ForAll _ ty) pn = ty `constructs` pn+  constructs (ForAll _ ty _) pn = ty `constructs` pn   constructs (TypeApp (TypeApp t _) ty) pn | t == tyFunction = ty `constructs` pn   constructs (TypeApp ty _) pn = ty `constructs` pn   constructs fn _ = error $ "Invalid arguments to constructs: " ++ show fn
src/Language/PureScript/TypeChecker/Kinds.hs view
@@ -142,7 +142,7 @@   k2 <- infer t2   k1 =?= FunKind k2 k0   return k0-infer (ForAll ident ty) = do+infer (ForAll ident ty _) = do   k <- fresh   Just moduleName <- checkCurrentModule <$> get   bindLocalTypeVariables moduleName [(ProperName ident, k)] $ infer ty
src/Language/PureScript/TypeChecker/Types.hs view
@@ -45,7 +45,8 @@ import Data.Maybe (maybeToList, isNothing, isJust, fromMaybe) import qualified Data.Data as D import Data.Generics-       (mkM, everywhereM, everything, mkT, something, everywhere, mkQ)+       (everythingWithContext, mkM, everywhereM, everything, mkT,+        something, everywhere, mkQ)  import Language.PureScript.Values import Language.PureScript.Types@@ -66,6 +67,7 @@  import qualified Data.Map as M import Data.Function (on)+import Debug.Trace (trace)  instance Partial Type where   unknown = TUnknown@@ -86,17 +88,23 @@   unifyTypes' (TUnknown u) t = u =:= t   unifyTypes' t (TUnknown u) = u =:= t   unifyTypes' (SaturatedTypeSynonym name args) ty = do-    ty1 <- expandTypeSynonym name args+    ty1 <- introduceSkolemScope <=< expandTypeSynonym name $ args     ty1 `unifyTypes` ty   unifyTypes' ty s@(SaturatedTypeSynonym _ _) = s `unifyTypes` ty-  unifyTypes' (ForAll ident1 ty1) (ForAll ident2 ty2) = do-    sk <- skolemize ident1 ty1-    replaced <- replaceVarWithUnknown ident2 ty2-    sk `unifyTypes` replaced-  unifyTypes' (ForAll ident ty1) ty2 = do-    sk <- skolemize ident ty1+  unifyTypes' (ForAll ident1 ty1 sc1) (ForAll ident2 ty2 sc2) =+    case (sc1, sc2) of+      (Just sc1', Just sc2') -> do+        sko <- newSkolemConstant+        let sk1 = skolemize ident1 sko sc1' ty1+        let sk2 = skolemize ident2 sko sc2' ty2+        sk1 `unifyTypes` sk2+      _ -> throwError (prettyPrintType ty1)+  unifyTypes' (ForAll ident ty1 (Just sc)) ty2 = do+    sko <- newSkolemConstant+    let sk = skolemize ident sko sc ty1     sk `unifyTypes` ty2-  unifyTypes' ty f@(ForAll _ _) = f `unifyTypes` ty+  unifyTypes' (ForAll _ _ _) _ = throwError "Skolem variable scope is unspecified"+  unifyTypes' ty f@(ForAll _ _ _) = f `unifyTypes` ty   unifyTypes' (Object row1) (Object row2) = row1 =?= row2   unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()   unifyTypes' (TypeConstructor c1) (TypeConstructor c2) = do@@ -106,7 +114,7 @@   unifyTypes' (TypeApp t3 t4) (TypeApp t5 t6) = do     t3 `unifyTypes` t5     t4 `unifyTypes` t6-  unifyTypes' (Skolem s1) (Skolem s2) | s1 == s2 = return ()+  unifyTypes' (Skolem s1 _) (Skolem s2 _) | s1 == s2 = return ()   unifyTypes' r1@(RCons _ _ _) r2 = unifyRows r1 r2   unifyTypes' r1 r2@(RCons _ _ _) = unifyRows r1 r2   unifyTypes' r1@REmpty r2 = unifyRows r1 r2@@ -143,7 +151,7 @@     unifyRows' row r others u'   unifyRows' [] REmpty [] REmpty = return ()   unifyRows' [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = return ()-  unifyRows' [] (Skolem s1) [] (Skolem s2) | s1 == s2 = return ()+  unifyRows' [] (Skolem s1 _) [] (Skolem s2 _) | s1 == s2 = return ()   unifyRows' sd3 r3 sd4 r4 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd3, r3)) ++ " with " ++ prettyPrintRow (rowFromList (sd4, r4)) ++ "."  -- |@@ -171,22 +179,24 @@         (ident, (val, Just (ty, checkType))) -> do           kind <- liftCheck $ kindOf moduleName ty           guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star-          ty' <- replaceAllTypeSynonyms ty-          val' <- bindNames dict $ if checkType then check val ty' else return val+          ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty+          val' <- bindNames dict $ if checkType+                                   then TypedValue True <$> check val ty' <*> pure ty'+                                   else return (TypedValue False val ty')           return (ident, (val', ty'))         (ident, (val, Nothing)) -> do           TypedValue _ val' ty <- bindNames dict $ infer val           ty =?= fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)-          return (ident, (val', ty))+          return (ident, (TypedValue True val' ty, ty))       when (moduleName == ModuleName (ProperName "Main") && fst e == Ident "main") $ do         [eff, a] <- replicateM 2 fresh         ty =?= TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a       escapeCheck val ty       return triple-  forM_ tys $ skolemEscapeCheck . snd . snd   forM tys $ \(ident, (val, ty)) -> do     val' <- replaceTypeClassDictionaries moduleName val-    return (ident, (overTypes (desaturateAllTypeSynonyms . setifyAll) $ val'+    rethrow (("Error in " ++ show ident ++ ": \n") ++) $ skolemEscapeCheck val'+    return $ (ident, (overTypes (desaturateAllTypeSynonyms . setifyAll) $ val'                    , varIfUnknown . desaturateAllTypeSynonyms . setifyAll $ ty))   where   tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (sub $?) val, sub $? ty))) ts@@ -238,7 +248,7 @@     return $ Just dict   mkDictionary :: Qualified Ident -> Maybe [Value] -> Value   mkDictionary fnName Nothing = Var fnName-  mkDictionary fnName (Just dicts) = foldr (flip App) (Var fnName) dicts+  mkDictionary fnName (Just dicts) = foldl App (Var fnName) dicts   filterModule :: TypeClassDictionaryInScope -> Bool   filterModule (TypeClassDictionaryInScope { tcdName = Qualified (Just mn) _ }) | mn == moduleName = True   filterModule (TypeClassDictionaryInScope { tcdName = Qualified Nothing _ }) = True@@ -252,7 +262,9 @@ -- and return a substitution from type variables to types which makes the type heads unify. -- typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]-typeHeadsAreEqual _ _ (Skolem s1) (Skolem s2) | s1 == s2 = Just []+typeHeadsAreEqual _ _ (Skolem s1 _) (Skolem s2 _) | s1 == s2 = Just []+typeHeadsAreEqual _ _ (TypeVar v) t = Just [(v, t)]+typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)] typeHeadsAreEqual m e (TypeConstructor c1) (TypeConstructor c2) | typeConstructorsAreEqual e m c1 c2 = Just [] typeHeadsAreEqual m e (TypeApp h1 (TypeVar v)) (TypeApp h2 arg) = (:) (v, arg) <$> typeHeadsAreEqual m e h1 h2 typeHeadsAreEqual m e t1@(TypeApp _ _) t2@(TypeApp _ (TypeVar _)) = typeHeadsAreEqual m e t2 t1@@ -268,7 +280,7 @@   let allUnknowns = findAllTypes value   forM_ allUnknowns $ \t -> do     let unsolvedUnknowns = nub . unknowns $ subst $? t-    guardWith ("Escape check fails" ++ show (subst $? ty, subst $? t)) $ null $ unsolvedUnknowns \\ visibleUnknowns+    guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns  -- | -- Find all type annotations occuring inside a value@@ -282,14 +294,31 @@ -- | -- Ensure skolem variables do not escape their scope ---skolemEscapeCheck :: Type -> Check ()-skolemEscapeCheck ty =-  case something (mkQ Nothing findSkolems) ty of-    Nothing -> return ()-    Just _ -> throwError $ "Skolem variables cannot escape. Consider adding a type signature."+skolemEscapeCheck :: Value -> Check ()+skolemEscapeCheck (TypedValue False _ _) = return ()+skolemEscapeCheck root@(TypedValue _ _ _) =+  case everythingWithContext [] (++) (mkQ ((,) []) go) root of+    [] -> return ()+    ((binding, val) : _) -> throwError $ "Rigid/skolem type variable bound by " ++ maybe "<unknown>" prettyPrintValue binding ++ " has escaped at " ++ prettyPrintValue val   where-    findSkolems (Skolem _) = return ()-    findSkolems _ = mzero+  go :: Value -> [(SkolemScope, Value)] -> ([(Maybe Value, Value)], [(SkolemScope, Value)])+  go val@(TypedValue _ _ (ForAll _ _ (Just sco))) scos = ([], (sco, val) : scos)+  go val@(TypedValue _ _ ty) scos = case collectSkolems ty \\ map fst scos of+                                      (sco : _) -> ([(findBindingScope sco, val)], scos)+                                      _ -> ([], scos)+    where+    collectSkolems :: Type -> [SkolemScope]+    collectSkolems = nub . everything (++) (mkQ [] collect)+      where+      collect (Skolem _ scope) = [scope]+      collect _ = []+  go _ scos = ([], scos)+  findBindingScope :: SkolemScope -> Maybe Value+  findBindingScope sco = something (mkQ Nothing go) root+    where+    go val@(TypedValue _ _ (ForAll _ _ (Just sco'))) | sco == sco' = Just val+    go _ = Nothing+skolemEscapeCheck val = throwError $ "Untyped value passed to skolemEscapeCheck: " ++ prettyPrintValue val  -- | -- Ensure a row contains no duplicate labels@@ -326,7 +355,7 @@ -- Replace named type variables with new unification variables -- replaceAllVarsWithUnknowns :: Type -> UnifyT Type Check Type-replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns+replaceAllVarsWithUnknowns (ForAll ident ty _) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns replaceAllVarsWithUnknowns ty = return ty  -- |@@ -404,7 +433,8 @@   newVals <- zipWith (\(name, _) t -> (name, t)) ps <$> mapM (infer . snd) ps   let newTys = map (\(name, TypedValue _ _ ty) -> (name, ty)) newVals   oldTys <- zip (map fst ps) <$> replicateM (length ps) fresh-  o' <- check o $ Object $ rowFromList (oldTys, row)+  let oldTy = Object $ rowFromList (oldTys, row)+  o' <- TypedValue True <$> check o oldTy <*> pure oldTy   return $ TypedValue True (ObjectUpdate o' newVals) $ Object $ rowFromList (newTys, row) infer' (Accessor prop val) = do   typed@(TypedValue _ _ objTy) <- infer val@@ -424,19 +454,17 @@     return $ TypedValue True (Abs arg body) $ function ty bodyTy infer' (App f arg) = do   f'@(TypedValue _ _ ft) <- infer f-  ret <- fresh-  app <- checkFunctionApplication f' ft arg ret+  (ret, app) <- checkFunctionApplication f' ft arg   return $ TypedValue True app ret infer' (Var var) = do   Just moduleName <- checkCurrentModule <$> get-  ty <- lookupVariable moduleName var-  ty' <- replaceAllTypeSynonyms ty-  case ty' of+  ty <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var+  case ty of     ConstrainedType constraints _ -> do       env <- getEnv       dicts <- getTypeClassDictionaries-      return $ TypedValue True (foldl App (Var var) (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) ty'-    _ -> return $ TypedValue True (Var var) ty'+      return $ TypedValue True (foldl App (Var var) (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) ty+    _ -> return $ TypedValue True (Var var) ty infer' (Block ss) = do   ret <- fresh   (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss@@ -447,7 +475,7 @@   Just moduleName <- checkCurrentModule <$> get   case M.lookup (qualify moduleName c) (dataConstructors env) of     Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"-    Just (ty, _) -> do ty' <- replaceAllTypeSynonyms ty+    Just (ty, _) -> do ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty                        return $ TypedValue True v ty' infer' (Case vals binders) = do   ts <- mapM infer vals@@ -464,9 +492,9 @@   Just moduleName <- checkCurrentModule <$> get   kind <- liftCheck $ kindOf moduleName ty   guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star-  ty' <- replaceAllTypeSynonyms ty+  ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $  ty   val' <- if checkType then check val ty' else return val-  return $ TypedValue True val' ty+  return $ TypedValue True val' ty' infer' _ = error "Invalid argument to infer"  -- |@@ -477,9 +505,9 @@   let (props, _) = rowToList row   return $ lookup prop props inferProperty (SaturatedTypeSynonym name args) prop = do-  replaced <- expandTypeSynonym name args+  replaced <- introduceSkolemScope <=< expandTypeSynonym name $ args   inferProperty replaced prop-inferProperty (ForAll ident ty) prop = do+inferProperty (ForAll ident ty _) prop = do   replaced <- replaceVarWithUnknown ident ty   inferProperty replaced prop inferProperty _ _ = return Nothing@@ -551,7 +579,7 @@   Just moduleName <- checkCurrentModule <$> get   m1 <- M.unions <$> zipWithM inferBinder nvals binders   r <- bindLocalVariables moduleName (M.toList m1) $ do-    val' <- check val ret+    val' <- TypedValue True <$> check val ret <*> pure ret     case grd of       Nothing -> return (binders, Nothing, val')       Just g -> do@@ -602,7 +630,7 @@   return (allCodePathsReturn, mass, For ident start' end' inner') checkStatement mass ret (Return val) = do   val' <- check val ret-  return (True, mass, Return val')+  return (True, mass, Return (TypedValue True val' ret))  -- | -- Check the type of an if-then-else statement@@ -643,14 +671,33 @@       return (b, m, s':ss'')  -- |+-- Generate a new skolem constant+--+newSkolemConstant :: UnifyT Type Check Int+newSkolemConstant = runUnknown <$> fresh'++-- |+-- Generate a new skolem scope+--+newSkolemScope :: UnifyT Type Check SkolemScope+newSkolemScope = SkolemScope . runUnknown <$> fresh'++-- | -- Skolemize a type variable by replacing its instances with fresh skolem constants ---skolemize :: String -> Type -> UnifyT Type Check Type-skolemize ident ty = do-  tsk <- Skolem . runUnknown <$> fresh'-  return $ replaceTypeVars ident tsk ty+skolemize :: (D.Data d) => String -> Int -> SkolemScope -> d -> d+skolemize ident sko scope d = replaceTypeVars ident (Skolem sko scope) d  -- |+-- Introduce skolem scope at every occurence of a ForAll+--+introduceSkolemScope :: Type -> UnifyT Type Check Type+introduceSkolemScope = everywhereM (mkM go)+  where+  go (ForAll ident ty Nothing) = ForAll ident ty <$> (Just <$> newSkolemScope)+  go other = return other++-- | -- Check the type of a value, rethrowing errors to provide a better error message -- check :: Value -> Type -> UnifyT Type Check Value@@ -668,10 +715,13 @@ -- Check the type of a value -- check' :: Value -> Type -> UnifyT Type Check Value-check' val (ForAll idents ty) = do-  sk <- skolemize idents ty-  check val sk-check' val (ConstrainedType constraints ty) = do+check' val t@(ForAll ident ty _) = do+  scope <- newSkolemScope+  sko <- newSkolemConstant+  let sk = skolemize ident sko scope ty+  val' <- check val sk+  return $ TypedValue True val' (ForAll ident ty (Just scope))+check' val t@(ConstrainedType constraints ty) = do   env <- getEnv   Just moduleName <- checkCurrentModule <$> get   dictNames <- flip mapM constraints $ \(Qualified _ (ProperName className), _) -> do@@ -681,34 +731,43 @@     TypeClassDictionaryInScope name className instanceTy Nothing TCDRegular) (map (Qualified Nothing) dictNames)       (qualifyAllUnqualifiedNames moduleName env constraints)) $         check val ty-  return $ foldr Abs val' dictNames+  return $ TypedValue True (foldr Abs val' dictNames) t+check' val t@(SaturatedTypeSynonym name args) = do+  ty <- introduceSkolemScope <=< expandTypeSynonym name $ args+  val' <- check val ty+  return $ TypedValue True val' ty check' val u@(TUnknown _) = do   val'@(TypedValue _ _ ty) <- infer val   -- Don't unify an unknown with an inferred polytype   ty' <- replaceAllVarsWithUnknowns ty   ty' =?= u-  return val'-check' v@(NumericLiteral _) t | t == tyNumber = return v-check' v@(StringLiteral _) t | t == tyString = return v-check' v@(BooleanLiteral _) t | t == tyBoolean = return v-check' (ArrayLiteral vals) (TypeApp a ty) | a == tyArray = ArrayLiteral <$> forM vals (\val -> check val ty)-check' (Abs arg ret) (TypeApp (TypeApp t argTy) retTy) | t == tyFunction = do+  return $ TypedValue True val' ty'+check' v@(NumericLiteral _) t | t == tyNumber =+  return $ TypedValue True v t+check' v@(StringLiteral _) t | t == tyString =+  return $ TypedValue True v t+check' v@(BooleanLiteral _) t | t == tyBoolean =+  return $ TypedValue True v t+check' (ArrayLiteral vals) t@(TypeApp a ty) | a == tyArray = do+  arr <- ArrayLiteral <$> forM vals (\val -> check val ty)+  return $ TypedValue True arr t+check' (Abs arg ret) ty@(TypeApp (TypeApp t argTy) retTy) | t == tyFunction = do   Just moduleName <- checkCurrentModule <$> get   ret' <- bindLocalVariables moduleName [(arg, argTy)] $ check ret retTy-  return $ Abs arg ret'+  return $ TypedValue True (Abs arg ret') ty check' (App f arg) ret = do   f'@(TypedValue _ _ ft) <- infer f-  app <- checkFunctionApplication f' ft arg ret-  return $ app+  (ret', app) <- checkFunctionApplication f' ft arg+  subsumes Nothing ret' ret+  return $ TypedValue True app ret check' v@(Var var) ty = do   Just moduleName <- checkCurrentModule <$> get-  ty1 <- lookupVariable moduleName var-  repl <- replaceAllTypeSynonyms ty1-  ty' <- replaceAllTypeSynonyms ty+  repl <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var+  ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty   v' <- subsumes (Just v) repl ty'   case v' of     Nothing -> throwError "Unable to check type subsumption"-    Just v'' -> return v''+    Just v'' -> return $ TypedValue True v'' ty' check' (TypedValue checkType val ty1) ty2 = do   Just moduleName <- checkCurrentModule <$> get   kind <- liftCheck $ kindOf moduleName ty1@@ -718,22 +777,22 @@     Nothing -> throwError "Unable to check type subsumption"     Just val'' -> do       val''' <- if checkType then check val'' ty1 else return val''-      return $ TypedValue True val''' ty1+      return $ TypedValue checkType (TypedValue True val''' ty1) ty2 check' (Case vals binders) ret = do   vals' <- mapM infer vals   let ts = map (\(TypedValue _ _ t) -> t) vals'   binders' <- checkBinders ts ret binders-  return $ Case vals' binders'+  return $ TypedValue True (Case vals' binders') ret check' (IfThenElse cond th el) ty = do   cond' <- check cond tyBoolean   th' <- check th ty   el' <- check el ty-  return $ IfThenElse cond' th' el'-check' (ObjectLiteral ps) (Object row) = do+  return $ TypedValue True (IfThenElse cond' th' el') ty+check' (ObjectLiteral ps) t@(Object row) = do   ensureNoDuplicateProperties ps   ps' <- checkProperties ps row False-  return $ ObjectLiteral ps'-check' (ObjectUpdate obj ps) (Object row) = do+  return $ TypedValue True (ObjectLiteral ps') t+check' (ObjectUpdate obj ps) t@(Object row) = do   ensureNoDuplicateProperties ps   us <- zip (map fst ps) <$> replicateM (length ps) fresh   let (propsToCheck, rest) = rowToList row@@ -741,27 +800,24 @@       remainingProps = filter (\(p, _) -> p `notElem` propsToRemove) propsToCheck   obj' <- check obj (Object (rowFromList (us ++ remainingProps, rest)))   ps' <- checkProperties ps row True-  return $ ObjectUpdate obj' ps'+  return $ TypedValue True (ObjectUpdate obj' ps') t check' (Accessor prop val) ty = do   rest <- fresh   val' <- check val (Object (RCons prop ty rest))-  return $ Accessor prop val'+  return $ TypedValue True (Accessor prop val') ty check' (Block ss) ret = do   (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss   guardWith "Block is missing a return statement" allCodePathsReturn-  return $ Block ss'+  return $ TypedValue True (Block ss') ret check' (Constructor c) ty = do   env <- getEnv   Just moduleName <- checkCurrentModule <$> get   case M.lookup (qualify moduleName c) (dataConstructors env) of     Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"     Just (ty1, _) -> do-      repl <- replaceAllTypeSynonyms ty1+      repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1       _ <- subsumes Nothing repl ty-      return $ Constructor c-check' val (SaturatedTypeSynonym name args) = do-  ty <- expandTypeSynonym name args-  check val ty+      return $ TypedValue True (Constructor c) ty check' val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty  -- |@@ -774,7 +830,7 @@   go [] [] REmpty = return []   go [] [] u@(TUnknown _) = do u =?= REmpty                                return []-  go [] [] (Skolem _) | lax = return []+  go [] [] (Skolem _ _) | lax = return []   go [] ((p, _): _) _ | lax = return []                       | otherwise = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have property " ++ p   go ((p,_):_) [] REmpty = throwError $ "Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row@@ -801,8 +857,8 @@ -- | -- Check the type of a function application, rethrowing errors to provide a better error message ---checkFunctionApplication :: Value -> Type -> Value -> Type -> UnifyT Type Check Value-checkFunctionApplication fn fnTy arg ret = rethrow errorMessage $ checkFunctionApplication' fn fnTy arg ret+checkFunctionApplication :: Value -> Type -> Value -> UnifyT Type Check (Type, Value)+checkFunctionApplication fn fnTy arg = rethrow errorMessage $ checkFunctionApplication' fn fnTy arg   where   errorMessage msg = "Error applying function of type "     ++ prettyPrintType fnTy@@ -812,34 +868,33 @@ -- | -- Check the type of a function application ---checkFunctionApplication' :: Value -> Type -> Value -> Type -> UnifyT Type Check Value-checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do+checkFunctionApplication' :: Value -> Type -> Value -> UnifyT Type Check (Type, Value)+checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg = do   tyFunction' =?= tyFunction   arg' <- check arg argTy-  _ <- subsumes Nothing retTy ret-  return $ App fn arg'-checkFunctionApplication' fn (ForAll ident ty) arg ret = do+  return (retTy, App fn arg')+checkFunctionApplication' fn (ForAll ident ty _) arg = do   replaced <- replaceVarWithUnknown ident ty-  checkFunctionApplication fn replaced arg ret-checkFunctionApplication' fn u@(TUnknown _) arg ret = do+  checkFunctionApplication fn replaced arg+checkFunctionApplication' fn u@(TUnknown _) arg = do   arg' <- do     TypedValue _ v t <- infer arg     TypedValue True v <$> replaceAllVarsWithUnknowns t   let ty = (\(TypedValue _ _ t) -> t) arg'+  ret <- fresh   u =?= function ty ret-  return $ App fn arg'-checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg ret = do-  ty <- expandTypeSynonym name tyArgs-  checkFunctionApplication fn ty arg ret-checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do+  return (ret, App fn arg')+checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg = do+  ty <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs+  checkFunctionApplication fn ty arg+checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg = do   env <- getEnv   dicts <- getTypeClassDictionaries   Just moduleName <- checkCurrentModule <$> get-  checkFunctionApplication' (foldl App fn (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) fnTy arg ret-checkFunctionApplication' _ fnTy arg ret = throwError $ "Applying a function of type "+  checkFunctionApplication' (foldl App fn (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) fnTy arg+checkFunctionApplication' _ fnTy arg = throwError $ "Cannot apply a function of type "   ++ prettyPrintType fnTy-  ++ " to argument(s) " ++ prettyPrintValue arg-  ++ " does not yield a value of type " ++ prettyPrintType ret ++ "."+  ++ " to argument " ++ prettyPrintValue arg  -- | -- Check whether one type subsumes another, rethrowing errors to provide a better error message@@ -857,18 +912,25 @@ -- Check whether one type subsumes another -- subsumes' :: Maybe Value -> Type -> Type -> UnifyT Type Check (Maybe Value)-subsumes' val (ForAll ident ty1) ty2 = do+subsumes' val (ForAll ident ty1 _) ty2 = do   replaced <- replaceVarWithUnknown ident ty1   subsumes val replaced ty2+subsumes' val ty1 (ForAll ident ty2 sco) =+  case sco of+    Just sco' -> do+      sko <- newSkolemConstant+      let sk = skolemize ident sko sco' ty2+      subsumes val ty1 sk+    Nothing -> throwError "Skolem variable scope is unspecified" subsumes' val (TypeApp (TypeApp f1 arg1) ret1) (TypeApp (TypeApp f2 arg2) ret2) | f1 == tyFunction && f2 == tyFunction = do   subsumes Nothing arg2 arg1   subsumes Nothing ret1 ret2   return val subsumes' val (SaturatedTypeSynonym name tyArgs) ty2 = do-  ty1 <- expandTypeSynonym name tyArgs+  ty1 <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs   subsumes val ty1 ty2 subsumes' val ty1 (SaturatedTypeSynonym name tyArgs) = do-  ty2 <- expandTypeSynonym name tyArgs+  ty2 <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs   subsumes val ty1 ty2 subsumes' (Just val) (ConstrainedType constraints ty1) ty2 = do   env <- getEnv
src/Language/PureScript/Types.hs view
@@ -25,6 +25,11 @@ import Language.PureScript.Names  -- |+-- An identifier for the scope of a skolem variable+--+newtype SkolemScope = SkolemScope { runSkolemScope :: Int } deriving (Show, Eq, Ord, Data, Typeable)++-- | -- The type of types -- data Type@@ -55,7 +60,7 @@   -- |   -- Forall quantifier   ---  | ForAll String Type+  | ForAll String Type (Maybe SkolemScope)   -- |   -- A type with a set of type class constraints   --@@ -63,7 +68,7 @@   -- |   -- A skolem constant   ---  | Skolem Int+  | Skolem Int SkolemScope   -- |   -- An empty row   --@@ -128,14 +133,14 @@ -- Check whether a type is a monotype -- isMonoType :: Type -> Bool-isMonoType (ForAll _ _) = False+isMonoType (ForAll _ _ _) = False isMonoType ty = True  -- | -- Universally quantify a type -- mkForAll :: [String] -> Type -> Type-mkForAll = flip . foldl . flip $ ForAll+mkForAll args ty = foldl (\t arg -> ForAll arg t Nothing) ty args  -- | -- The empty record type@@ -151,5 +156,5 @@   where   replaceTypeVar (TypeVar v) | v == name = t   replaceTypeVar other = other-  isShadowed (ForAll v _) | v == name = True+  isShadowed (ForAll v _ _) | v == name = True   isShadowed _ = False
tests/Main.hs view
@@ -39,7 +39,7 @@ readInput :: [FilePath] -> IO (Either ParseError [P.Module]) readInput inputFiles = fmap (fmap concat . sequence) $ forM inputFiles $ \inputFile -> do   text <- U.readFile inputFile-  return $ P.runIndentParser P.parseModules text+  return $ P.runIndentParser inputFile P.parseModules text  compile :: P.Options -> [FilePath] -> IO (Either String String) compile opts inputFiles = do