From: Damien Doligez <damien.doligez@inria.fr>
To: caml users <caml-list@inria.fr>
Subject: Re: [Caml-list] Type constraints
Date: Tue, 7 Dec 2004 22:04:24 +0100 [thread overview]
Message-ID: <9296F5C2-4893-11D9-8195-000D9345235C@inria.fr> (raw)
In-Reply-To: <41B5F1B2.3000503@inria.fr>
On 7 Dec 2004, at 19:08, Alain Frisch wrote:
> I still don't understand. Compare:
>
> # module M = struct let v = ref [] end;;
> module M : sig val v : '_a list ref end
> # module M : sig val v : 'a -> 'a end = struct let v x = x end;;
> module M : sig val v : 'a -> 'a end
>
> Of course, the type variable in the first example must not be
> generalized, and it isn't. In the second example, there is no problem.
> We get:
>
> # M.v;;
> - : 'a -> 'a = <fun>
>
> So why not give the same type scheme to:
>
> let module M : sig val v : 'a -> 'a end = struct let v x = x end in M.v
The typing algorithm is very simple (really!):
1. Type the module. Generalization occurs and the v field gets a
polymorphic type.
2. Type "M.v". This takes an instance of the polymorphic type.
3. Can we generalize it? Look at the syntactic shape of the expression
(in this case, let module ... in ...). If it is always safe to
generalize such expressions, OK. If not, do not generalize.
That's the beauty of the Wright criterion: it's very easy to implement
and to understand (because it is syntactic), and works well in almost
all
cases (with a little eta-expansion if needed).
So the answer to your original question is: the type is not generalized
because in some cases the let-module construct is not safely
polymorphic.
Of course, there must be some criteria for generalizing more
expressions. Check out Xavier's thesis for example. They are usually
not worth the trouble.
-- Damien
next prev parent reply other threads:[~2004-12-07 21:04 UTC|newest]
Thread overview: 21+ messages / expand[flat|nested] mbox.gz Atom feed top
2004-12-06 19:55 Jim Farrand
2004-12-07 7:12 ` [Caml-list] " Alain Frisch
2004-12-07 13:43 ` Damien Doligez
2004-12-07 14:57 ` Andreas Rossberg
2004-12-07 17:44 ` Damien Doligez
2004-12-07 18:08 ` Alain Frisch
2004-12-07 21:04 ` Damien Doligez [this message]
2004-12-07 21:43 ` Alain Frisch
2004-12-08 3:30 ` nakata keiko
[not found] ` <8002B033-4906-11D9-8195-000D9345235C@inria.fr>
2004-12-09 0:56 ` nakata keiko
2004-12-09 1:27 ` Jacques Garrigue
2004-12-08 10:53 ` Damien Doligez
2004-12-08 12:39 ` Alain Frisch
2004-12-08 14:23 ` Jacques Garrigue
2004-12-09 3:07 ` skaller
2004-12-09 4:53 ` Jacques Garrigue
2004-12-08 16:10 ` Xavier Leroy
2004-12-07 18:13 ` William Lovas
2004-12-08 0:27 ` Jacques Garrigue
2004-12-07 18:41 ` Boris Yakobowski
2004-12-07 19:38 ` Jim Farrand
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=9296F5C2-4893-11D9-8195-000D9345235C@inria.fr \
--to=damien.doligez@inria.fr \
--cc=caml-list@inria.fr \
/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;
as well as URLs for NNTP newsgroup(s).