[Haskell-cafe] checking types with type families

[Simon Peyton-Jones]

Claus

|  > I'm interested in situations where you think fundeps work
|  > and type families don't.  Reason: no one knows how to make
|  > fundeps work cleanly with local type constraints (such as GADTs).
|  >
|  > If you think you have such as case, do send me a test case.
|  
|  Do you have a wiki page somewhere collecting these examples?

I don't think so.  Would you feel like starting one?

I do try to turn every tricky example into a case in the testsuite though.  

|  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.  In GHC, as in Mark Jones's original descrption, fundeps just give rise to some extra unifications of otherwise under-constrained type variables.

Now, Dimitrios and I have recently found that our OutsideIn type system and inference algorithm (described in the Epic Paper on my home page) can easily handle functional dependencies too, by adding a couple of extra rules.  That's good news both because it improves our understanding (well, mine anyway); and because it will give GHC a solid implementation, and one that will make the above program typecheck.  We are deep in the midst of implementing OutsideIn right now.  

That said, I'd much prefer to express the program like this:

class D a where
  type B a 
  dop :: a -> B a

instance D Int where
  type B Int = Bool
  dop n = n>0

g :: D a => T a -> Bool
g T1 = True
g T2 = dop 3

More perspicuous types, simpler reasoning.  


Bottom line: I now have a clear idea of how to formalise and implement fundeps; but I am dubious about the long-term software engineering merits of supporting both fundeps and type families.  They cover the same territory.  Copying Oleg in case he has other counter-examples.
 
Simon