On 08/01/2012 21:13, Brandon Allbery wrote:
(Also, de facto I think it's already more or less been decided in favor of type families, just because functional dependencies are (a) a bit alien [being a glob of Prolog-style logic language imported into the middle of System Fc] and (b) [as I understand it] difficult to verify that the code in the compiler is handling all the potential corner cases right [mainly because of (a)].
Without meaning to express an opinion either way about an issue I don't understand... Isn't Haskell doing some prolog-ish things anyway? I thought the compiler must be doing unification to resolve type inference within expressions. It's not a simple expression evaluation problem (just evaluate the type rather than the value) because sometimes you know the return type but not (yet) the argument types - type information flows bottom-up and top-down through the same expression tree. I could easily be mistaken, though. Looking at the similar overload-resolution problem, Ada can resolve based on return types but C++ cannot. Ada needs unification or something similar to resolve overloading, whereas C++ just evaluates expressions for type instead of value. I can't now say for sure where I picked up the idea that Haskell needs unification to resolve type inference, but I've had some odd error messages which seem to confirm that belief - I assume because the mistake doesn't cause an immediate conflict, instead causing an indirect conflict somewhere else in the larger expression.