[Caml-list] a question about Ocaml semantics

[Caml-list] a question about Ocaml semantics

[Matej Kosik]

Hi,

There's an Ocaml language feature I do not understand.

E.g. in this example:

  type 'a phantom = int
  type t = { enter : 'a. 'a phantom -> int }
  let f g = g.enter 2
  let _ = f { enter = fun x -> 1 + x } (* ok *)
  let _ = f { enter = (+) 1 }          (* fails to typecheck *)

I don't get why, if we have:

  type 'a phantom = int

i.e. "'a phantom" is defined as an alias of "int",
how is it possible that the following types:

  { enter : 'a. 'a phantom -> int }

is not equal to

  { enter : 'a. int -> int }

I've tried to find a corresponding section in the Reference Manual, but I failed.
Where is this explained?

Re: [Caml-list] a question about Ocaml semantics

[Philippe Veber]

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

Hi Matej,

I'm no expert, but I'm pretty sure the problem here is related to the value
restriction [0]. If you change the last line to:

# let _ = f { enter = fun x -> (+) 1 x } ;;
- : int = 3

there is no typing error anymore. Note that with ocaml 4.04.0 and 4.04.1,
your original definition is accepted.

hope this helps,
  Philippe.

[0] https://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf



2017-05-26 10:08 GMT+02:00 Matej Kosik <
5764c029b688c1c0d24a2e97cd764f@gmail.com>:

> Hi,
>
> There's an Ocaml language feature I do not understand.
>
> E.g. in this example:
>
>   type 'a phantom = int
>   type t = { enter : 'a. 'a phantom -> int }
>   let f g = g.enter 2
>   let _ = f { enter = fun x -> 1 + x } (* ok *)
>   let _ = f { enter = (+) 1 }          (* fails to typecheck *)
>
> I don't get why, if we have:
>
>   type 'a phantom = int
>
> i.e. "'a phantom" is defined as an alias of "int",
> how is it possible that the following types:
>
>   { enter : 'a. 'a phantom -> int }
>
> is not equal to
>
>   { enter : 'a. int -> int }
>
> I've tried to find a corresponding section in the Reference Manual, but I
> failed.
> Where is this explained?
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

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

Re: [Caml-list] a question about Ocaml semantics

[Jeremy Yallop]

On 26 May 2017 at 09:08, Matej Kosik
<5764c029b688c1c0d24a2e97cd764f@gmail.com> wrote:
> There's an Ocaml language feature I do not understand.
>
> E.g. in this example:
>
>   type 'a phantom = int
>   type t = { enter : 'a. 'a phantom -> int }
>   let f g = g.enter 2
>   let _ = f { enter = fun x -> 1 + x } (* ok *)
>   let _ = f { enter = (+) 1 }          (* fails to typecheck *)
>
> I don't get why, if we have:
>
>   type 'a phantom = int
>
> i.e. "'a phantom" is defined as an alias of "int",
> how is it possible that the following types:
>
>   { enter : 'a. 'a phantom -> int }
>
> is not equal to
>
>   { enter : 'a. int -> int }
>
> I've tried to find a corresponding section in the Reference Manual, but I failed.
> Where is this explained?

I'm not sure that the interaction of features here is documented
anywhere.  But your expectations seem reasonable to me.

The good news is that the behaviour changed in OCaml 4.04.0, and your
program is now accepted.  However, it's not clear (to me) that the
interaction between generalization, phantom types and variance is
quite optimal or consistent yet.  For example, I'd expect this similar
program to be accepted

   type 'a phantom = int
   let x : type a. a phantom -> int = (+) 1

but it's rejected by OCaml 4.04.1.

Re: [Caml-list] a question about Ocaml semantics

[Jeremy Yallop]

Dear Matej,

On 26 April 2017 at 15:26, Matej Kosik
<5764c029b688c1c0d24a2e97cd764f@gmail.com> wrote:
> I am not sure I understand particular aspect of Ocaml semantics.
>
> In the context of an *.ml file, can
>
>         struct include A end
>
> be in general (i.e. unconditionally always) be rewritten to
>
>         A
>
> ?

The answer depends a bit on exactly what you consider semantics as
opposed to implementation details, but there are a few cases where the
rewriting you describe either changes the behaviour of programs or
changes whether the programs are accepted by the type checker.

Since 'struct include A end' allocates in the current implementation,
while 'A' does not allocate, any program that detects allocation
behaviour will be able to tell the difference between the two.
Physical equality (whose behaviour on package types is
implementation-dependent) is a simple example.  If you have the
following definitions

   module type T = sig val x : int end
   module M = struct let x = 0 end

then this expression evaluates to 'false':

  # (module struct include A end :T) == (module A);;
  - : bool = false

but rewriting 'struct include A end' to 'A' changes the result to 'true':

  # (module A :T) == (module A);;
  - : bool = true

There are other ways to detect allocation, but most or all of them are
similarly implementation-dependent.

There's a second difference, related to typing.  The module type
expression 'module type of A' does not add equalities to the types of
A, while 'module type of struct include A end' does include the
equalities:

  # module A = struct type t end;;
  module A : sig type t end
  # module type S = module type of A;;
  module type S = sig type t end
  # module type S = module type of struct include A end;;
  module type S = sig type t = A.t end

Since changing 'struct include A end' to 'A' removes some type
equalities, there are programs that are well-typed before the change
but ill-typed after.  For example, if you have the following
definition

  module A : sig type t val x : t end =
  struct type t = int let x = 0 end

then the following program is well-typed, because M1.t is equal to A.t

  module M1 : module type of struct include A end = A
  M1.x = A.x

but the following program is ill-typed, because M2.t is not equal to A.t

  module M2 : module type of A = A
  M2.x = A.x

With a bit more effort it's possible to come up with an example where
the program remains well-typed but the behaviour changes.  In many
cases types are just a check that a program won't go wrong, and
type-checking doesn't change the behaviour of a program.  But in a few
cases the OCaml implementation uses type information to decide how to
compile and execute a program.  For example, if the OCaml compiler can
tell that all the fields in a record type are floats then the record
will be given an unboxed layout.  The following example shows how the
layout of records can change according to whether 'struct include A
end' or 'A' is used in a particular location.

Suppose you have a GADT that tells you whether a type is equal to float:

   type _ is_float = Is_float : float is_float

and an existential type that can hold any value:

   type box = Box : _ -> box

and a module with an abstract type 't' together with a value of type
't' and a proof that 't' is equal to float:

  module A : sig type t val x : t val is_float : t is_float end =
  struct type t = float let x : t = 0.0 let is_float = Is_float end

Then the behaviour of the following program changes if you replace
'struct include A end' with 'A':

  match A.is_float with Is_float ->
    let module X = struct
      module N : module type of struct include A end = A
      type t1 = {x:float} and t2 = {y:N.t}
    end in
  assert (X.(Box {x=0.0} = Box {y=N.x}))

When the program above is compiled N.t is known to be equal to A.t and
A.t is known to be equal to float under the match, so both the 't1'
and 't2' records are given identical unboxed layouts and the assertion
succeeds.

However, if you change 'struct include A end' to 'A' then N.t is no
longer equal to A.t, and so 't2' does not have an unboxed layout.
Since the polymorphic equality function '=' compares values by their
layout, the difference between 't1' and 't2' is observable.

Kind regards,

Jeremy.

[Caml-list] a question about Ocaml semantics

[Matej Kosik]

Dear all,

I am not sure I understand particular aspect of Ocaml semantics.

In the context of an *.ml file, can

	struct include A end

be in general (i.e. unconditionally always) be rewritten to

	A

?