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

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

[Bob Zhang]

Hi all,
    Record disambiguation is a practical feature, it helps a lot in
writing open-free code.
    In practice, I found it is a bit limited, below is two scenarios
that the compiler can not infer in a correct way, will this be
improved in the future by any chance?
     From the user's point of view, annotating the toplevel is quite
acceptable, maybe the typechecker could take the type-annotation as a
higher priority.
    ---
    1.
         let f (ls:t) =
            ls |> List.map (fun x -> x.loc) (* cannot inferred x.loc*)
   2.
        type t = {loc:string}
        type v = {loc:string; x:int}
        type u = [`Key of t]
        let f (u:t) =
          match u with
          | `Key {loc} -> loc (* does not compile *)

-- 
Regards
-- Bob

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

[Jacques Garrigue]

On 2013/10/24, at 5:52, Bob Zhang <bobzhang1988@gmail.com> wrote:

>    Record disambiguation is a practical feature, it helps a lot in
> writing open-free code.
>    In practice, I found it is a bit limited, below is two scenarios
> that the compiler can not infer in a correct way, will this be
> improved in the future by any chance?
>     From the user's point of view, annotating the toplevel is quite
> acceptable, maybe the typechecker could take the type-annotation as a
> higher priority.
>    ---
>    1.
>         let f (ls:t) =
>            ls |> List.map (fun x -> x.loc) (* cannot inferred x.loc*)
>   2.
>        type t = {loc:string}
>        type v = {loc:string; x:int}
>        type u = [`Key of t]
>        let f (u:t) =
>          match u with
>          | `Key {loc} -> loc (* does not compile *)

Case 1 would require a new specification of how type propagation works.
In particular, propagating from an argument to another argument.
For this reason, the probability that it gets done is low.
(I know that F# handles this case in a special way, but do we want to introduce
a special case just for |> ?)

Case 2 seems more reasonable (after replacing (u:t) by (u:u)).
In particular,
   let f (u:u) =
        match u with `Key loc -> loc.loc
already works, so it seems strange that the pattern-matching version doesn't.

	Jacques

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

[Bob Zhang]

Hi Jacques,
> Case 2 seems more reasonable (after replacing (u:t) by (u:u)).
> In particular,
>    let f (u:u) =
>         match u with `Key loc -> loc.loc
> already works, so it seems strange that the pattern-matching version doesn't.
Sorry for the typo
I expected
   let f (u:u) =   match u with `Key {loc} -> loc
to work, it does not  yet (against 4.01.0)
>
>         Jacques



-- 
Regards
-- Bob

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

[Alain Frisch]

On 10/24/2013 03:40 AM, Jacques Garrigue wrote:
>>     1.
>>          let f (ls:t) =
>>             ls |> List.map (fun x -> x.loc) (* cannot inferred x.loc*)
>
> Case 1 would require a new specification of how type propagation works.
> In particular, propagating from an argument to another argument.
> For this reason, the probability that it gets done is low.
> (I know that F# handles this case in a special way, but do we want to introduce
> a special case just for |> ?)

The situation with List.map (or similar iterators) is quite common, and 
remains one of the only cases where local annotations are often required.

There is already a left-to-right propagation between arguments:

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


With -principal, the first case is reported as non principal (warning 18).

Is there any practical or theoretical problem with specifying the 
information flow in order to make it principal?



For List.map and similar cases, one often prefers the type information 
to flow from the data stucture to the local abstraction.  One can define:

  let map l f = List.map f l

so that:

  map [{a=2}] (fun ({a} : t) -> a + 1);;   (* rejected *)
  map [({a=2} : t)] (fun {a} -> a + 1);;   (* accepted *)


One could imagine heuristics (based either on the function type, or on 
the argument shape) to pick a different ordering, but it seems much 
better to have a simple and predictable flow, and the left-to-right 
seems the most natural one between function arguments.  If we specify 
such information flow, it is then the responsibility of the library 
author to choose a "good" ordering.  I hoped that labeled arguments 
could let the client code choose a different one, but this doesn't work:

  let map ~f l = List.map f l

  map [{a=2}] ~f:(fun ({a} : t) -> a + 1);;   (* accepted *)
  map ~f:(fun ({a} : t) -> a + 1) [{a=2}];;   (* accepted *)

  map [({a=2} : t)] ~f:(fun {a} -> a + 1);;   (* rejected *)
  map ~f:(fun {a} -> a + 1) [({a=2} : t)];;   (* rejected *)


Does it seem reasonable to use the actual ordering between arguments on 
the call site rather than the one defined by the function type?


Alain

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

[Didier Remy]

> There is already a left-to-right propagation between arguments:
>
>   type t = {a: int};;
>   type s = {a: string};;
>   List.map (fun ({a} : t) -> a + 1) [{a=2}];;   (* accepted *)
>   List.map (fun {a} -> a + 1) [({a=2} : t)];;   (* rejected *)

Yes, but as you notice this is not principal.

> With -principal, the first case is reported as non principal (warning 18).
>
> Is there any practical or theoretical problem with specifying the information
> flow in order to make it principal?

I don't think specifying the information flow between left and right
(always-left-to-right, always-right-to-left, or depending-on-examples) is a
good design. This leads to non predictable type inference and less robust
programs: refactoring a function by just changing the order of parameters
(and consistently changing the order of arguments in all uses of the
function) may break existing programs and also require new annotations.

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.

         Didier

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

[Alain Frisch]

On 10/25/2013 01:27 PM, Didier Remy wrote:
> I don't think specifying the information flow between left and right
> (always-left-to-right, always-right-to-left, or depending-on-examples) is a
> good design. This leads to non predictable type inference and less robust
> programs  : refactoring a function by just changing the order of parameters
> (and consistently changing the order of arguments in all uses of the
> function) may break existing programs and also require new annotations.

This is already the case, except for people using -principal.  I know it 
is recommended to use this option (at least once in a while), but I 
doubt many users actually do it.  (And FWIW, -principal is so slow on 
our code base that we cannot actually use it in practice -- this is 
probably related to the way we use object types.)

As a user, I think I'm willing to pay the price of risking having to add 
a few annotations on the next refactoring if this makes a very common 
idiom more practical.


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

If the ordering used for the (specified) information flow were drawn 
from the actual call site, labeled arguments would be a good solution.


Alain

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

[Wojciech Meyer]

[-- Attachment #1: Type: text/plain, Size: 2370 bytes --]

Not being here a type system's expert so excuse if I did a serious mistake
or I said something trivial.

Wouldn't make sense to perform the unification of the arguments (GADT
constructors and function arguments), in both ways? First propagate the
type information left right and then right left, and then finally unify the
results? Alternatively, we could also add check such that if the left right
type checking fails (being not principal), then we try also right to left.



On Fri, Oct 25, 2013 at 1:39 PM, Alain Frisch <alain@frisch.fr> wrote:

> On 10/25/2013 01:27 PM, Didier Remy wrote:
>
>> I don't think specifying the information flow between left and right
>> (always-left-to-right, always-right-to-left, or depending-on-examples) is
>> a
>> good design. This leads to non predictable type inference and less robust
>> programs  : refactoring a function by just changing the order of
>> parameters
>> (and consistently changing the order of arguments in all uses of the
>> function) may break existing programs and also require new annotations.
>>
>
> This is already the case, except for people using -principal.  I know it
> is recommended to use this option (at least once in a while), but I doubt
> many users actually do it.  (And FWIW, -principal is so slow on our code
> base that we cannot actually use it in practice -- this is probably related
> to the way we use object types.)
>
> As a user, I think I'm willing to pay the price of risking having to add a
> few annotations on the next refactoring if this makes a very common idiom
> more practical.
>
>
>
>  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.
>>
>
> If the ordering used for the (specified) information flow were drawn from
> the actual call site, labeled arguments would be a good solution.
>
>
> Alain
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/**arc/caml-list<https://sympa.inria.fr/sympa/arc/caml-list>
> Beginner's list: http://groups.yahoo.com/group/**ocaml_beginners<http://groups.yahoo.com/group/ocaml_beginners>
> Bug reports: http://caml.inria.fr/bin/caml-**bugs<http://caml.inria.fr/bin/caml-bugs>
>

[-- Attachment #2: Type: text/html, Size: 3286 bytes --]

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

[oleg]

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