Re: [Caml-list] Type inference and marshalling

[malc <av1474@comtv.ru>]

On Wed, 6 Jul 2011, Jacques Garrigue wrote:

> On 2011/07/06, at 14:11, malc wrote:
> 
> > On Wed, 6 Jul 2011, Jacques Garrigue wrote:
> > 
> >> On 2011/07/05, at 22:59, malc wrote:
> >> 
> >>> Perhaps someone could explain why following behaves the way it does:
> >>> 
> >>> ~$ ocaml
> >>>       Objective Caml version 3.11.2
> >>> 
> >>> # let f ic = let i = input_value ic in let j = i + 1 in LargeFile.seek_in ic i;;
> >>> Warning Y: unused variable j.
> >>> val f : in_channel -> unit = <fun>
> >> 
> >> The return type of input_value being 'a, which gets generalized by the
> >> relaxed value restriction, i gets the polymorphic type "forall 'a. 'a".
> >> So you can use it both as an int and an int64.
> >> ==> input_value is an unsafe function, you should always write a type
> >> 	annotation on its return type.
> > 
> > Sure i'm well aware of that, but to me "let j = i + 1" means that i has
> > type int and after that "LargeFile.seek ic i" makes no sense yet is
> > accepted by the type checker.
> 
> But this is just the definition of let polymorphism...

Thing is - the original code looked something like this:

let offset = input_value ic in
Printf.printf "%d" offset;
LargeFile.seek_in other_ic offset;

And it also worked... and caught me by surprise..

> If the type of a let-bound value  contains variables, they can be generalized
> (with some restriction for soundness).
> So i can perfectly have several types.
> What makes no sense here is the return type of input_value,
> yet this cannot be avoided since there is currently no mechanism
> in ocaml to actually check the type of the value received.
> 
> I have no simple solution for this with the current standard library.
> A potential way to avoid this problem would be to force the user to
> provide a monomorphic type:
> 
> module type T = sig type t end
> 
> let input_value ic (type a) (t : (module T with type t = a)) : a =
>   Pervasives.input_value ic
> 
> let f ic =
>   let i =
>     input_value ic (module struct type t = int end : T with type t = int) in
>   let _ = i + 1 in seek_in ic i;;
> 
> This is verbose, but some syntactic sugar could be easily provided.
> In the long term, safe input primitives are the solution.
> 

-- 
mailto:av1474@comtv.ru