3ed6f05 · rowtype-yoga/purescript-native

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

on golang help sign in

Infer types with class constraints (work in progress)

3ed6f05Phil Freeman11 years ago

src/Language/PureScript/TypeChecker/Entailment.hs+35−21

compare with golang

unifiedsplit

@@ -18,6 +18,7 @@ import Control.Arrow (Arrow(..))

18import Control.Monad.State

19import Control.Monad.Error.Class (MonadError(..))

20import Control.Monad.Writer.Class (MonadWriter(..))

21+import Control.Monad.Supply.Class (MonadSupply(..))

22import Language.PureScript.Crash

23import Language.PureScript.Crash

23import Language.PureScript.AST

24import Language.PureScript.AST

@@ -34,11 +35,11 @@ import qualified Language.PureScript.Constants as C

34--

35--

35entails

36entails

36 :: forall m

37 :: forall m

37− . (Functor m, Applicative m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

38+ . (Functor m, Applicative m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)

38 => ModuleName

39 => ModuleName

39 -> M.Map (Maybe ModuleName) (M.Map (Qualified (ProperName 'ClassName)) (M.Map (Qualified Ident) TypeClassDictionaryInScope))

40 -> M.Map (Maybe ModuleName) (M.Map (Qualified (ProperName 'ClassName)) (M.Map (Qualified Ident) TypeClassDictionaryInScope))

40 -> Constraint

41 -> Constraint

41− -> m Expr

42+ -> m (Expr, [(Ident, Constraint)])

42entails moduleName context = solve

43entails moduleName context = solve

43 where

44 where

44 forClassName :: Qualified (ProperName 'ClassName) -> [Type] -> [TypeClassDictionaryInScope]

45 forClassName :: Qualified (ProperName 'ClassName) -> [Type] -> [TypeClassDictionaryInScope]

@@ -54,12 +55,12 @@ entails moduleName context = solve

54 findDicts :: Qualified (ProperName 'ClassName) -> Maybe ModuleName -> [TypeClassDictionaryInScope]

55 findDicts :: Qualified (ProperName 'ClassName) -> Maybe ModuleName -> [TypeClassDictionaryInScope]

55 findDicts cn = maybe [] M.elems . (>>= M.lookup cn) . flip M.lookup context

56 findDicts cn = maybe [] M.elems . (>>= M.lookup cn) . flip M.lookup context

57− solve :: Constraint -> m Expr

58+ solve :: Constraint -> m (Expr, [(Ident, Constraint)])

58 solve (className, tys) = do

59 solve (className, tys) = do

59− dict <- go 0 className tys

60+ (dict, unsolved) <- go 0 className tys

60− return $ dictionaryValueToValue dict

61+ return (dictionaryValueToValue dict, unsolved)

61 where

62 where

62− go :: Int -> Qualified (ProperName 'ClassName) -> [Type] -> m DictionaryValue

63+ go :: Int -> Qualified (ProperName 'ClassName) -> [Type] -> m (DictionaryValue, [(Ident, Constraint)])

63 go work className' tys' | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'

64 go work className' tys' | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'

64 go work className' tys' = do

65 go work className' tys' = do

65 let instances = do

66 let instances = do

@@ -67,21 +68,33 @@ entails moduleName context = solve

67 -- Make sure the type unifies with the type in the type instance definition

68 -- Make sure the type unifies with the type in the type instance definition

68 subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName) tys' (tcdInstanceTypes tcd)

69 subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName) tys' (tcdInstanceTypes tcd)

69 return (subst, tcd)

70 return (subst, tcd)

70− (subst, tcd) <- unique instances

71+ solution <- unique instances

72+ case solution of

73+ Left (subst, tcd) -> do

71− -- Solve any necessary subgoals

74+ -- Solve any necessary subgoals

72− args <- solveSubgoals subst (tcdDependencies tcd)

75+ (args, unsolved) <- solveSubgoals subst (tcdDependencies tcd)

73− return $ foldr (\(superclassName, index) dict -> SubclassDictionaryValue dict superclassName index)

76+ let match = foldr (\(superclassName, index) dict -> SubclassDictionaryValue dict superclassName index)

74− (mkDictionary (tcdName tcd) args)

77+ (mkDictionary (tcdName tcd) args)

75− (tcdPath tcd)

78+ (tcdPath tcd)

79+ return (match, unsolved)

80+ Right unsolved@(Qualified _ (ProperName unsolvedClassName), _) -> do

81+ ident <- freshIdent ("dict" ++ unsolvedClassName)

82+ return (LocalDictionaryValue (Qualified Nothing ident), [(ident, unsolved)])

76 where

83 where

78− unique :: [(a, TypeClassDictionaryInScope)] -> m (a, TypeClassDictionaryInScope)

85+ unique :: [(a, TypeClassDictionaryInScope)] -> m (Either (a, TypeClassDictionaryInScope) Constraint)

86+ unique [] | all canBeGeneralized tys' = return $ Right (className, tys)

79− unique [] = throwError . errorMessage $ NoInstanceFound className' tys'

87+ | otherwise = throwError . errorMessage $ NoInstanceFound className' tys'

80− unique [a] = return a

88+ unique [a] = return $ Left a

81 unique tcds | pairwise overlapping (map snd tcds) = do

89 unique tcds | pairwise overlapping (map snd tcds) = do

82 tell . errorMessage $ OverlappingInstances className' tys' (map (tcdName . snd) tcds)

90 tell . errorMessage $ OverlappingInstances className' tys' (map (tcdName . snd) tcds)

83− return (head tcds)

91+ return $ Left (head tcds)

84− | otherwise = return (minimumBy (compare `on` length . tcdPath . snd) tcds)

92+ | otherwise = return $ Left (minimumBy (compare `on` length . tcdPath . snd) tcds)

93+

94+ canBeGeneralized :: Type -> Bool

95+ canBeGeneralized TUnknown{} = True

96+ canBeGeneralized Skolem{} = True

97+ canBeGeneralized _ = False

86 -- |

99 -- |

87 -- Check if two dictionaries are overlapping

100 -- Check if two dictionaries are overlapping

@@ -98,11 +111,12 @@ entails moduleName context = solve

98 -- Create dictionaries for subgoals which still need to be solved by calling go recursively

111 -- Create dictionaries for subgoals which still need to be solved by calling go recursively

99 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type

112 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type

100 -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.

113 -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.

101− solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> m (Maybe [DictionaryValue])

114+ solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> m (Maybe [DictionaryValue], [(Ident, Constraint)])

102− solveSubgoals _ Nothing = return Nothing

115+ solveSubgoals _ Nothing = return (Nothing, [])

103 solveSubgoals subst (Just subgoals) = do

116 solveSubgoals subst (Just subgoals) = do

104− dict <- traverse (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals

117+ zipped <- traverse (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals

118+ let (dicts, unsolved) = unzip zipped

105− return $ Just dict

119+ return (Just dicts, concat unsolved)

106

120

107 -- Make a dictionary from subgoal dictionaries by applying the correct function

121 -- Make a dictionary from subgoal dictionaries by applying the correct function

108 mkDictionary :: Qualified Ident -> Maybe [DictionaryValue] -> DictionaryValue

122 mkDictionary :: Qualified Ident -> Maybe [DictionaryValue] -> DictionaryValue

src/Language/PureScript/TypeChecker/Types.hs+11−7

@@ -39,6 +39,7 @@ import Control.Monad.State.Class (MonadState(..), gets)

39import Control.Monad.Supply.Class (MonadSupply)

40import Control.Monad.Error.Class (MonadError(..))

41import Control.Monad.Writer.Class (MonadWriter(..))

42+import Control.Monad.Trans.Writer (WriterT(..))

43import Language.PureScript.Crash

44import Language.PureScript.Crash

44import Language.PureScript.AST

45import Language.PureScript.AST

@@ -74,13 +75,16 @@ typesOf moduleName vals = do

75 forM tys $ \(ident, (val, ty)) -> do

76 forM tys $ \(ident, (val, ty)) -> do

76 -- Replace type class dictionary placeholders with actual dictionaries

77 -- Replace type class dictionary placeholders with actual dictionaries

77− val' <- replaceTypeClassDictionaries moduleName val

78+ (val', unsolved) <- replaceTypeClassDictionaries moduleName val

78 -- Check skolem variables did not escape their scope

79 -- Check skolem variables did not escape their scope

79 skolemEscapeCheck val'

80 skolemEscapeCheck val'

80 -- Check rows do not contain duplicate labels

81 -- Check rows do not contain duplicate labels

81 checkDuplicateLabels val'

82 checkDuplicateLabels val'

82− return (ident, (val', varIfUnknown ty))

83+ return (ident, (foldr (Abs . Left) val' (map fst unsolved), varIfUnknown (constrain unsolved ty)))

83 where

84 where

85+ -- | Generalize over any unsolved constraints

86+ constrain [] = id

87+ constrain cs = ConstrainedType (map snd cs)

84 -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values

88 -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values

85 tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (substituteType sub) val, substituteType sub ty))) ts

89 tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (substituteType sub) val, substituteType sub ty))) ts

86 -- Replace all the wildcards types with their inferred types

90 -- Replace all the wildcards types with their inferred types

@@ -168,16 +172,16 @@ overTypes f = let (_, f', _) = everywhereOnValues id g id in f'

168

172

169-- | Replace type class dictionary placeholders with inferred type class dictionaries

173-- | Replace type class dictionary placeholders with inferred type class dictionaries

170replaceTypeClassDictionaries ::

174replaceTypeClassDictionaries ::

171− (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

175+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m) =>

172 ModuleName ->

176 ModuleName ->

173 Expr ->

177 Expr ->

174− m Expr

178+ m (Expr, [(Ident, Constraint)])

175replaceTypeClassDictionaries mn =

179replaceTypeClassDictionaries mn =

176− let (_, f, _) = everywhereOnValuesTopDownM return go return

180+ let (_, f, _) = everywhereOnValuesTopDownM return (WriterT . go) return

177− in f

181+ in runWriterT . f

178 where

182 where

179 go (TypeClassDictionary constraint dicts) = entails mn dicts constraint

183 go (TypeClassDictionary constraint dicts) = entails mn dicts constraint

180− go other = return other

184+ go other = return (other, [])

181

185

182-- | Check the kind of a type, failing if it is not of kind *.

186-- | Check the kind of a type, failing if it is not of kind *.

183checkTypeKind ::

187checkTypeKind ::