Here are two more legal problems, ie problems concerning (broken) laws. The first is a problem with lifted functions spaces (even though I voted for them before), similar to Simon's recent "Effect 1". Consider: f [] = \y -> e1 g [] y = e1 f (x:xs) = \y -> e2 g (x:xs) y = e2 Is f _|_ = _|_ ? I guess so (the functions on the right needn't be so blatant) Is g _|_ = _|_ ? I guess so, because g = f Is seq (g _|_) 42 = _|_ ? It has to be, but this suggests that when a partial application is evaluated, other than because it is being applied to something, the `relevant amount' of pattern matching needs to be done to determine termination. This would be difficult to generalise, given current pattern matching practice. I think what's wrong here is the statement g = f, which relies on a relative of the eta rule, namely extensionality: "if for all x: g x = f x then g = f" which is only true for non-_|_ functions. Thus g /= f, g _|_ = \y -> g _|_ y and functions generally have have a `detectable' natural arity. (I have personally never liked partial application; it can lead to very bad error reporting for beginners for one thing. I still like higher order functions, of course.) The second problem concerns a law which I would like to see enforced: symmetry of arguments. That is, if I swap the arguments of a function (f x y goes to f y x) in its definition and in every call, there should be no overall effect on the program. I believe this is compatible with partial application if you are careful (although partial application does tend to promote asymmetrical thinking; another reason why I don't like it). However, is this compatible with current pattern matching practice? I am not sure (certainly with uniform patterns there are definitions which are not uniform when you exchange arguments, as Simon points out in his 1987 implementation book). Incidentally, we are experimenting with a compilation method which eliminates partial applications early on (and otherwise follows the STG route). It is easy to explain and implement, it supports a lifted function space, and it allows the standard C calling conventions to be used. At first sight, it appears costly; a call-and-return to evaluate every (dynamic) function value before appying it, but then you don't have to do a check for the right number of arguments on entry to every function. Ian [EMAIL PROTECTED], Tel: 0272 303334
