Re: [Caml-list] typechecking

[oleg@okmij.org]

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.