Re: [Caml-list] typechecking

[Yaron Minsky <yminsky@janestreet.com>]

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