[Caml-list] Question on "more general"

[Caml-list] Question on "more general"

[Kenichi Asai]

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

Dear OCaml type inference experts,

If I infer the type (using Typemod.type_structure) of:

let a = 1 in fun x -> 1

and see if the type of x is more general (using Ctype.moregeneral)
than the type of a type variable (Btype.newgenvar ()), I obtain yes
(since the type of x is 'a which is more general (or equal) than a
newly created type variable, I guess).  If I do the same for:

let a = assert false in fun x -> 1

I obtain no, although it still seems that the type of x is the same
'a.  (See attached file for the concrete program I executed.  I used
OCaml 4.04.0.)  Why?

Thank you in advance!

-- 
Kenichi Asai

[-- Attachment #2: main.ml --]
[-- Type: text/plain, Size: 1764 bytes --]

open Asttypes
open Ast_helper
open Types
open Typedtree
open Parsetree

(* some helper functions *)

(* extract_typ : Typedtree.structure -> type_expr *)
let extract_typ str = match str.str_items with
    [{str_desc = Tstr_eval ({ exp_type = typ }, _)}] -> typ
  | _ -> failwith "cannot happen"

(* split_arrow : type_expr -> type_expr * type_expr *)
let rec split_arrow typ = match typ.desc with
    Tarrow (_, t1, t2, _) -> (t1, t2)
  | Tlink (typ') -> split_arrow typ'
  | _ -> failwith "cannot happen"

(* various expressions *)

(* 1 *)
let one : expression = Exp.constant (Const.integer "1")

(* false *)
let ff : expression = Exp.construct (mknoloc (Longident.Lident "false")) None

(* variable pattern *)
let var x : pattern = Pat.var (mknoloc x)

(* fun x -> 1 *)
let fun_x_one : expression = Exp.fun_ Nolabel None (var "x") one

(* let a = 1 in fun x -> 1 *)
let exp1 : expression =
  Exp.let_ Nonrecursive [Vb.mk (var "a") one] fun_x_one

let env : Env.t = Env.initial_safe_string

(* infer type of exp1 *)
let (str1', _, _) =
  Typemod.type_structure env [Str.eval exp1] Location.none

(* type of x *)
let (typx1, _) = split_arrow (extract_typ str1')

let b1 = Ctype.moregeneral env false typx1 (Btype.newgenvar ())

;; print_endline (if b1 then "true" else "false")

(* assert false *)
let assert_false : expression = Exp.assert_ ff

(* let a = assert false in fun x -> 1 *)
let exp2 : expression =
  Exp.let_ Nonrecursive [Vb.mk (var "a") assert_false] fun_x_one

(* infer type of exp2 *)
let (str2', _, _) =
  Typemod.type_structure env [Str.eval exp2] Location.none

(* type of x *)
let (typx2, _) = split_arrow (extract_typ str2')

let b2 = Ctype.moregeneral env false typx2 (Btype.newgenvar ())

;; print_endline (if b2 then "true" else "false")

[-- Attachment #3: Makefile --]
[-- Type: text/plain, Size: 167 bytes --]

run : main
	./main

main : main.ml
	ocamlfind ocamlc -package compiler-libs.common,compiler-libs.bytecomp -linkpkg main.ml -o main

clean :
	rm main main.cmi main.cmo

Re: [Caml-list] Question on "more general"

[Leo White]

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

Without looking too closely at your question I would assume that is just
the value restriction.

Regards,

Leo

On 19 April 2017 at 11:40, Kenichi Asai <asai@is.ocha.ac.jp> wrote:

> Dear OCaml type inference experts,
>
> If I infer the type (using Typemod.type_structure) of:
>
> let a = 1 in fun x -> 1
>
> and see if the type of x is more general (using Ctype.moregeneral)
> than the type of a type variable (Btype.newgenvar ()), I obtain yes
> (since the type of x is 'a which is more general (or equal) than a
> newly created type variable, I guess).  If I do the same for:
>
> let a = assert false in fun x -> 1
>
> I obtain no, although it still seems that the type of x is the same
> 'a.  (See attached file for the concrete program I executed.  I used
> OCaml 4.04.0.)  Why?
>
> Thank you in advance!
>
> --
> Kenichi Asai
>
> --
> 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: 1848 bytes --]

Re: [Caml-list] Question on "more general"

[Kenichi Asai]

> Without looking too closely at your question I would assume that is just the
> value restriction.

But both in the expressions:

>     let a = 1 in fun x -> 1
>     let a = assert false in fun x -> 1

the variable a is not used in fun x -> 1.  How can the type of x be
affected by an unused binding for a around fun x -> 1?

It also seems that assert false can be used polymorphically (because
of the relaxed value restriction?):

# fun () -> let a = assert false in (a 1, a true);;
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
- : unit -> 'a * 'b = <fun>

-- 
Kenichi Asai

Re: [Caml-list] Question on "more general"

[Leo White]

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

The expression:

  let a = assert false in
    fun x -> 1

is not a syntactic value, so because of the value restriction it has type:

    '_a -> int

That '_a comes from the `x` parameter.

> the variable a is not used in fun x -> 1

OCaml doesn't take account of whether `a` is used in deciding if something
is a value, although if you had written:

  ignore (assert false);
  fun x -> 1

then it would have been a value.

I suspect the part you are missing is that generalization happens as part
of `let` (and `match`, class definitions, polymorphic record creation,
etc...). If you had written:

  let a = assert false in
  let f = fun x -> 1 in
  f

then the type associated with `x` would have been generalized as part of
the definition of `f` although the resulting function would still have type:

  '_a -> int

Regards,

Leo


On 20 April 2017 at 01:15, Kenichi Asai <asai@is.ocha.ac.jp> wrote:

> > Without looking too closely at your question I would assume that is just
> the
> > value restriction.
>
> But both in the expressions:
>
> >     let a = 1 in fun x -> 1
> >     let a = assert false in fun x -> 1
>
> the variable a is not used in fun x -> 1.  How can the type of x be
> affected by an unused binding for a around fun x -> 1?
>
> It also seems that assert false can be used polymorphically (because
> of the relaxed value restriction?):
>
> # fun () -> let a = assert false in (a 1, a true);;
> Warning 20: this argument will not be used by the function.
> Warning 20: this argument will not be used by the function.
> - : unit -> 'a * 'b = <fun>
>
> --
> Kenichi Asai
>

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

Re: [Caml-list] Question on "more general"

[Kenichi Asai]

Thank you!  That's very clear.  So instead of writing assert false, if
I could write a "value" of type 'a, then the type of x becomes 'a.

I confirmed it with the following file:

--------------------------------
let v = assert false

let g1 = let a = v in
         let f = fun x -> 1 in
         f

let g2 = let a = assert false in
         let f = fun x -> 1 in
         f
--------------------------------

If I see the types of variables via "ocamlc -i", I obtained:

val v : 'a
val g1 : 'a -> int
val g2 : '_a -> int

Thank you again!

-- 
Kenichi Asai

Re: [Caml-list] Question on "more general"

[Ivan Gotovchits]

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

A small update.

But before the update, let me clarify the original reason, why the
expression `let a = assert false in fun x -> 1` is not generalized. The
reason is because the `assert false` is not nonexpansive (sorry for the
double negation). A nonexpansive value, in OCaml compiler parlance, is a
value that has "no _observable_ side effects". The `assert false` is
currently typed as a special expression, that is assumed to have a side
effect (i.e., it is expansive).  Thus, it is basically treated the same as
`let a = print_int 1 in fun x -> 1` that is also not generalized, as the
evaluation of the `print_int 1 in fun x -> 1` has some effect.

Apparently, the assumption that `assert false` is expansive was too
conservative, as it was already subsumed (in some cases) with the value
restriction relaxation. So it will be relaxed soon, see GPR#1142 [1]. And
soon both of your functions will have the same type.



[1]: https://github.com/ocaml/ocaml/pull/1142

On Thu, Apr 20, 2017 at 11:13 AM, Kenichi Asai <asai@is.ocha.ac.jp> wrote:

> Thank you!  That's very clear.  So instead of writing assert false, if
> I could write a "value" of type 'a, then the type of x becomes 'a.
>
> I confirmed it with the following file:
>
> --------------------------------
> let v = assert false
>
> let g1 = let a = v in
>          let f = fun x -> 1 in
>          f
>
> let g2 = let a = assert false in
>          let f = fun x -> 1 in
>          f
> --------------------------------
>
> If I see the types of variables via "ocamlc -i", I obtained:
>
> val v : 'a
> val g1 : 'a -> int
> val g2 : '_a -> int
>
> Thank you again!
>
> --
> Kenichi Asai
>
> --
> 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: 2929 bytes --]