Browse thread
Type constraints
[
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: | 2004-12-08 (03:30) |
From: | nakata keiko <keiko@k...> |
Subject: | Re: [Caml-list] Type constraints |
Damien Doligez wrote: >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). This does not answer to me why this works, #type t = { t : 'a. 'a -> 'a} #let v = let module M = struct let t x = x end in {t = M.t} in (v.t 5, v.t true) Of cource, both of the following are not type checked, #let v = let module M = struct let t = x end in M.t in (v 5, v true) #let v : 'a -> 'a = let module M = struct let t x = x end in M.t in (v 5, v true) However, if I can write something like #let v : 'a. 'a -> 'a = let module M = struct let t x = x end in M.t in (v 5, v true) then, it would be type checked ? Regards, Keiko.