User loginNavigation 
Overlapping Instances + Functional Dependencies Unsound?In the course of a BitC discussion today, somebody pointed me at this recent note by Simon PeytonJones. In it, Simon cites Oleg and Martin as pointing out that (1) type families do not play nicely with overlapping instances, (2) functional dependencies appear to, but (3) the two are equivalent, so something smells wrong. Simon gives two illustrating examples, both of which are constructed by exploiting lexical hiding across modules. I found this quite disturbing, since we rely on functional dependencies in BitC and we've been struggling with the instance resolution question. But looking at Simon's examples, it seems to me that both of them result from obvious type checking failures in the assumed implementation. I would greatly appreciate a sanity check on this. A functional dependency constitutes a statement by the programmer that a deterministic function exists between the type parameters of the type function and its type result. We are told that such a function exists, but not how it is defined. That is: the functional dependency is an assertion that such a deterministic function exists, and we should interpret it as meaning that the typing of the program is sound provided the assertion is true. The assertion itself remains to be checked. Both of Simon's examples construct circumstances in which two modules construct conflicting instantiations of a functional dependency by exploiting the limitations of scope visibility. Both break a type class: class C a b  a > b The first does so directly by introducing instances In both cases, it seems to me that we have a global determinism requirement on the type function that isn't being checked correctly, and that this is the root of the problem. In the first case, the overlap is direct. In the second case, it is sufficient to note that the two instances are not unifiable. The root problem appears to be that a global assertion is not being globally checked. That such a failure to check would lead to unsoundness does not seem either complex or surprising to me. Indeed, I would be surprised by any other outcome! So here is my question: assuming we do check that the functional dependency requirements are not violated, does an unsoundness problem remain? It's not too late to drop fundeps from BitC v1 if we need to be conservative about this. By shap at 20100731 06:50  LtU Forum  previous forum topic  next forum topic  other blogs  5718 reads

Browse archivesActive forum topics 
Recent comments
31 min 22 sec ago
3 hours 19 min ago
4 hours 23 min ago
6 hours 43 min ago
12 hours 15 min ago
13 hours 28 min ago
13 hours 59 min ago
15 hours 52 min ago
19 hours 58 min ago
20 hours 57 min ago