Mantis Bug Tracker

View Revisions: Issue #7816 All Revisions ] Back to Issue ]
Summary 0007816: About the order in which record fields are typed
Revision 2018-07-02 16:30 by trefis
Description Original starting point of the discussion: https://github.com/ocaml/ocaml/pull/1675 [^]

N.B. I will not discuss principality concerns here, they remain the same regardless of which order is actually chosen.

# Current state of things (up-to OCaml 4.07)

For patterns:
- when typing a record pattern, fields are typed in the order following that of the record declaration
- parmatch currently relies on this sorting having been done, cf. https://github.com/ocaml/ocaml/blob/41a432ff50fdd0f3559d0f8936d17dfa5bf73232/typing/parmatch.ml#L261 [^]
- matching doesn't appear to rely on this having been done, but does use that same (declaration) order, cf.
  + https://github.com/ocaml/ocaml/blob/41a432ff50fdd0f3559d0f8936d17dfa5bf73232/bytecomp/matching.ml#L556 [^]
  + https://github.com/ocaml/ocaml/blob/41a432ff50fdd0f3559d0f8936d17dfa5bf73232/bytecomp/matching.ml#L64 [^]

For expressions fields are typed in the order following that of the record declaration
Alain pointed out this is coherent with the way labeled arguments are typechecked.

# Suggested change: follow the source order instead

If I'm not mistaken, the proposition has been made by both Gabriel and Leo.

I'm not sure whether they propose this change to be limited to patterns or to apply to expression as well.
Although it seems like if we change the order in patterns we should change the order in expressions as well.

## Potential issues

If we change the order in which typing is done, then we also need to update the evaluation order (to match the new typing order).

As Jeremy said:
> The equation propagation behaviour is closely connected with
> evaluation order, too. In a match like this:
>
> match e with
> | {x = lazy A, y = lazy B}
>
> equality information needs to flow in the direction first-evaluated
> to last-evaluated because the equalities are only available when
> pattern matching succeeds.
>
> So changing the direction in which equalities flow (which will cause
> a noisy type-checking failure in some currently-valid programs) also
> involves changing the order in which patterns are evaluated (which
> will cause a silent evaluation-order change in some currently-valid
> programs).

Although I'm not sure lazyness really matters here?

Following that, Gabriel added:
> I thought that the evaluation-order change would be simple, but we
> have a problem if a matched column contains two record patterns with
> different field orders.

To give a concrete example of a problematic pattern:


    type _ t = Pair : ('a * 'b) t | Unit : unit t
    type 'a r = { x : 'a t * 'a; y : 'a t * 'a; }
    let foo (type a) (r : a r) =
      match r with
      | { x = (Pair, _); y = (_, (a, b)) } -> ignore (a, b)
      | { y = (Pair, _); x = (_, (c, d)) } -> ignore (c, d)
      | _ -> ()
Revision 2018-07-02 16:21 by trefis
Description Original starting point of the discussion: https://github.com/ocaml/ocaml/pull/1675 [^]

N.B. I will not discuss principality concerns here, they remain the same regardless of which order is actually chosen.

# Current state of things (up-to OCaml 4.07)

For patterns:
- when typing a record pattern, fields are typed in the order following that of the record declaration
- parmatch currently relies on this sorting having been done, cf. https://github.com/ocaml/ocaml/blob/41a432ff50fdd0f3559d0f8936d17dfa5bf73232/typing/parmatch.ml#L261 [^]
- matching doesn't appear to rely on this having been done, but does use that same (declaration) order, cf.
  + https://github.com/ocaml/ocaml/blob/41a432ff50fdd0f3559d0f8936d17dfa5bf73232/bytecomp/matching.ml#L556 [^]
  + https://github.com/ocaml/ocaml/blob/41a432ff50fdd0f3559d0f8936d17dfa5bf73232/bytecomp/matching.ml#L64 [^]

For expressions fields are typed in the order following that of the record declaration
Alain pointed out this is coherent with the way labeled arguments are typechecked.

# Suggested change: follow the source order instead

If I'm not mistaken, the proposition has been made by both Gabriel and Leo.

I'm not sure whether they propose this change to be limited to patterns or to apply to expression as well.
Although it seems like if we change the order in patterns we should change the order in expressions as well.

## Potential issues

If we change the order in which typing is done, then we also need to update the evaluation order (to match the new typing order).

As Jeremy said:
> The equation propagation behaviour is closely connected with
> evaluation order, too. In a match like this:
>
> match e with
> | {x = lazy A, y = lazy B}
>
> equality information needs to flow in the direction first-evaluated
> to last-evaluated because the equalities are only available when
> pattern matching succeeds.
>
> So changing the direction in which equalities flow (which will cause
> a noisy type-checking failure in some currently-valid programs) also
> involves changing the order in which patterns are evaluated (which
> will cause a silent evaluation-order change in some currently-valid
> programs).

Although I'm not sure lazyness really matters here?

Following that, Gabriel added:
> I thought that the evaluation-order change would be simple, but we
> have a problem if a matched column contains two record patterns with
> different field orders.

To give a concrete example of a problematic pattern:

    # type _ t = Pair : 'a * 'b t | Unit : unit t;;
    Error: Syntax error
    # type _ t = Pair : ('a * 'b) t | Unit : unit t;;
    type _ t = Pair : ('a * 'b) t | Unit : unit t
    # type 'a r = { x : 'a t * 'a; y : 'a t * 'a };;
    type 'a r = { x : 'a t * 'a; y : 'a t * 'a; }
    # let foo (type a) (r : a r) =
        match r with
        | { x = (Pair, _); y = (_, (a, b)) } -> ignore (a, b)
        | { y = (Pair, _); x = (_, (c, d)) } -> ignore (c, d)
        | _ -> ()
      ;;


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker