6954b06 · rowtype-yoga/purescript-native

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

Add support for rows in instance head under fundeps (#2451)

* Support rows in instance head under fundeps * Check determined class args by calculating contributing deps * Move determined arguments to TypeClassData and compute in 'smart constructor' * Update description of algorithm for computing determined type class args

commit6954b06d5e3316af4419b6594464c4ec2ec17aa8 authorLiam Goodacre <goodacre.liam@gmail.com> dateTue 6 Dec 2016, 04:36 (10 years ago) parent1d6934e

9 files changed+156−32

compare with golang

unifiedsplit

examples/failing/RowInInstanceNotDetermined0.purs+9 examples/failing/RowInInstanceNotDetermined1.purs+9 examples/failing/RowInInstanceNotDetermined2.purs+9 examples/passing/RowInInstanceHeadDetermined.purs+40 src/Language/PureScript/Environment.hs+53−2 src/Language/PureScript/Errors.hs+1−1 src/Language/PureScript/Externs.hs+1−1 src/Language/PureScript/Sugar/TypeClasses.hs+2−6 src/Language/PureScript/TypeChecker.hs+32−22

examples/failing/RowInInstanceNotDetermined0.pursnew file+9

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

1+-- @shouldFailWith InvalidInstanceHead

2+module Main where

4+import Prelude

6+-- no fundeps

7+class C a b

8+instance c :: C Unit {}

examples/failing/RowInInstanceNotDetermined1.pursnew file+9

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

1+-- @shouldFailWith InvalidInstanceHead

2+module Main where

4+import Prelude

6+-- `c` not mentioned in any fundeps

7+class C a b c | a -> b

8+instance c :: C Unit Unit {}

examples/failing/RowInInstanceNotDetermined2.pursnew file+9

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

1+-- @shouldFailWith InvalidInstanceHead

2+module Main where

4+import Prelude

6+-- `b` isn't determined by anything that `b` doesn't determine

7+class C a b | a -> b, b -> a

8+instance c :: C Unit {}

examples/passing/RowInInstanceHeadDetermined.pursnew file+40

@@ -0,0 +1,40 @@

1+module Main where

3+import Prelude

4+import Control.Monad.Eff.Console (log)

6+data Empty = Empty

7+data Cons = Cons

10+-- simple case

11+class Simple a b | a -> b where c :: a -> b

12+instance simple0 :: Simple Empty {} where c _ = {}

13+instance simple1 :: Simple Cons {foo :: Cons} where c cons = {foo: cons}

14+

15+

16+-- simple transitive example

17+class Transitive a b c | a -> b, b -> c where d :: a -> c

18+instance transitive :: Transitive Empty {} {} where d _ = {}

19+

20+

21+-- transitive example with cycles

22+class Cyclic a b c d | a -> b, b -> a

23+ , a -> c

24+ , c -> d, d -> c

25+instance cyclic :: Cyclic Empty Empty {} {}

26+

27+

28+-- Determined cycle

29+class DeterminedCycle a b c | a -> b

30+ , b -> c, c -> b

31+instance determinedCycle :: DeterminedCycle Empty {} {}

32+

33+

34+-- multiple determiners

35+class MultipleDeterminers a b c d | a b -> c d

36+instance multipleDeterminers :: MultipleDeterminers Empty Empty {} {}

37+

38+

39+main = log "Done"

40+

src/Language/PureScript/Environment.hs+53−2

@@ -7,9 +7,12 @@ import Prelude.Compat

77import Data.Aeson.TH

88import qualified Data.Aeson as A

99import qualified Data.Map as M

10+import qualified Data.Set as S

1011import Data.Maybe (fromMaybe)

1112import Data.Text (Text)

1213import qualified Data.Text as T

14+import Data.List (nub)

15+import qualified Data.Graph as G

1316

1417import Language.PureScript.Crash

1518import Language.PureScript.Kinds

@@ -48,6 +51,10 @@ data TypeClassData = TypeClassData

4851 -- are considered bound in the types appearing in these constraints.

4952 , typeClassDependencies :: [FunctionalDependency]

5053 -- ^ A list of functional dependencies for the type arguments of this class.

54+ , typeClassDeterminedArguments :: S.Set Int

55+ -- ^ A set of indexes of type argument that are fully determined by other

56+ -- arguments via functional dependencies. This can be computed from both

57+ -- typeClassArguments and typeClassDependencies.

5158 } deriving Show

5259

5360-- | A functional dependency indicates a relationship between two sets of

@@ -65,6 +72,50 @@ data FunctionalDependency = FunctionalDependency

6572initEnvironment :: Environment

6673initEnvironment = Environment M.empty primTypes M.empty M.empty M.empty primClasses

6774

75+-- |

76+-- A constructor for TypeClassData that computes which type class arguments are fully determined.

77+-- Fully determined means that this argument cannot be used when selecting a type class instance.

78+--

79+-- An example of the difference between determined and fully determined would be with the class:

80+-- ```class C a b c | a -> b, b -> a, b -> c```

81+-- In this case, `a` must differ when `b` differs, and vice versa - each is determined by the other.

82+-- Both `a` and `b` can be used in selecting a type class instance. However, `c` cannot - it is

83+-- fully determined by `a` and `b`.

84+--

85+-- Define a graph of type class arguments with edges being fundep determiners to determined.

86+-- An argument is fully determined if doesn't appear at the start of a path of strongly connected components.

87+-- An argument is not fully determined otherwise.

88+--

89+-- The way we compute this is by saying: an argument X is fully determined if there are arguments that

90+-- determine X that X does not determine. This is the same thing: everything X determines includes everything

91+-- in its SCC, and everything determining X is either before it in an SCC path, or in the same SCC.

92+makeTypeClassData

93+ :: [(Text, Maybe Kind)]

94+ -> [(Ident, Type)]

95+ -> [Constraint]

96+ -> [FunctionalDependency]

97+ -> TypeClassData

98+makeTypeClassData args m s deps = TypeClassData args m s deps determinedArgs

99+ where

100+ -- list all the edges in the graph: for each fundep an edge exists for each determiner to each determined

101+ contributingDeps = M.fromListWith (++) $ do

102+ fd <- deps

103+ src <- fdDeterminers fd

104+ (src, fdDetermined fd) : map (, []) (fdDetermined fd)

105+

106+ -- here we build a graph of which arguments determine other arguments

107+ (depGraph, _, fromKey) = G.graphFromEdges ((\(n, v) -> (n, n, nub v)) <$> M.toList contributingDeps)

108+

109+ -- do there exist any arguments that contribute to `arg` that `arg` doesn't contribute to

110+ isFunDepDetermined arg = case fromKey arg of

111+ Nothing -> False -- not mentioned in fundeps

112+ Just v -> let contributesToVar = G.reachable (G.transposeG depGraph) v

113+ varContributesTo = G.reachable depGraph v

114+ in any (\r -> not (r `elem` varContributesTo)) contributesToVar

115+

116+ -- find all the arguments that are determined

117+ determinedArgs = S.fromList $ filter isFunDepDetermined [0 .. length args - 1]

118+

68119-- |

69120-- The visibility of a name in scope

70121--

@@ -264,8 +315,8 @@ primTypes =

264315primClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData

265316primClasses =

266317 M.fromList

267− [ (primName "Partial", (TypeClassData [] [] [] []))

268− , (primName "Fail", (TypeClassData [("message", Just Symbol)] [] [] []))

318+ [ (primName "Partial", (makeTypeClassData [] [] [] []))

319+ , (primName "Fail", (makeTypeClassData [("message", Just Symbol)] [] [] []))

269320 ]

270321

271322-- |

src/Language/PureScript/Errors.hs+1−1

@@ -726,7 +726,7 @@ prettyPrintSingleError (PPEOptions codeColor full level showWiki) e = flip evalS

726726 renderSimpleErrorMessage (InvalidInstanceHead ty) =

727727 paras [ line "Type class instance head is invalid due to use of type"

728728 , markCodeBox $ indent $ typeAsBox ty

729− , line "All types appearing in instance declarations must be of the form T a_1 .. a_n, where each type a_i is of the same form."

729+ , line "All types appearing in instance declarations must be of the form T a_1 .. a_n, where each type a_i is of the same form, unless the type is fully determined by other type class arguments via functional dependencies."

730730 ]

731731 renderSimpleErrorMessage (TransitiveExportError x ys) =

732732 paras [ line $ "An export for " <> markCode (prettyPrintExport x) <> " requires the following to also be exported: "

src/Language/PureScript/Externs.hs+1−1

@@ -144,7 +144,7 @@ applyExternsFileToEnvironment ExternsFile{..} = flip (foldl' applyDecl) efDeclar

144144 applyDecl env (EDTypeSynonym pn args ty) = env { typeSynonyms = M.insert (qual pn) (args, ty) (typeSynonyms env) }

145145 applyDecl env (EDDataConstructor pn dTy tNm ty nms) = env { dataConstructors = M.insert (qual pn) (dTy, tNm, ty, nms) (dataConstructors env) }

146146 applyDecl env (EDValue ident ty) = env { names = M.insert (Qualified (Just efModuleName) ident) (ty, External, Defined) (names env) }

147− applyDecl env (EDClass pn args members cs deps) = env { typeClasses = M.insert (qual pn) (TypeClassData args members cs deps) (typeClasses env) }

147+ applyDecl env (EDClass pn args members cs deps) = env { typeClasses = M.insert (qual pn) (makeTypeClassData args members cs deps) (typeClasses env) }

148148 applyDecl env (EDInstance className ident tys cs) = env { typeClassDictionaries = updateMap (updateMap (M.insert (qual ident) dict) className) (Just efModuleName) (typeClassDictionaries env) }

149149 where

150150 dict :: NamedDict

src/Language/PureScript/Sugar/TypeClasses.hs+2−6

@@ -57,11 +57,7 @@ desugarTypeClasses externs = flip evalStateT initialState . traverse desugarModu

5757 -> ExternsDeclaration

5858 -> Maybe ((ModuleName, ProperName 'ClassName), TypeClassData)

5959 fromExternsDecl mn (EDClass name args members implies deps) = Just ((mn, name), typeClass) where

60− typeClass = TypeClassData { typeClassArguments = args

61− , typeClassMembers = members

62− , typeClassSuperclasses = implies

63− , typeClassDependencies = deps

64− }

60+ typeClass = makeTypeClassData args members implies deps

6561 fromExternsDecl _ _ = Nothing

6662

6763desugarModule

@@ -182,7 +178,7 @@ desugarDecl

182178desugarDecl mn exps = go

183179 where

184180 go d@(TypeClassDeclaration name args implies deps members) = do

185− modify (M.insert (mn, name) (TypeClassData args (map memberToNameAndType members) implies deps))

181+ modify (M.insert (mn, name) (makeTypeClassData args (map memberToNameAndType members) implies deps))

186182 return (Nothing, d : typeClassDictionaryDeclaration name args implies members : map (typeClassMemberToDictionaryAccessor mn name args) members)

187183 go (TypeInstanceDeclaration _ _ _ _ DerivedInstance) = internalError "Derived instanced should have been desugared"

188184 go d@(TypeInstanceDeclaration name deps className tys (ExplicitInstance members)) = do

src/Language/PureScript/TypeChecker.hs+32−22

@@ -22,6 +22,7 @@ import Data.Foldable (for_, traverse_)

2222import Data.List (nub, nubBy, (\\), sort, group)

2323import Data.Maybe

2424import qualified Data.Map as M

25+import qualified Data.Set as S

2526import Data.Monoid ((<>))

2627import qualified Data.Text as T

2728import Data.Text (Text)

@@ -124,12 +125,7 @@ addTypeClass moduleName pn args implies dependencies ds =

124125 modify $ \st -> st { checkEnv = (checkEnv st) { typeClasses = M.insert (Qualified (Just moduleName) pn) newClass (typeClasses . checkEnv $ st) } }

125126 where

126127 newClass :: TypeClassData

127− newClass =

128− TypeClassData { typeClassArguments = args

129− , typeClassMembers = map toPair ds

130− , typeClassSuperclasses = implies

131− , typeClassDependencies = dependencies

132− }

128+ newClass = makeTypeClassData args (map toPair ds) implies dependencies

133129

134130 toPair (TypeDeclaration ident ty) = (ident, ty)

135131 toPair (PositionedDeclaration _ _ d) = toPair d

@@ -155,18 +151,28 @@ checkDuplicateTypeArguments args = for_ firstDup $ \dup ->

155151 firstDup = listToMaybe $ args \\ nub args

156152

157153checkTypeClassInstance

158− :: (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

159− => ModuleName

154+ :: (MonadState CheckState m, MonadError MultipleErrors m)

155+ => TypeClassData

156+ -> Int -- ^ index of type class argument

160157 -> Type

161158 -> m ()

162−checkTypeClassInstance _ (TypeVar _) = return ()

163−checkTypeClassInstance _ (TypeLevelString _) = return ()

164−checkTypeClassInstance _ (TypeConstructor ctor) = do

165− env <- getEnv

166− when (ctor `M.member` typeSynonyms env) . throwError . errorMessage $ TypeSynonymInstance

167− return ()

168−checkTypeClassInstance m (TypeApp t1 t2) = checkTypeClassInstance m t1 >> checkTypeClassInstance m t2

169−checkTypeClassInstance _ ty = throwError . errorMessage $ InvalidInstanceHead ty

159+checkTypeClassInstance cls i = check where

160+ -- If the argument is determined via fundeps then we are less restrictive in

161+ -- what type is allowed. This is because the type cannot be used to influence

162+ -- which instance is selected. Currently the only weakened restriction is that

163+ -- row types are allowed in determined type class arguments.

164+ isFunDepDetermined = S.member i (typeClassDeterminedArguments cls)

165+ check = \case

166+ TypeVar _ -> return ()

167+ TypeLevelString _ -> return ()

168+ TypeConstructor ctor -> do

169+ env <- getEnv

170+ when (ctor `M.member` typeSynonyms env) . throwError . errorMessage $ TypeSynonymInstance

171+ return ()

172+ TypeApp t1 t2 -> check t1 >> check t2

173+ REmpty | isFunDepDetermined -> return ()

174+ RCons _ hd tl | isFunDepDetermined -> check hd >> check tl

175+ ty -> throwError . errorMessage $ InvalidInstanceHead ty

170176

171177-- |

172178-- Check that type synonyms are fully-applied in a type

@@ -283,12 +289,16 @@ typeCheckAll moduleName _ = traverse go

283289 addTypeClass moduleName pn args implies deps tys

284290 return d

285291 go (d@(TypeInstanceDeclaration dictName deps className tys body)) = rethrow (addHint (ErrorInInstance className tys)) $ do

286− traverse_ (checkTypeClassInstance moduleName) tys

287− checkOrphanInstance dictName className tys

288− _ <- traverseTypeInstanceBody checkInstanceMembers body

289− let dict = TypeClassDictionaryInScope (Qualified (Just moduleName) dictName) [] className tys (Just deps)

290− addTypeClassDictionaries (Just moduleName) . M.singleton className $ M.singleton (tcdValue dict) dict

291− return d

292+ env <- getEnv

293+ case M.lookup className (typeClasses env) of

294+ Nothing -> internalError "typeCheckAll: Encountered unknown type class in instance declaration"

295+ Just typeClass -> do

296+ sequence_ (zipWith (checkTypeClassInstance typeClass) [0..] tys)

297+ checkOrphanInstance dictName className tys

298+ _ <- traverseTypeInstanceBody checkInstanceMembers body

299+ let dict = TypeClassDictionaryInScope (Qualified (Just moduleName) dictName) [] className tys (Just deps)

300+ addTypeClassDictionaries (Just moduleName) . M.singleton className $ M.singleton (tcdValue dict) dict

301+ return d

292302 go (PositionedDeclaration pos com d) =

293303 warnAndRethrowWithPosition pos $ PositionedDeclaration pos com <$> go d

294304