MPTCs and functional dependencies

[Martin Sulzmann]

Manuel M T Chakravarty writes:
 > Simon Peyton-Jones: 
 > > My current take, FWIW.
 > > 
 > > [...]
 > > Tentative conclusion: H' should have MPTC + FDs, but not ATs.
 > 
 > My conclusion is that we should not include FDs or ATs into the standard
 > at the moment.  Standardising FDs as a stopgap measure may easily put us
 > into the same situation that we are having with records at the moment.
 > Nobody is really happy with it, but we don't dare to change it either.
 > 
 > Manuel

The situation here is clearly different. Whatever comes next
(after FDs) will be a conservative extension. So, standardising
FDs is a good thing because they have proven to be a useful (somewhat
essential for MPTCs) feature. Hence, I will go with Simon:
H' should have MPTC + FDs, but not ATs.

You mention that nobody is really happy with FDs at the moment,
but you don't provide concrete arguments why. I assume you
refer to the following two issues:

1) FDs may threaten complete and decidable type inference
2) FDs are more verbose than say ATs

Issue 1) is not limited to FDs. ATs share the same problem.
I'll spare the details.

Issue 2) may be a matter of taste. 
In fact, sometimes it's easier to write "decidable" (but
more verbose) FDs than writing an "equivalent" *and* "decidable" AT
program.

Recall the following discussion.
Somebody asked how to write the MonadReader class with ATs:
http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html

This requires an AT extension which may lead to undecidable type
inference:
http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html
It is possible to recover decidable AT inference (I hinted how, see
the above email thread), but the sufficient conditions get more and
more complex.


 > > * MPTCs are very useful.  They came along very rapidly (well before
 > > H98).  I think we must put them in H'
 > > 
 > > * But MPTCs are hamstrung without FDs or ATs
 > > 
 > > * FDs and ATs are of the same order of technical difficulty, as Martin
 > > says
 > 
 > Both FDs and ATs come in various versions of different levels of
 > expressiveness.  They may be of the same level of difficulty with all
 > bells and whistles, but that's a bit of a red herring.  The real
 > question is how do the levels of difficulty compare at the level of
 > expressiveness that we want.  Or phrased differently, for a version that
 > is not too difficult, how does the expressiveness compare.
 > 

See the MonadReader example above!

 > > * ATs are (I believe) a bit weaker from the expressiveness point of view
 > > (zip example), but are (I believe) nicer to program with.  
 > 
 > The zip example can be done with ATs - it's actually in one of Martin's
 > papers.  I currently don't know of any FD example that you can't do with
 > ATs.  It's a matter of what forms of AT definitions you want to allow.
 > 

The zip example canNOT be expressed with ATs as described in the
ICFP'05 paper!

The point here is really that it's fairly easy to write down the zip
instances and let FDs automatically derive the necessary improvement
rules. In case of ATs (using an extension which has been sketched
in the "Associated FD" paper), the programmer has to write down 
all improvement rules (as type functions) herself. This can be a
non-trivial task!

 > > 
 > > * Medium term, I think ATs may *at the programming-language level*
 > > displace FDs, because they are nicer to program with.  But that's just
 > > my opinion, and we don't have enough experience to know one way or the
 > > other.
 > 
 > Maybe not only at the programming-language level.  Given our latest paper,
 > 
 >   http://www.cse.unsw.edu.au/~chak/papers/SCP06.html
 > 
 > for example, the translation of ATs is simpler than FDs if we also have
 > existential types (but admittedly that became clear to us only after
 > your email message).
 > 

Be careful, somebody could argue the opposite.
ATs are now redundant because all FD programs can now be translated.
Hence, the AT via FD encoding scheme which I once sketched is now type
preserving.
The fact that the FD translation is more "complex" is not a serious
issue. After all, there's an automatic translation scheme.

Martin