Re: [Caml-list] typechecking

[Jonathan Protzenko <jonathan.protzenko@gmail.com>]

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
>