On 29.05.2011 22:59, David Mazieres wrote:
But now you have overlapping type synonyms, which pose a safety threat where the more-specific instance is not in scope. Therefore, Haskell likely cannot be extended to accept code such as the above.
No it could. Inconsistency arise from fact that it's not guaranted that all instances are known. Such guaranties are possible with closed type families. In such families instances could be added only in the same module with family declaration. Here is simplistic example:
data HTrue data HFalse
closed type family Equal a b :: * closed type instance a a = HTrue closed type instance a b = HFalse
No more instances could be added. So type could be determined unambigously. In type level programming type families often meant to be closed but there is no explicit way to say that and it limit their expressiveness. Also closed type families could help with lack of injectivity. It could be untracktable though.
One possible extension that *would* enable type-level recursive programming is the ability to constrain by inequality of types. I noticed GHC is on its way to accepting "a ~ b" as a constraint that types a and b are equal. If there were a corresponding "a /~ b", then one might be able to say something like:
instance HLookup k (HCons (k, v) l) where ... instance (h /~ (k, v), HLookup k l) => HLookup k (HCons h l) where ...
I can't see how it change things. AFAIR instances selected only by their heads, contexts are not taken into account. Besides type inequality could be easily implemented with closed type families. See code above. Here is contrived example of usage:
instance (Equal Thing Int ~ HFalse) => Whatever Thing
P.S. Also I have suspicion that version with fundeps will behave badly if more instances are added in another module.