git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Basic context simplification
fdc9435Phil Freeman
examples/passing/ContextSimplification.purs+7−3
compare with golang
unifiedsplit
@@ -1,9 +1,13 @@
1module Main where
1module Main where
2
2
3import Prelude
3import Prelude
4+import Control.Monad.Eff.Console
4
5
6+shout = log <<< (<> "!") <<< show
7+
5−-- Here, we should simplify the context so that only one Eq
8+-- Here, we should simplify the context so that only one Show
6-- constraint is added.
9-- constraint is added.
7−usesEqTwice x = if x == x then x == x else false
10+usesShowTwice true = shout
11+usesShowTwice false = print
8
12
9−main = Control.Monad.Eff.Console.log "Done"
13+main = usesShowTwice true "Done"
src/Language/PureScript/TypeChecker/Entailment.hs+51−17
@@ -4,7 +4,7 @@
4-- |
4-- |
5-- Type class entailment
5-- Type class entailment
6--
6--
7−module Language.PureScript.TypeChecker.Entailment (entails) where
7+module Language.PureScript.TypeChecker.Entailment (Context, replaceTypeClassDictionaries) where
8
8
9import Prelude ()
9import Prelude ()
10import Prelude.Compat
10import Prelude.Compat
@@ -16,8 +16,8 @@ import qualified Data.Map as M
16
16
17import Control.Arrow (Arrow(..))
17import Control.Arrow (Arrow(..))
18import Control.Monad.State
18import Control.Monad.State
19+import Control.Monad.Writer
19import Control.Monad.Error.Class (MonadError(..))
20import Control.Monad.Error.Class (MonadError(..))
20−import Control.Monad.Writer.Class (MonadWriter(..))
21import Control.Monad.Supply.Class (MonadSupply(..))
21import Control.Monad.Supply.Class (MonadSupply(..))
22
22
23import Language.PureScript.Crash
23import Language.PureScript.Crash
@@ -29,6 +29,30 @@ import Language.PureScript.TypeClassDictionaries
29import Language.PureScript.Types
29import Language.PureScript.Types
30import qualified Language.PureScript.Constants as C
30import qualified Language.PureScript.Constants as C
31
31
32+-- | The 'Context' tracks those constraints which can be satisfied.
33+type Context = M.Map (Maybe ModuleName)
34+ (M.Map (Qualified (ProperName 'ClassName))
35+ (M.Map (Qualified Ident)
36+ TypeClassDictionaryInScope))
37+
38+-- | Merge two type class contexts
39+combineContexts :: Context -> Context -> Context
40+combineContexts = M.unionWith (M.unionWith M.union)
41+
42+-- | Replace type class dictionary placeholders with inferred type class dictionaries
43+replaceTypeClassDictionaries
44+ :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
45+ => Bool
46+ -> ModuleName
47+ -> Expr
48+ -> m (Expr, [(Ident, Constraint)])
49+replaceTypeClassDictionaries shouldGeneralize mn =
50+ let (_, f, _) = everywhereOnValuesTopDownM return (WriterT . go) return
51+ in flip evalStateT M.empty . runWriterT . f
52+ where
53+ go (TypeClassDictionary constraint dicts) = entails shouldGeneralize mn dicts constraint
54+ go other = return (other, [])
55+
32-- |
56-- |
33-- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
57-- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
34-- return a type class dictionary reference.
58-- return a type class dictionary reference.
@@ -38,14 +62,14 @@ entails
38 . (Functor m, Applicative m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
62 . (Functor m, Applicative m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
39 => Bool
63 => Bool
40 -> ModuleName
64 -> ModuleName
41− -> M.Map (Maybe ModuleName) (M.Map (Qualified (ProperName 'ClassName)) (M.Map (Qualified Ident) TypeClassDictionaryInScope))
65+ -> Context
42 -> Constraint
66 -> Constraint
43− -> m (Expr, [(Ident, Constraint)])
67+ -> StateT Context m (Expr, [(Ident, Constraint)])
44entails shouldGeneralize moduleName context = solve
68entails shouldGeneralize moduleName context = solve
45 where
69 where
46− forClassName :: Qualified (ProperName 'ClassName) -> [Type] -> [TypeClassDictionaryInScope]
70+ forClassName :: Context -> Qualified (ProperName 'ClassName) -> [Type] -> [TypeClassDictionaryInScope]
47− forClassName cn@(Qualified (Just mn) _) tys = concatMap (findDicts cn) (Nothing : Just mn : map Just (mapMaybe ctorModules tys))
71+ forClassName ctx cn@(Qualified (Just mn) _) tys = concatMap (findDicts ctx cn) (Nothing : Just mn : map Just (mapMaybe ctorModules tys))
48− forClassName _ _ = internalError "forClassName: expected qualified class name"
72+ forClassName _ _ _ = internalError "forClassName: expected qualified class name"
49
73
50 ctorModules :: Type -> Maybe ModuleName
74 ctorModules :: Type -> Maybe ModuleName
51 ctorModules (TypeConstructor (Qualified (Just mn) _)) = Just mn
75 ctorModules (TypeConstructor (Qualified (Just mn) _)) = Just mn
@@ -53,23 +77,25 @@ entails shouldGeneralize moduleName context = solve
53 ctorModules (TypeApp ty _) = ctorModules ty
77 ctorModules (TypeApp ty _) = ctorModules ty
54 ctorModules _ = Nothing
78 ctorModules _ = Nothing
55
79
56− findDicts :: Qualified (ProperName 'ClassName) -> Maybe ModuleName -> [TypeClassDictionaryInScope]
80+ findDicts :: Context -> Qualified (ProperName 'ClassName) -> Maybe ModuleName -> [TypeClassDictionaryInScope]
57− findDicts cn = maybe [] M.elems . (>>= M.lookup cn) . flip M.lookup context
81+ findDicts ctx cn = maybe [] M.elems . (>>= M.lookup cn) . flip M.lookup ctx
58
82
59− solve :: Constraint -> m (Expr, [(Ident, Constraint)])
83+ solve :: Constraint -> StateT Context m (Expr, [(Ident, Constraint)])
60 solve (className, tys) = do
84 solve (className, tys) = do
61 (dict, unsolved) <- go 0 className tys
85 (dict, unsolved) <- go 0 className tys
62 return (dictionaryValueToValue dict, unsolved)
86 return (dictionaryValueToValue dict, unsolved)
63 where
87 where
64− go :: Int -> Qualified (ProperName 'ClassName) -> [Type] -> m (DictionaryValue, [(Ident, Constraint)])
88+ go :: Int -> Qualified (ProperName 'ClassName) -> [Type] -> StateT Context m (DictionaryValue, [(Ident, Constraint)])
65 go work className' tys' | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'
89 go work className' tys' | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'
66 go work className' tys' = do
90 go work className' tys' = do
91+ -- Get the inferred constraint context so far, and merge it with the global context
92+ inferred <- get
67 let instances = do
93 let instances = do
68− tcd <- forClassName className' tys'
94+ tcd <- forClassName (combineContexts context inferred) className' tys'
69 -- Make sure the type unifies with the type in the type instance definition
95 -- Make sure the type unifies with the type in the type instance definition
70 subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName) tys' (tcdInstanceTypes tcd)
96 subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName) tys' (tcdInstanceTypes tcd)
71 return (subst, tcd)
97 return (subst, tcd)
72− solution <- unique instances
98+ solution <- lift $ unique instances
73 case solution of
99 case solution of
74 Left (subst, tcd) -> do
100 Left (subst, tcd) -> do
75 -- Solve any necessary subgoals
101 -- Solve any necessary subgoals
@@ -78,9 +104,16 @@ entails shouldGeneralize moduleName context = solve
78 (mkDictionary (tcdName tcd) args)
104 (mkDictionary (tcdName tcd) args)
79 (tcdPath tcd)
105 (tcdPath tcd)
80 return (match, unsolved)
106 return (match, unsolved)
81− Right unsolved@(Qualified _ (ProperName unsolvedClassName), _) -> do
107+ Right unsolved@(unsolvedClassName@(Qualified _ pn), unsolvedTys) -> do
108+ -- Generate a fresh name for the unsolved constraint's new dictionary
82− ident <- freshIdent ("dict" ++ unsolvedClassName)
109+ ident <- freshIdent ("dict" ++ runProperName pn)
110+ let qident = Qualified Nothing ident
111+ -- Store the new dictionary in the Context so that we can solve this goal in
112+ -- future.
113+ let newDict = TypeClassDictionaryInScope qident [] unsolvedClassName unsolvedTys Nothing
114+ newContext = M.singleton Nothing (M.singleton unsolvedClassName (M.singleton qident newDict))
115+ modify (combineContexts newContext)
83− return (LocalDictionaryValue (Qualified Nothing ident), [(ident, unsolved)])
116+ return (LocalDictionaryValue qident, [(ident, unsolved)])
84 where
117 where
85
118
86 unique :: [(a, TypeClassDictionaryInScope)] -> m (Either (a, TypeClassDictionaryInScope) Constraint)
119 unique :: [(a, TypeClassDictionaryInScope)] -> m (Either (a, TypeClassDictionaryInScope) Constraint)
@@ -112,7 +145,7 @@ entails shouldGeneralize moduleName context = solve
112 -- Create dictionaries for subgoals which still need to be solved by calling go recursively
145 -- Create dictionaries for subgoals which still need to be solved by calling go recursively
113 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
146 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
114 -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
147 -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
115− solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> m (Maybe [DictionaryValue], [(Ident, Constraint)])
148+ solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> StateT Context m (Maybe [DictionaryValue], [(Ident, Constraint)])
116 solveSubgoals _ Nothing = return (Nothing, [])
149 solveSubgoals _ Nothing = return (Nothing, [])
117 solveSubgoals subst (Just subgoals) = do
150 solveSubgoals subst (Just subgoals) = do
118 zipped <- traverse (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals
151 zipped <- traverse (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals
@@ -149,6 +182,7 @@ entails shouldGeneralize moduleName context = solve
149-- and return a substitution from type variables to types which makes the type heads unify.
182-- and return a substitution from type variables to types which makes the type heads unify.
150--
183--
151typeHeadsAreEqual :: ModuleName -> Type -> Type -> Maybe [(String, Type)]
184typeHeadsAreEqual :: ModuleName -> Type -> Type -> Maybe [(String, Type)]
185+typeHeadsAreEqual _ (TUnknown u1) (TUnknown u2) | u1 == u2 = Just []
152typeHeadsAreEqual _ (Skolem _ s1 _ _) (Skolem _ s2 _ _) | s1 == s2 = Just []
186typeHeadsAreEqual _ (Skolem _ s1 _ _) (Skolem _ s2 _ _) | s1 == s2 = Just []
153typeHeadsAreEqual _ t (TypeVar v) = Just [(v, t)]
187typeHeadsAreEqual _ t (TypeVar v) = Just [(v, t)]
154typeHeadsAreEqual _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
188typeHeadsAreEqual _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
src/Language/PureScript/TypeChecker/Types.hs−15
@@ -40,7 +40,6 @@ import Control.Monad.State.Class (MonadState(..), gets)
40import Control.Monad.Supply.Class (MonadSupply)
40import Control.Monad.Supply.Class (MonadSupply)
41import Control.Monad.Error.Class (MonadError(..))
41import Control.Monad.Error.Class (MonadError(..))
42import Control.Monad.Writer.Class (MonadWriter(..))
42import Control.Monad.Writer.Class (MonadWriter(..))
43−import Control.Monad.Trans.Writer (WriterT(..))
44
43
45import Language.PureScript.Crash
44import Language.PureScript.Crash
46import Language.PureScript.AST
45import Language.PureScript.AST
@@ -181,20 +180,6 @@ overTypes f = let (_, f', _) = everywhereOnValues id g id in f'
181 g (TypeClassDictionary (nm, tys) sco) = TypeClassDictionary (nm, map f tys) sco
180 g (TypeClassDictionary (nm, tys) sco) = TypeClassDictionary (nm, map f tys) sco
182 g other = other
181 g other = other
183
182
184−-- | Replace type class dictionary placeholders with inferred type class dictionaries
185−replaceTypeClassDictionaries ::
186− (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m) =>
187− Bool ->
188− ModuleName ->
189− Expr ->
190− m (Expr, [(Ident, Constraint)])
191−replaceTypeClassDictionaries shouldGeneralize mn =
192− let (_, f, _) = everywhereOnValuesTopDownM return (WriterT . go) return
193− in runWriterT . f
194− where
195− go (TypeClassDictionary constraint dicts) = entails shouldGeneralize mn dicts constraint
196− go other = return (other, [])
197−
198-- | Check the kind of a type, failing if it is not of kind *.
183-- | Check the kind of a type, failing if it is not of kind *.
199checkTypeKind ::
184checkTypeKind ::
200 (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m) =>
185 (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m) =>