On Thu, Jul 1, 2010 at 7:54 PM, Simon Peyton-Jones
| Also, what is the difference between fundeps and type families | wrt local type constraints? I had always assumed them to be | equivalent, if fully implemented. Similar to logic vs functional | programming, where Haskellers tend to find the latter more | convenient. Functional logic programming shows that there | are some tricks missing if one just drops the logic part.
Until now, no one has know how to combine fundeps and local constraints. For example
class C a b | a->b where op :: a -> b
instance C Int Bool where op n = n>0
data T a where T1 :: T a T2 :: T Int
-- Does this typecheck? f :: C a b => T a -> Bool f T1 = True f T2 = op 3
The function f "should" typecheck because inside the T2 branch we know that (a~Int), and hence by the fundep (b~Bool). But we have no formal type system for fundeps that describes this, and GHC's implementation certainly rejects it.
Martin Sulzmann, Jeremy Waznyhttp://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wazny:Jeremy.h..., Peter J. Stuckeyhttp://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/s/Stuckey:Peter_...: A Framework for Extended Algebraic Data Types. FLOPS 2006http://www.informatik.uni-trier.de/%7Eley/db/conf/flops/flops2006.html#Sulzm...: 47-64 describes such a system, fully implemented in Chameleon, but this system is no longer maintained. Type families and Fundeps are equivalent in expressive power and it's not too hard to show how to encode one in terms of the other. Local constraints are an orthogonal extension. In terms of type inference, type families + local constraints and fundeps + local constraints pose the same challenges. Probably, Simon is refrerring to the 'unresolved' issue of providing a System F style translation for fundeps + local constraints. Well, the point is that System FC is geared toward type families. The two possible solutions are (a) either consider fundeps as syntactic sugar for type families (doesn't quite work once you throw in overlapping instances), (b) design a variant System FC_fundep which has built-in support for fundeps. -Martin