2372665 · rowtype-yoga/purescript-native

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

on golang help sign in

Scoped type variables #347

2372665Phil Freeman12 years ago

examples/passing/ScopedTypeVariables.pursnew file+9

compare with golang

unifiedsplit

@@ -0,0 +1,9 @@

1+module Main where

3+test1 :: forall a. (a -> a) -> a -> a

4+test1 f x = g (g x)

5+ where

6+ g :: a -> a

7+ g y = f (f y)

9+main = Debug.Trace.trace "Done"

src/Language/PureScript/Environment.hs+6−1

@@ -136,7 +136,12 @@ data TypeKind

136 -- |

137 -- A local type variable

138 --

139+ | LocalTypeVariable

140+ -- |

141+ -- A scoped type variable

142+ --

143+ | ScopedTypeVar Type

139− | LocalTypeVariable deriving (Show, Eq, Data, Typeable)

144+ deriving (Show, Eq, Data, Typeable)

140

145

141-- |

146-- |

142-- The type ('data' or 'newtype') of a data type declaration

147-- The type ('data' or 'newtype') of a data type declaration

src/Language/PureScript/TypeChecker/Kinds.hs+69−42

@@ -14,19 +14,22 @@

14-----------------------------------------------------------------------------

16{-# OPTIONS_GHC -fno-warn-orphans #-}

17−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

17+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TupleSections #-}

19module Language.PureScript.TypeChecker.Kinds (

20 kindOf,

21+ kindOfWithScopedVars,

21 kindsOf,

22 kindsOf,

22 kindsOfAll

23 kindsOfAll

23) where

24) where

25import Data.Maybe (fromMaybe)

26import Data.Maybe (fromMaybe)

26import Data.Monoid ((<>))

27import Data.Monoid ((<>))

28+

27import qualified Data.HashMap.Strict as H

29import qualified Data.HashMap.Strict as H

28import qualified Data.Map as M

30import qualified Data.Map as M

32+import Control.Arrow (second)

30import Control.Applicative

33import Control.Applicative

31import Control.Monad.Error

34import Control.Monad.Error

32import Control.Monad.State

35import Control.Monad.State

@@ -69,11 +72,19 @@ instance Unifiable Check Kind where

69-- Infer the kind of a single type

72-- Infer the kind of a single type

70--

73--

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

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

72−kindOf _ ty =

75+kindOf _ ty = fst <$> kindOfWithScopedVars ty

76+

77+-- |

78+-- Infer the kind of a single type, returning the kinds of any scoped type variables

79+--

80+kindOfWithScopedVars :: Type -> Check (Kind, [(String, Kind)])

81+kindOfWithScopedVars ty =

73 rethrow (mkErrorStack "Error checking kind" (Just (TypeError ty)) <>) $

82 rethrow (mkErrorStack "Error checking kind" (Just (TypeError ty)) <>) $

74− fmap (starIfUnknown . tidyUp) . liftUnify $ infer ty

83+ fmap tidyUp . liftUnify $ infer ty

75 where

84 where

76− tidyUp (k, sub) = sub $? k

85+ tidyUp ((k, args), sub) = ( starIfUnknown (sub $? k)

86+ , map (second (starIfUnknown . (sub $?))) args

87+ )

78-- |

89-- |

79-- Infer the kind of a type constructor with a collection of arguments and a collection of associated data constructors

90-- Infer the kind of a type constructor with a collection of arguments and a collection of associated data constructors

@@ -125,7 +136,7 @@ kindsOfAll moduleName syns tys = fmap tidyUp . liftUnify $ do

125--

136--

126solveTypes :: Bool -> [Type] -> [Kind] -> Kind -> UnifyT Kind Check Kind

137solveTypes :: Bool -> [Type] -> [Kind] -> Kind -> UnifyT Kind Check Kind

127solveTypes isData ts kargs tyCon = do

138solveTypes isData ts kargs tyCon = do

128− ks <- mapM infer ts

139+ ks <- mapM (fmap fst . infer) ts

129 when isData $ do

140 when isData $ do

130 tyCon =?= foldr FunKind Star kargs

141 tyCon =?= foldr FunKind Star kargs

131 forM_ ks $ \k -> k =?= Star

142 forM_ ks $ \k -> k =?= Star

@@ -145,48 +156,64 @@ starIfUnknown k = k

145-- |

156-- |

146-- Infer a kind for a type

157-- Infer a kind for a type

147--

158--

148−infer :: Type -> UnifyT Kind Check Kind

159+infer :: Type -> UnifyT Kind Check (Kind, [(String, Kind)])

149infer ty = rethrow (mkErrorStack "Error inferring type of value" (Just (TypeError ty)) <>) $ infer' ty

160infer ty = rethrow (mkErrorStack "Error inferring type of value" (Just (TypeError ty)) <>) $ infer' ty

150

161

151−infer' :: Type -> UnifyT Kind Check Kind

162+infer' :: Type -> UnifyT Kind Check (Kind, [(String, Kind)])

152−infer' TypeWildcard = fresh

153−infer' (TypeVar v) = do

154− Just moduleName <- checkCurrentModule <$> get

155− UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))

156−infer' c@(TypeConstructor v) = do

157− env <- liftCheck getEnv

158− case M.lookup v (types env) of

159− Nothing -> UnifyT . lift . throwError $ mkErrorStack "Unknown type constructor" (Just (TypeError c))

160− Just (kind, _) -> return kind

161−infer' (TypeApp t1 t2) = do

162− k0 <- fresh

163− k1 <- infer t1

164− k2 <- infer t2

165− k1 =?= FunKind k2 k0

166− return k0

167infer' (ForAll ident ty _) = do

163infer' (ForAll ident ty _) = do

168 k1 <- fresh

164 k1 <- fresh

169 Just moduleName <- checkCurrentModule <$> get

165 Just moduleName <- checkCurrentModule <$> get

170− k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty

166+ (k2, args) <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty

171 k2 =?= Star

167 k2 =?= Star

172− return Star

168+ return (Star, (ident, k1) : args)

173−infer' REmpty = do

174− k <- fresh

175− return $ Row k

176−infer' (RCons _ ty row) = do

177− k1 <- infer ty

178− k2 <- infer row

179− k2 =?= Row k1

180− return $ Row k1

181−infer' (ConstrainedType deps ty) = do

182− forM_ deps $ \(className, tys) -> do

183− _ <- infer $ foldl TypeApp (TypeConstructor className) tys

184− return ()

185− k <- infer ty

186− k =?= Star

187− return Star

188infer' (KindedType ty k) = do

169infer' (KindedType ty k) = do

189− k' <- infer ty

170+ (k', args) <- infer ty

190 k =?= k'

171 k =?= k'

191− return k'

172+ return (k', args)

173+infer' other = (, []) <$> go other

174+ where

175+ go :: Type -> UnifyT Kind Check Kind

176+ go (ForAll ident ty _) = do

177+ k1 <- fresh

178+ Just moduleName <- checkCurrentModule <$> get

179+ k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ go ty

180+ k2 =?= Star

181+ return Star

182+ go (KindedType ty k) = do

183+ k' <- go ty

184+ k =?= k'

185+ return k'

186+ go TypeWildcard = fresh

187+ go (TypeVar v) = do

188+ Just moduleName <- checkCurrentModule <$> get

189+ UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))

190+ go (Skolem v _ _) = do

191+ Just moduleName <- checkCurrentModule <$> get

192+ UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))

193+ go c@(TypeConstructor v) = do

194+ env <- liftCheck getEnv

195+ case M.lookup v (types env) of

196+ Nothing -> UnifyT . lift . throwError $ mkErrorStack "Unknown type constructor" (Just (TypeError c))

197+ Just (kind, _) -> return kind

198+ go (TypeApp t1 t2) = do

199+ k0 <- fresh

200+ k1 <- go t1

201+ k2 <- go t2

202+ k1 =?= FunKind k2 k0

203+ return k0

204+ go REmpty = do

205+ k <- fresh

206+ return $ Row k

207+ go (RCons _ ty row) = do

208+ k1 <- go ty

209+ k2 <- go row

210+ k2 =?= Row k1

211+ return $ Row k1

212+ go (ConstrainedType deps ty) = do

213+ forM_ deps $ \(className, tys) -> do

214+ _ <- go $ foldl TypeApp (TypeConstructor className) tys

215+ return ()

216+ k <- go ty

217+ k =?= Star

218+ return Star

192−infer' _ = error "Invalid argument to infer"

219+ go _ = error "Invalid argument to infer"

src/Language/PureScript/TypeChecker/Monad.hs+6

@@ -56,6 +56,12 @@ bindTypes newNames action = do

56 modify $ \st -> st { checkEnv = (checkEnv st) { types = types . checkEnv $ orig } }

57 return a

59+-- |

60+-- Temporarily bind a collection of names to types

61+--

62+withScopedTypeVars :: (Functor m, MonadState CheckState m) => ModuleName -> [(String, Kind)] -> m a -> m a

63+withScopedTypeVars mn ks = bindTypes (M.fromList (map (\(name, k) -> (Qualified (Just mn) (ProperName name), (k, ScopedTypeVar (TypeVar name)))) ks))

64+

59-- |

65-- |

60-- Temporarily make a collection of type class dictionaries available

66-- Temporarily make a collection of type class dictionaries available

61--

67--

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

@@ -71,6 +71,7 @@ skolemizeTypesInValue :: String -> Int -> SkolemScope -> Expr -> Expr

71skolemizeTypesInValue ident sko scope = let (_, f, _) = everywhereOnValues id go id in f

72 where

73 go (SuperClassDictionary c ts) = SuperClassDictionary c (map (skolemize ident sko scope) ts)

74+ go (TypedValue check val ty) = TypedValue check val (skolemize ident sko scope ty)

74 go other = other

75 go other = other

76-- |

77-- |

src/Language/PureScript/TypeChecker/Types.hs+3−3

@@ -129,16 +129,16 @@ typeDictionaryForBindingGroup moduleName vals = do

129 return (untyped, typed, dict, untypedDict)

130

131checkTypedBindingGroupElement :: ModuleName -> (Ident, (Expr, Type, Bool)) -> TypeData -> UnifyT Type Check (Ident, (Expr, Type))

132−checkTypedBindingGroupElement moduleName (ident, (val', ty, checkType)) dict = do

132+checkTypedBindingGroupElement mn (ident, (val', ty, checkType)) dict = do

133 -- Replace type wildcards

134 ty' <- replaceTypeWildcards ty

135 -- Kind check

136− kind <- liftCheck $ kindOf moduleName ty

136+ (kind, args) <- liftCheck $ kindOfWithScopedVars ty

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

138 -- Check the type with the new names in scope

139 ty'' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty'

140 val'' <- if checkType

141− then bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''

141+ then withScopedTypeVars mn args $ bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''

142 else return (TypedValue False val' ty'')

143 return (ident, (val'', ty''))

144