[Caml-list] typechecking

[Caml-list] typechecking

[Misha Aizatulin]

  Using ocaml 4.00.1 the program below successfully compiles. I think
this should be rejected because the call (f t) forces t to be of type t2
whereas the annotation on input function requires it to be of type t1.

type t1 = T1
type t2 = T2

let f T2 = ()

let input (c : in_channel) : t1 =
  let t = input_value c in
  f t;
  t

Re: [Caml-list] typechecking

[Daniel Bünzli]

Le samedi, 22 mars 2014 à 21:02, Misha Aizatulin a écrit :
> type t1 = T1
> type t2 = T2
>  
> let f T2 = ()
>  
> let input (c : in_channel) : t1 =
> let t = input_value c in
> f t;
> t

Unmarshaling is not type-safe, you always need to add a type annotation when you input_value. See the warning in the documentation here [1]. Your program should read:

type t1 = T1
type t2 = T2

let f T2 = ()

let input (c : in_channel) : t1 =
let t = (input_value c : t1) in
f t;
t



Which the compiler rejects.  

Best,

Daniel

[1] http://caml.inria.fr/pub/docs/manual-ocaml-4.01/libref/Marshal.html

Re: [Caml-list] typechecking

[Yaron Minsky]

Marshal is of course not type-safe, but it's still worth explaining
why this happens.  My type-theory is weak, but I'll do my best.

A naive mental model of type-checking is that the application of [f]
should require [t] to be of type [t2], and the constraint in the
return value should constrain [t] to be of type [t1], and thus there
should be a type-error.  Here are some examples that emphasize the
point.

utop[2]> let z () : t1 = let t = Obj.magic () in f t; t;;
val z : unit -> t1 = <fun>

If [t] comes in as an argument, we get the expected error:

utop[10]> let z t : t1 = f t; t;;
Error: This expression has type t2 but an expression was expected of type t1

The issue here, I think, is that the result of Obj.magic (or
input_value) is truly polymorphic, so it's simultaneously compatible
with all types.  And the fact that it's in some contexts where it's
used doesn't mean its definition is constrained.  A value passed in as
an argument, however, is monomorphic within the body of the function.

Here's a similar example, without using Obj.magic, just using an empty
list, whose type is truly polymorphic.

utop[11]> let z () : t1 list = let t = [] in ignore (List.map ~f t); t;;
val z : unit -> t1 list = <fun>

On the other hand, if we constraint t at the definition time, we get a
type error, because that makes the type not polymorphic.

utop[13]> let z () : t1 list = let t = ([] : t2 list) in t;;
Error: This expression has type t2 list but an expression was expected of type
         t1 list
       Type t2 is not compatible with type t1

In the end, Daniel's advice of annotating the value at its creation
point is sound, but it's worth understanding why.

y

On Sun, Mar 23, 2014 at 7:40 AM, Daniel Bünzli
<daniel.buenzli@erratique.ch> wrote:
> Le samedi, 22 mars 2014 à 21:02, Misha Aizatulin a écrit :
>> type t1 = T1
>> type t2 = T2
>>
>> let f T2 = ()
>>
>> let input (c : in_channel) : t1 =
>> let t = input_value c in
>> f t;
>> t
>
> Unmarshaling is not type-safe, you always need to add a type annotation when you input_value. See the warning in the documentation here [1]. Your program should read:
>
> type t1 = T1
> type t2 = T2
>
> let f T2 = ()
>
> let input (c : in_channel) : t1 =
> let t = (input_value c : t1) in
> f t;
> t
>
>
>
> Which the compiler rejects.
>
> Best,
>
> Daniel
>
> [1] http://caml.inria.fr/pub/docs/manual-ocaml-4.01/libref/Marshal.html
>
> --
> 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

Re: [Caml-list] typechecking

[Jonathan Protzenko]

I was also surprised by this example, and I kind of expected 
input_value to have type in_channel -> '_a. However, input_value is 
defined as follows:

stdlib/pervasives.ml
365:external input_value : in_channel -> 'a = "caml_input_value"

Since writing '_a is not allowed, I guess there's not much we can do 
here.

Cheers,

~ jonathan

On Sat 22 Mar 2014 11:12:10 PM CET, Yaron Minsky wrote:
> Marshal is of course not type-safe, but it's still worth explaining
> why this happens.  My type-theory is weak, but I'll do my best.
>
> A naive mental model of type-checking is that the application of [f]
> should require [t] to be of type [t2], and the constraint in the
> return value should constrain [t] to be of type [t1], and thus there
> should be a type-error.  Here are some examples that emphasize the
> point.
>
> utop[2]> let z () : t1 = let t = Obj.magic () in f t; t;;
> val z : unit -> t1 = <fun>
>
> If [t] comes in as an argument, we get the expected error:
>
> utop[10]> let z t : t1 = f t; t;;
> Error: This expression has type t2 but an expression was expected of type t1
>
> The issue here, I think, is that the result of Obj.magic (or
> input_value) is truly polymorphic, so it's simultaneously compatible
> with all types.  And the fact that it's in some contexts where it's
> used doesn't mean its definition is constrained.  A value passed in as
> an argument, however, is monomorphic within the body of the function.
>
> Here's a similar example, without using Obj.magic, just using an empty
> list, whose type is truly polymorphic.
>
> utop[11]> let z () : t1 list = let t = [] in ignore (List.map ~f t); t;;
> val z : unit -> t1 list = <fun>
>
> On the other hand, if we constraint t at the definition time, we get a
> type error, because that makes the type not polymorphic.
>
> utop[13]> let z () : t1 list = let t = ([] : t2 list) in t;;
> Error: This expression has type t2 list but an expression was expected of type
>          t1 list
>        Type t2 is not compatible with type t1
>
> In the end, Daniel's advice of annotating the value at its creation
> point is sound, but it's worth understanding why.
>
> y
>
> On Sun, Mar 23, 2014 at 7:40 AM, Daniel Bünzli
> <daniel.buenzli@erratique.ch> wrote:
>> Le samedi, 22 mars 2014 à 21:02, Misha Aizatulin a écrit :
>>> type t1 = T1
>>> type t2 = T2
>>>
>>> let f T2 = ()
>>>
>>> let input (c : in_channel) : t1 =
>>> let t = input_value c in
>>> f t;
>>> t
>>
>> Unmarshaling is not type-safe, you always need to add a type annotation when you input_value. See the warning in the documentation here [1]. Your program should read:
>>
>> type t1 = T1
>> type t2 = T2
>>
>> let f T2 = ()
>>
>> let input (c : in_channel) : t1 =
>> let t = (input_value c : t1) in
>> f t;
>> t
>>
>>
>>
>> Which the compiler rejects.
>>
>> Best,
>>
>> Daniel
>>
>> [1] http://caml.inria.fr/pub/docs/manual-ocaml-4.01/libref/Marshal.html
>>
>> --
>> 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
>

Re: [Caml-list] typechecking

[oleg]

Misha Aizatulin wrote:
> type t1 = T1
> type t2 = T2
>
> let f T2 = ()
>
> let input (c : in_channel) : t1 =
>   let t = input_value c in
>   f t;
>   t

The expression input_value c has the type 'a. The variable t is
let-bound, so it receives the generalized, polymorphic type
        forall 'a. 'a
In the expression [f t] this polymorphic type is instantiated to t1.
In [t], the last expression of [input], the polymorphic type is
instantiated to t2. There are no problems.

One may shout: wait a minute! The expression [input_value c]
is not syntactically a value. Therefore, the value restriction should
prevent generalization. The classical value restriction indeed does
prevent. But OCaml has a relaxed value restriction. For example, the
following legitimate code

        let foo () = []
                val foo : unit -> 'a list = <fun>
        let f [1] = ()
                val f : int list -> unit = <fun>
        let bar () : char list =
          let t = foo () in
          f t;
          t
                val bar : unit -> char list = <fun>

typechecks in OCaml -- but it wouldn't under the classical
value restriction. The paper

    Jacques Garrigue: Relaxing the Value Restriction.
    Proc. Int. Symposium on Functional and Logic Programming, Nara, April 2004. 
    LNCS 2998, pp. 196--213. (extended version: RIMS Preprint 1444)
    < http://www.math.nagoya-u.ac.jp/~garrigue/papers/morepoly-long.pdf >

explains very well why the original value restriction is too
restrictive.

So, what to do about the original problem?

Jonathan Protzenko recommended:
> I was also surprised by this example, and I kind of expected
> input_value to have type in_channel -> '_a.
> Since writing '_a is not allowed, I guess there's not much we can do here.

Although writing the type '_a in a type annotation is not allowed,
internally such a type could be ascribed to a value (I side-step murky
separate compilation issues that creates). So, one could have
input_value of the type Jonathan wants. Alas, that is too
restrictive. Consider

        let ll = ref [];;
                val ll : '_a list ref = {contents = []}
        let input_list (c:in_channel) = !ll;;
                val input_list : in_channel -> '_a list = <fun>

        let c = open_in "/dev/null" in
        (1::input_list c, true::input_list c)

        Error: This expression has type int list
        but an expression was expected of type bool list
        Type int is not compatible with type bool 

Some if input_value has the type Jonathan suggest, we can only use
input_value to read the values of the same type.

One solution is to give input_value a sound type such as the
following:

        val input_value : 'a -> in_channel -> 'a

That is, input_value should receive _some_ value of the type it is
supposed to read. The user must provide the evidence that the type to
read is populated. One problem: it is too
cumbersome in practice. The second problem is that function types are
all populated -- by, for example, [fun _ -> failwith "black hole"].

The complete solution is to update the function
        generalize_expansive in typing/ctype.ml
which is responsible for implementing the relaxed value restriction.
The type 'a should not be considered co-variant in 'a. Alas, such a
modification is a bit cumbersome since generalize_expansive is called
recursively. One have to split cases. It is not clear how much benefit
can be gained -- complicating type checker for the sake of a rare
error.

Re: [Caml-list] typechecking

[Jacques Garrigue]

On 2014/03/23 13:41, oleg@okmij.org wrote:

> The complete solution is to update the function
>        generalize_expansive in typing/ctype.ml
> which is responsible for implementing the relaxed value restriction.
> The type 'a should not be considered co-variant in 'a. Alas, such a
> modification is a bit cumbersome since generalize_expansive is called
> recursively. One have to split cases. It is not clear how much benefit
> can be gained -- complicating type checker for the sake of a rare
> error.

I don't think it would make sense anyway.
I suppose your rationale is that since 'a is empty in the sound part
of the language, if you actually get a value of this type it must be
unsound, and should not be generalized.
However, this would just be a hack, and would not catch all such
errors. For instance 'a list contains the empty list, so we have no reason
not to generalize it, but an unsound function might still return a
non empty list with this type.
Moreover, there are also useful applications of the generalization of 'a.
For instance, the following idiom allows you to give an arbitrary polymorphic
type to a non-value, which you cannot under the strict value restriction.

	let y = Obj.magic (f x)
	let z : ('a -> 'a) t = y

So well, unsound functions are unsound, and you have to live with that.
In particular _always_ annotate with ground types.

Jacques Garrigue

Re: [Caml-list] typechecking

[Alain Frisch]

On 03/23/2014 01:59 PM, Jacques Garrigue wrote:
> So well, unsound functions are unsound, and you have to live with that.
> In particular _always_ annotate with ground types.

It might be useful to check that the user provides an explicit type for 
the result of input_value and similar functions.  This could be 
implemented in the same way as the new warning on deprecated 
declarations, i.e. with a compiler-recognized attribute on those special 
functions:


  val input_value: in_channel -> 'a
     [@@requires_explicit_type]


The compiler would raise a warning if the call site does not provide 
explicit type information such as:

    let x : ... = input_value ic in ...

or:

   let x = (input_value ic : x) in ...


The notion of "explicit type information" could probably be the same as 
the one used for type propagation, or even a more syntactic criterion.


-- Alain