[prev in list] [next in list] [prev in thread] [next in thread] 

List:       haskell-prime
Subject:    Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
From:       Alexey Khudyakov <alexey.skladnoy () gmail ! com>
Date:       2011-05-29 21:29:53
Message-ID: 4DE2BAD1.6080202 () gmail ! com
[Download RAW message or body]

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.

_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
[prev in list] [next in list] [prev in thread] [next in thread]