Add support for rows in instance head under fundeps #2451

LiamGoodacre · 2016-11-26T15:11:05Z

LiamGoodacre · 2016-11-26T15:12:36Z

src/Language/PureScript/TypeChecker.hs

-    return d
+    env <- getEnv
+    case M.lookup className (typeClasses env) of
+      Nothing -> internalError "typeCheckAll: Encountered unknown type class in instance declaration"


Am I correct in the assumption that by this point the referenced type class should already have been added to the environment?

Yes, I believe so.

paf31 · 2016-11-28T17:32:22Z

src/Language/PureScript/Errors.hs

@@ -724,7 +724,7 @@ prettyPrintSingleError (PPEOptions codeColor full level showWiki) e = flip evalS
    renderSimpleErrorMessage (InvalidInstanceHead ty) =
      paras [ line "Type class instance head is invalid due to use of type"
            , markCodeBox $ indent $ typeAsBox ty
-            , 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."
+            , 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."


Wording nitpick: I'd use a comma or parens here rather than a period. Although I wonder if we should just link to the wiki for further details here.

paf31 · 2016-11-28T17:36:53Z

src/Language/PureScript/TypeChecker.hs

+  isDeterminedInGroup fd = not (i `elem` fdDeterminers fd) && (i `elem` fdDetermined fd)
+
+  -- is this argument fully determined via fundeps
+  isFunDepDetermined = Just (All True) == foldMap (Just . All . isDeterminedInGroup) (typeClassDependencies cls)


I don't think this needs to be determined by all fundeps, just by some type variable which is not itself determined. This means that variable must be solved by the solver, which means that we know the variable we care about will be determined.

Eventually, we might want to allow the variable to be determined transitively (you have an example where this would be useful), but we don't need to deal with that yet.

Yeah I messed this up. Hmm, shouldn't it be: if the type is detemined in at least one fundep and never a determiner? For example in class C a b c | a -> b, b -> c we should allow rows in c right? However this sounds like it goes against what you said. Or is that the transitive case you're talking about?

paf31 · 2016-11-28T17:37:47Z

src/Language/PureScript/TypeChecker.hs

+      return ()
+    TypeApp t1 t2 -> check t1 >> check t2
+    REmpty | isFunDepDetermined -> return ()
+    RCons _ hd tl | isFunDepDetermined -> check hd >> check tl


You'll keep performing the check here for each RCons. Maybe pull this out into a checkRow function?

Well, it will check if True or if False each time, but only actually compute it for the first time.

Oh right, good point.

LiamGoodacre · 2016-11-28T23:58:03Z

src/Language/PureScript/TypeChecker.hs

+  -- is this argument fully determined via fundeps
+  isFunDepDetermined = (Any False, Any True) == foldMap determining (typeClassDependencies cls)
+    where determining fd = (Any (i `elem` fdDeterminers fd),
+                            Any (i `elem` fdDetermined fd))


Not sure if this is exactly what we want, but it makes more sense than what I had before.

Okay I think I understand what you were saying before, I was originally reading it differently.

Here are a few examples cases though and what I think the outcome is:

fundeps fully determined

a -> b b

a -> b, b -> a

a -> b, b -> a, c -> a a, b

a -> b, b -> c b, c

a -> b, b -> a, a -> c c

Well let's write out explicitly what we want.

We want to prevent the user from casing on types in rows (i.e. labels in rows shouldn't determine behavior).

So we can't have two different instances with different rows in some type argument and every other type argument the same.

One way to achieve that with a single functional dependency (e.g. MonadState, where m -> s) is to say that we have a functional relationship on type arguments (m determines s), so changing the result of the function forces the argument to change (if s differs, m must differ too). If the input types are the same but the outputs differ, that will lead to overlap.

In general, there must be some type argument which is forced to differ between the two instances. We can find the set of such type arguments by following functional dependencies backwards, but I think to do this properly we need a full (static) overlap check, which is why I suggest limiting things to a single functional dependency for now.

paf31 · 2016-11-29T03:29:49Z

src/Language/PureScript/TypeChecker.hs

+checkTypeClassInstance cls i = check where
+  -- is this argument fully determined via fundeps
+  isFunDepDetermined = (Any False, Any True) == foldMap determining (typeClassDependencies cls)
+    where determining fd = (Any (i `elem` fdDeterminers fd),


Is i `elem` fdDeterminers fd enough if fdDeterminers has more than one thing in it?

Actually, I'm not sure that i `elem` fdDeterminers fd is relevant at all, is it?

I would say this: i is determined by some fundep, but none of the determiners for that fundep can themselves be determined by some other fundep (so the solver is forced to case on at least one determiner).

I'm not sure that makes sense 😕, wouldn't that mean x -> y, y -> z and x -> y z are different? Using that algorithm:

Walkthrough of checking z in x -> y z

determined by: x ("determiners for that fundep") x isn't determined by anything therefore, c is determined

Walkthrough of checking z in x -> y, y -> z:

determined by: y ("determiners for that fundep", from: y -> z) y is determined by: x ("determined by some other fundep") therefore, z is not determined ???

I have come up with what I think is a correct general solution: I'll push a new commit in a minute for you to look at. It uses a graph to compute contributing dependencies between variables. We will want to move computing the determined args out of the instance check, but it's there for now whilst we discuss the algorithm.

You're right, with the approximation I wrote down, they wouldn't behave the same. In terms of a graph, I would say the correct general version is:

There is some node (let's call it an initial node, for want of a better name, but it'll be the one which the solver cases on to make its decision) which is not determined by any fundep, and a path from that node to the one we're interested in.

In the case of fundeps with multiple inputs, it's slightly trickier:

Working backwards from the target, every path ends in an initial node.

Either way, this means that every pair of instances with different types in the target node will be forced to differ in some initial node, or else will be overlapping.

LiamGoodacre · 2016-12-01T02:08:37Z

Okay I've moved where we compute the determined arguments and stored the result in TypeClassData. How's this look?

…tructor'

paf31 · 2016-12-03T19:58:44Z

@LiamGoodacre Looks great, but I'd like to go over the isFunDepDetermined a bit more to make sure it's doing the right thing. I'm still thinking in terms of the "all paths lead to a non-determined type argument" approach. Maybe we can chat about it on IRC.

LiamGoodacre · 2016-12-05T16:17:08Z

I tried to write up how I'm thinking about the algorithm in a more descriptive way. Hope this helps get my idea across :)

Cycles in a fundep constitute arguments of the same determinacy. That is, say x is determined, and there is a cycle between x and y, then y must also be determined.

From the point of view of calculating determinacy, we can consider cycles of arguments together. So consider each cyclic group as a node in a DAG. Where an edge exists between nodes A and B if an argument in A determines and argument in B. Implicitly each argument depends on itself. Therefore each argument must be in exactly one group. Then the collection of initial nodes of each disconnected path is the set of determiners of everything else. Everything else being determined.

Relating to the implementation: for an argument X, if there exists a node (in a cyclic group) that determines X, which X does not determine (isn't in the same cyclic group, or implied by the cyclic group), then X is determined. If there doesn't exist such an argument, then the cyclic group in which X resides is at the root of a path - as such it is a determiner.

paf31 · 2016-12-05T16:44:17Z

It sounds like we might be able to phrase that in terms of the strongly-connected components? But again, things are possibly complicated by edges like a b -> c with multiple types in the source, since we don't have a graph any more, but a hypergraph (I think).

Actually, now that I think about it in terms of SCC, I think your algorithm must be right after all. Could you just please add a comment explaining what we discussed?

paf31 · 2016-12-06T04:36:10Z

Thanks very much!

LiamGoodacre commented Nov 26, 2016

View reviewed changes

paf31 reviewed Nov 28, 2016

View reviewed changes

paf31 added the status: ready for review label Nov 28, 2016

LiamGoodacre commented Nov 28, 2016

View reviewed changes

paf31 reviewed Nov 29, 2016

View reviewed changes

LiamGoodacre added 3 commits December 1, 2016 02:12

Support rows in instance head under fundeps

dabd7ee

Check determined class args by calculating contributing deps

8f07799

Move determined arguments to TypeClassData and compute in 'smart cons…

a447f47

…tructor'

Update description of algorithm for computing determined type class args

115f2ba

paf31 merged commit 6954b06 into purescript:master Dec 6, 2016

LiamGoodacre deleted the feature/instance-head-rows branch December 6, 2016 08:14

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add support for rows in instance head under fundeps #2451

Add support for rows in instance head under fundeps #2451

LiamGoodacre commented Nov 26, 2016

LiamGoodacre Nov 26, 2016

paf31 Nov 28, 2016

paf31 Nov 28, 2016

paf31 Nov 28, 2016

LiamGoodacre Nov 28, 2016 •

edited

paf31 Nov 28, 2016

LiamGoodacre Nov 28, 2016 •

edited

paf31 Nov 28, 2016

LiamGoodacre Nov 28, 2016

LiamGoodacre Nov 29, 2016

paf31 Nov 29, 2016

paf31 Nov 29, 2016

paf31 Nov 29, 2016

LiamGoodacre Nov 30, 2016

paf31 Nov 30, 2016 •

edited

LiamGoodacre commented Dec 1, 2016

paf31 commented Dec 3, 2016 •

edited

LiamGoodacre commented Dec 5, 2016

paf31 commented Dec 5, 2016

paf31 commented Dec 6, 2016

fundeps	fully determined
`a -> b`	`b`
`a -> b, b -> a`
`a -> b, b -> a, c -> a`	`a, b`
`a -> b, b -> c`	`b, c`
`a -> b, b -> a, a -> c`	`c`

Add support for rows in instance head under fundeps #2451

Add support for rows in instance head under fundeps #2451

Conversation

LiamGoodacre commented Nov 26, 2016

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LiamGoodacre Nov 28, 2016 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LiamGoodacre Nov 28, 2016 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

paf31 Nov 30, 2016 • edited

Choose a reason for hiding this comment

LiamGoodacre commented Dec 1, 2016

paf31 commented Dec 3, 2016 • edited

LiamGoodacre commented Dec 5, 2016

paf31 commented Dec 5, 2016

paf31 commented Dec 6, 2016

LiamGoodacre Nov 28, 2016 •

edited

LiamGoodacre Nov 28, 2016 •

edited

paf31 Nov 30, 2016 •

edited

paf31 commented Dec 3, 2016 •

edited