Re: [Caml-list] Robust left to right flow for record disambiguation

[oleg@okmij.org]

First, I'd like to state the agreement with:
> Also, such a biased will encourage people to write parameters of functions
> in an order that works well for the uses they have in mind.  I think it odd
> that type inference would have such an influence in choosing the order of
> function parameters.

It seems the declarative model of type inference -- type checker
non-deterministically choosing type parameters -- is best to program
against. This model also gives the implementor enough freedom. If we
need explicit propagation, we should use bi-directional type-checking,
which was designed for such a case.

My main point is that record-type disambiguation is the golden
opportunity for tool writers, making the great case that programming
must be interactive, in interaction between a programmer and a
compiler. For example, when the following snippet is submitted

>   type t = {a: int};;
>   type s = {a: string};;
>   List.map (fun {a} -> a + 1) [({a=2} : t)];; 

the compiler (or a smart editor, acting on compiler's behalf) may tell
the programmer that the type of {a} in fun {a} is ambiguous, and the
possible candidates are the record types 't' and 's'. Which one the
programmer has in mind? The user will choose, and the editor will
remember user's preference by inserting the type annotation on {a} in
the source code.


Interactive programming has becoming a norm in Agda (I think Epigram
was one of the first successful experiments). When the type system is
expressive enough, interactivity seems to be the only way forward.
The alternative, a sufficiently smart compiler, has not worked out
every time it was tried. One of the main reasons the classical Partial
Evaluation (PE) is not used nowadays, despite great promises, is that
it proved hard to program against the very smart, and capricious PE.
A programmer never knows what the PE may think or do. Smart programmers
eventually figured out how to write code tailored to a particular PE,
and have become disappointed in the process [private communication
from a person who wrote a book on PE].