the MPTC Dilemma (please solve)

[Manuel M T Chakravarty]

Ross Paterson:
> On Sun, Mar 19, 2006 at 11:25:44AM -0500, Manuel M T Chakravarty wrote:
> > My statement remains:  Why use a relational notation if you can have a
> > functional one?
> 
> I agree that functions on static data are more attractive than logic
> programming at the type level.  But with associated type synonyms,
> the type level is not a functional language but a functional-logic one.

Your are right, of course.  

<Hand-waving-alert>
        However, the evaluation model is what is known as "residuation"
        in the FL community, which is essentially functional programming
        with logic variables and lenient evaluation (a la Id).  As long
        as we only have strongly normalising functions, lenient
        evaluation and lazy evaluation coincide.  So, for Haskell
        programmers, we are on familiar ground.
</Hand-waving-alert>

Manuel