From: Alain Frisch <Alain.Frisch@inria.fr>
To: Remi Vanicat <remi.vanicat@gmail.com>
Cc: "O'Caml Mailing List" <caml-list@inria.fr>,
Chris King <colanderman@gmail.com>
Subject: Re: [Caml-list] Unexpected '_a problem
Date: Wed, 02 Aug 2006 09:00:19 +0200 [thread overview]
Message-ID: <44D04D83.5020503@inria.fr> (raw)
In-Reply-To: <6b8a91420608011509s696233cew8d499f315aa0cba9@mail.gmail.com>
Remi Vanicat wrote:
> But for a reson I don't
> fully understood, one cannot do:
>
> # let f () (_ : 'a -> unit) = ();;
> val f : unit -> ('a -> unit) -> unit = <fun>
> # f ();;
> - : ('_a -> unit) -> unit = <fun>
See the paper _Relaxing the value restriction_ by Jacques Garrigue (
http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/morepoly-long.pdf
), page 15: dangerous type variables (which are not generalized when the
right-hand side of the let-binding is not a value) are not only those is
contravariant position - this would be enough to ensure type soundness -
but also those which appear in a contravariant branch (e.g. anywhere on
the left of an arrow) - this is necessary to ensure that the type system
has principal types.
Let me reformulate the example given in the paper. Consider the
top-level binding:
let f = print_newline (); fun x -> raise Exit
Semantically, it would be sound to give g a polymorphic type:
\forall 'a,'b. 'a -> 'b. However, the relaxed value restriction does not
try to be that clever; it decides which variables to generalize only by
looking at the type of the bound expression (when it is not a
syntactical value). Here are two possible types for the expression:
'a -> 'b
('c -> 'd) -> 'b
Generalizing all variables in covariant positions would give these two
type schemes:
\forall 'b. 'a -> 'b ('a monomorphic)
\forall 'b,'c. ('c -> 'd) -> 'b ('d monomorphic)
The only type-scheme which is more general than these two
would be \forall 'a,'b. 'a -> 'b, but this one is not ok (a
contravariant variable has been generalized).
To retrieve principality, the type system has been designed so that
the variable 'c above would not be generalized (it is on the left of an
arrow), which makes the type scheme \forall 'b. ('c -> 'd) -> 'b
less general than \forall 'b. ('a -> 'b) (which is the principal type
scheme inferred by OCaml).
-- Alain
next prev parent reply other threads:[~2006-08-02 7:00 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2006-08-01 20:47 Chris King
2006-08-01 21:20 ` [Caml-list] " Andreas Rossberg
2006-08-01 22:09 ` Remi Vanicat
2006-08-02 7:00 ` Alain Frisch [this message]
2006-08-02 17:57 ` Chris King
2006-08-04 2:42 ` Jacques Garrigue
2006-08-04 14:18 ` Chris King
2006-08-02 7:03 ` Christophe Dehlinger
2006-08-02 8:07 ` Andreas Rossberg
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=44D04D83.5020503@inria.fr \
--to=alain.frisch@inria.fr \
--cc=caml-list@inria.fr \
--cc=colanderman@gmail.com \
--cc=remi.vanicat@gmail.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox