Why does the order of operands affect scope?

user_1477667 0
Viewed 79

I'm trying to understand why a certain constructor is accepted in one expression but not another. I would have expected it to be out of scope in both. I'm a rank beginner to OCaml (I mostly use Haskell), so I could be missing something totally obvious to someone experienced.

type zero = Zero
type 'n succ = Succ
type 'n snat =
  | SZero : zero snat
  | SSucc : 'm snat -> 'm succ snat

module SimpleInduction (Pred : sig type 'n pred end) = struct
  open Pred
  type hyps =
    { base : zero pred
    ; step : 'm. 'm pred -> 'm succ pred}

  let rec induct : type n. hyps -> n snat -> n pred =
          fun h sn -> match sn with
          | SZero -> h.base
          | SSucc p -> h.step (induct h p)
end;;

let module Snot = struct type 'n pred = Top end in
  let module Goop = SimpleInduction(Snot) in
    Goop.induct {base = Top; step = fun _ -> Top} SZero = Top;;
(*
let module Snot = struct type 'n pred = Top end in
  let module Goop = SimpleInduction(Snot) in
    Top = Goop.induct {base = Top; step = fun _ -> Top} SZero;;
*)

This compiles just fine, for some reason. With the second definition of Snot uncommented, I get an error:

19 |     Top = Goop.induct {base = Top; step = fun _ -> Top} SZero;;
         ^^^
Error: Unbound constructor Top

What brings Top into scope in the first definition of Snot? Using regular modules rather than first-classlocal ones makes no difference.

If I use Snot.Top on the left-hand side, I get no complaints on the right-hand side. Why is that?

ocaml module
1 Answers

In short, type-directed disambiguation is indeed not restricted to scope.

With an explicit type annotation, the type checker can select the constructor from the type without bringing the constructor in scope.

For instance,

module M = struct type 'a t = A of 'a end
let ok: _ M.t = A ()
let wrong: _ M.t = A (A ())

the first example is valid because the type annotation is enough to know that the A in A () is an _ A.t. However, the second example does not work because the constructor has not been brought into the scope.

Moreover, type-directed disambiguation only requires the expected type of the constructor or record to be known. Typically, in this example

let expected =
  let f (M.A x) = x in
  f (A ())

we know that the type of the argument of f is an _ M.t, thus we know that the A in f (A ()) come from _ M.t and we can use type-directed disambiguation like in the case with the explicit annotation.

If you find this behavior exotic, the warning 42 [name-out-of-scope] can be used to warn in such situation. Compiling your example with this warning yields (among many other instances of this warning)

23 |     Goop.induct {base = Top; step = fun _ -> Top} SZero = Top
                                                               ^^^
Warning 40 [name-out-of-scope]: Top was selected from type Snot.pred.
It is not visible in the current scope, and will not 
be selected if the type becomes unknown.

(the warning names are new in 4.12)

Concerning your second point, the order of expression may matter in the absence of explicit annotations. Indeed, without explicit annotation, type-directed disambiguation will be only be able to select the right constructor when the expected type is already known. And type checking goes from left to right in OCaml. Thus in

... = Top

the type of the left-hand side has already been inferred and thus the expected type of Top is _ Snot.pred. When the order is reversed

Top = ...

the typechecker is trying to find a constructor Top without any type information and there are no constructor Top in scope. Thus it fails with an Unbound constructor error. If you want to avoid depending on the order, you can either

  • write the full name of the constructor:
  Snot.Top = ...
  • use an explicit type annotation
(Top: _ Snot.pred) = ...
  • open the Snot module.
  Snot.( Top ) = ...
  (* or *)
  let open Snot in Top = ...

I would advise to use one of those solutions since there are more robust.

After all, relying on the specific implementation of the type checking is brittle. In fact, there is a compiler flag -principal and a warning (18) [not-principal] that takes care to emit a warning in presence of such potentially brittle inference:

23 |     Goop.induct {base = Top; step = fun _ -> Top} SZero = Top
                                                               ^^^
Warning 18 [not-principal]: this type-based constructor disambiguation is not principal.

Here "not principal" means that the result of the type-based disambiguation depended on the order of the type-checking.

user_73693660
Related