TypeFamilies vs. FunctionalDependencies & type-level recursion

Alexey Khudyakov alexey.skladnoy at gmail.com
Sun May 29 23:29:53 CEST 2011

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

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 

 > 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 
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.

More information about the Haskell-prime mailing list