MPTCs and functional dependencies

[Manuel M T Chakravarty]

Simon Peyton-Jones: 
> My current take, FWIW.
> 
> * 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.

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

> * BUT we have way more experience with actually programming with FDs.
> ATs fail the "well-established" test by a mile.

Indeed!

> * Largely due to Martin's work, we now have a much better handle on just
> what restrictions on FDs make type inference tractable.  So I believe
> there is a solid MPTC+FD story that we could embody in H'.
> 
> * 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).

> 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