Browse thread
Type inference question
-
Julien Verlaguet
-
Jean-Christophe Filliatre
-
Mark Shinwell
- Andreas Rossberg
- Jacques Garrigue
-
Mark Shinwell
-
Jean-Christophe Filliatre
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Jacques Garrigue <garrigue@m...> |
| Subject: | Re: [Caml-list] Type inference question |
From: Mark Shinwell <Mark.Shinwell@cl.cam.ac.uk> > However, in the Marshal example above, we have > > Marshal.from_channel stdin [] > > in the first part of the "let". In the SML terminology, this is not a > "nonexpansive expression"[*] (unlike "fun x -> x"). Therefore, I would > have thought that the appearance of such an expression here would > prohibit generalisation (in order to prevent possible unsoundness in the > presence of mutable state). This is presumably not the case in OCaml: > can someone explain why? Because ocaml now uses an improvement of the so-called "value restriction". Rather than refusing to generalize any variable in expansive expressions, it generalizes covariant ones, as they cannot be used in an unsound way. (See "Relaxing the value restriction" at http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/) What we see here is a consequence of that for functions which are known as typing holes: any function that returns a totally unconstrained result (as input_value or Obj.magic) allows this result to be generalized. Actually, for Obj.magic this is a good thing: you sometimes want the result to be polymorphic (this is not a real function anyway). For input_value this is subject for discussion, but anyway this function is a glaring hole in the type system... maybe we should have a way to explicitly require its result to be annotated with a ground type! Jacques Garrigue