
Hi, On Mon, Jan 09 2012 at 10:37 +0100, Steve Horne wrote:
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)].
Isn't Haskell doing some prolog-ish things anyway?
I thought the compiler must be doing unification to resolve type inference within expressions.
Even quite basic type reconstruction (e.g. for ML) needs unification, see e.g. Pierce TaPL chapter 22. The algorithm is rather easy to understand and implement. Based on that, I wouldn't think using /some kind of unification/ in the compilation process qualifies as being particularly prolog-ish. I suppose ``...importing a Prolog-style logic language...'' would mean to allow a significantly more powerful (and explicit) way of expressing constraints in the type system than before. I believe Brandon Allbery, when he says that this is difficult. Best regards Lu