* Type constraints
@ 2004-12-06 19:55 Jim Farrand
2004-12-07 7:12 ` [Caml-list] " Alain Frisch
0 siblings, 1 reply; 27+ messages in thread
From: Jim Farrand @ 2004-12-06 19:55 UTC (permalink / raw)
To: caml-list
Hi,
I am writing a camlp4 extension to implement dynamic types in O'Caml[1].
I am doing this by generating run-time type representations of values.
When a value is "made dynamic" I tag it with type information. Then
when it is later "made static" I check the tagged type information
against the type the value is being cast to.
(* x is a dynamic value with type Dynamic.t *)
value x = (10 => dynamic int) ;
(* y has type int. *)
value y = (x => static int) ;
(* y has type string *)
value z = (x => static string) ;
(* (But as x doesn't have an int, this raises a Type_error exception) *)
When generating the code for the first example, I have to check that x
really has type int, so that the run-time type information I output
matches the actual type.. I do this by introducing a type constraint.
(x : int)
This works fine for monomorphic value, but I now want to extend to
polymorphic values. The idea is that if you have a value, which has a
polymorphic type, eg.
value x = ((fun x -> x) => dynamic 'a -> 'a) ;
The problem is that the type constraint generated,
((fun x -> x) : 'a -> 'a)
does not reject values with a less general type. This is fine when the
type given matches the function, as it does above, but causes me
problems if the type given is less general.
For example,
value x = ((fun x -> x) => dynamic 'a -> int) ;
yields
((fun x -> x) : 'a -> int)
which is happily compiled by ocaml (I want to reject it).
(To understand why this is a problem, consider the code
value y = (x => static 'a -> int) ;
My extension will accept this as the type matches the type given when
the value was made dynamic. I can now do
value z = y "foo" ; (** Ooops! Just cast a string to an int!! *)
How can I achieve this?
It occurs to me that if I declared a record with a polymorphic type
{ foo : ! 'a . 'a -> 'a }
then values with the intended type are accepted
value t = { foo = id }
wherease values with a less general type are not
value t = { foo = (id : 'a -> int) } ; (** Type error *)
It seems logical to me that I should be able to use similar syntax in
type constraints, eg. (id : ! 'a . 'a -> 'a), and I think that if I
could, I could use this to solve my problems.
Objective Caml version 3.09+dev3 (2004-10-06)
# #load "camlp4r.cma" ;;
Camlp4 Parsing version 3.09+dev3 (2004-10-06)
# value id x = x ;
value id : 'a -> 'a = <fun>
# (id : ! 'a . 'a -> 'a) ;
This expression has type 'a -> 'a but is here used with type 'b. 'b ->
'b
Why is this?
Thanks in advance, and sorry for such a long post.
Jim
[1] I know that there are all sorts of reasons why I shouldn't be doing
this. I'm not arguing that it's a good idea, but it's certainly
interesting.
--
Jim Farrand
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-06 19:55 Type constraints Jim Farrand
@ 2004-12-07 7:12 ` Alain Frisch
2004-12-07 13:43 ` Damien Doligez
2004-12-07 19:38 ` Jim Farrand
0 siblings, 2 replies; 27+ messages in thread
From: Alain Frisch @ 2004-12-07 7:12 UTC (permalink / raw)
To: Jim Farrand; +Cc: caml-list
Jim Farrand wrote:
> Hi,
> The problem is that the type constraint generated,
>
> ((fun x -> x) : 'a -> 'a)
>
> does not reject values with a less general type. This is fine when the
> type given matches the function, as it does above, but causes me
> problems if the type given is less general.
Maybe you can use local structures and signatures:
(e :: s) ==>
let module M : sig val v : s end = struct let v = e end in M.v;;
where s is a type scheme.
Btw, does someone know why in
# let module M : sig val v: 'a -> 'a end = struct let v x = x end in M.v;;
- : '_a -> '_a = <fun>
the type variable is not generalized ?
-- Alain
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
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 19:38 ` Jim Farrand
1 sibling, 1 reply; 27+ messages in thread
From: Damien Doligez @ 2004-12-07 13:43 UTC (permalink / raw)
To: caml users
On 7 Dec 2004, at 08:12, Alain Frisch wrote:
> Btw, does someone know why in
>
> # let module M : sig val v: 'a -> 'a end = struct let v x = x end in
> M.v;;
> - : '_a -> '_a = <fun>
>
> the type variable is not generalized ?
Consider this:
let module M = struct let v = ref end in M.v;;
-- Damien
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-07 13:43 ` Damien Doligez
@ 2004-12-07 14:57 ` Andreas Rossberg
2004-12-07 17:44 ` Damien Doligez
0 siblings, 1 reply; 27+ messages in thread
From: Andreas Rossberg @ 2004-12-07 14:57 UTC (permalink / raw)
To: caml users
Damien Doligez wrote:
> On 7 Dec 2004, at 08:12, Alain Frisch wrote:
>
>> Btw, does someone know why in
>>
>> # let module M : sig val v: 'a -> 'a end = struct let v x = x end in
>> M.v;;
>> - : '_a -> '_a = <fun>
>>
>> the type variable is not generalized ?
>
> Consider this:
>
> let module M = struct let v = ref end in M.v;;
Is this really a counter-example? I don't see any problem with making it
polymorphic - it evaluates to ref, and ref can happily be polymorphic.
- Andreas
--
Andreas Rossberg, rossberg@ps.uni-sb.de
Let's get rid of those possible thingies! -- TB
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-07 14:57 ` Andreas Rossberg
@ 2004-12-07 17:44 ` Damien Doligez
2004-12-07 18:08 ` Alain Frisch
` (2 more replies)
0 siblings, 3 replies; 27+ messages in thread
From: Damien Doligez @ 2004-12-07 17:44 UTC (permalink / raw)
To: caml users
On 7 Dec 2004, at 15:57, Andreas Rossberg wrote:
> Is this really a counter-example? I don't see any problem with making
> it polymorphic - it evaluates to ref, and ref can happily be
> polymorphic.
Yes, well I simplified it a bit too much. Try this instead:
let module M = struct let v = ref [] end in M.v;;
-- Damien
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-07 17:44 ` Damien Doligez
@ 2004-12-07 18:08 ` Alain Frisch
2004-12-07 21:04 ` Damien Doligez
2004-12-07 18:13 ` William Lovas
2004-12-07 18:41 ` Boris Yakobowski
2 siblings, 1 reply; 27+ messages in thread
From: Alain Frisch @ 2004-12-07 18:08 UTC (permalink / raw)
To: Damien Doligez; +Cc: caml users
Damien Doligez wrote:
> Yes, well I simplified it a bit too much. Try this instead:
>
> let module M = struct let v = ref [] end in M.v;;
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
?
Alain
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-07 18:08 ` Alain Frisch
@ 2004-12-07 21:04 ` Damien Doligez
2004-12-07 21:43 ` Alain Frisch
0 siblings, 1 reply; 27+ messages in thread
From: Damien Doligez @ 2004-12-07 21:04 UTC (permalink / raw)
To: caml users
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
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-07 21:04 ` Damien Doligez
@ 2004-12-07 21:43 ` Alain Frisch
2004-12-08 3:30 ` nakata keiko
2004-12-08 10:53 ` Damien Doligez
0 siblings, 2 replies; 27+ messages in thread
From: Alain Frisch @ 2004-12-07 21:43 UTC (permalink / raw)
To: Damien Doligez; +Cc: caml users
Damien Doligez wrote:
> 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.
Ah ok, this explains that:
# let module M = struct end in fun x -> x;;
- : '_a -> '_a = <fun>
Still, I'm not sure to understand the bottomline. Consider:
# module M = struct let v = ref [] end;;
module M : sig val v : '_a list ref end
# M.v;;
- : '_a list ref = {contents = []}
Here M.v is not generalized either. But here it is:
# module M = struct let v x = x end;;
module M : sig val v : 'a -> 'a end
# M.v;;
- : 'a -> 'a = <fun>
So I don't understand why the same cannot apply to local modules. If the
let-module-in were declared "safe" for the value restriction, shouldn't
let module M = struct let v = ref [] end in M.v
yield a non-generalized type for the same reason as for the non-local
case (and not because of the value restriction) ?
-- Alain
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
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-08 10:53 ` Damien Doligez
1 sibling, 1 reply; 27+ messages in thread
From: nakata keiko @ 2004-12-08 3:30 UTC (permalink / raw)
To: damien.doligez; +Cc: caml-list
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.
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-07 21:43 ` Alain Frisch
2004-12-08 3:30 ` nakata keiko
@ 2004-12-08 10:53 ` Damien Doligez
2004-12-08 12:39 ` Alain Frisch
2004-12-08 16:10 ` Xavier Leroy
1 sibling, 2 replies; 27+ messages in thread
From: Damien Doligez @ 2004-12-08 10:53 UTC (permalink / raw)
To: caml users
On 7 Dec 2004, at 22:43, Alain Frisch wrote:
> Damien Doligez wrote:
>
>> 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.
[...]
> So I don't understand why the same cannot apply to local modules. If
> the let-module-in were declared "safe" for the value restriction,
> shouldn't
>
> let module M = struct let v = ref [] end in M.v
>
> yield a non-generalized type for the same reason as for the non-local
> case (and not because of the value restriction) ?
Hmmm... Now I don't know whether it's safe or not, and I don't know
whether someone checked its safety before excluding it from the value
restriction code...
-- Damien
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-08 10:53 ` Damien Doligez
@ 2004-12-08 12:39 ` Alain Frisch
2004-12-08 14:23 ` Jacques Garrigue
2004-12-08 16:10 ` Xavier Leroy
1 sibling, 1 reply; 27+ messages in thread
From: Alain Frisch @ 2004-12-08 12:39 UTC (permalink / raw)
To: Damien Doligez; +Cc: caml users
Damien Doligez wrote:
> Hmmm... Now I don't know whether it's safe or not, and I don't know
> whether someone checked its safety before excluding it from the value
> restriction code...
With this extra line added to is_nonexpansive:
| Texp_letmodule (_,_,e) -> is_nonexpansive e
we get:
# let module M = struct let x = ref [] end in M.x;;
- : 'a list ref = {contents = []}
The non-generalizable status has been forgotten. What I'm not sure is
whether this is only an artefact of the internal representation of
levels to control generalization, or whether there are some deeper issues.
-- Alain
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-08 12:39 ` Alain Frisch
@ 2004-12-08 14:23 ` Jacques Garrigue
2004-12-09 3:07 ` skaller
0 siblings, 1 reply; 27+ messages in thread
From: Jacques Garrigue @ 2004-12-08 14:23 UTC (permalink / raw)
To: Alain.Frisch; +Cc: caml-list
From: Alain Frisch <Alain.Frisch@inria.fr>
> Damien Doligez wrote:
> > Hmmm... Now I don't know whether it's safe or not, and I don't know
> > whether someone checked its safety before excluding it from the value
> > restriction code...
>
> With this extra line added to is_nonexpansive:
>
> | Texp_letmodule (_,_,e) -> is_nonexpansive e
>
> we get:
>
> # let module M = struct let x = ref [] end in M.x;;
> - : 'a list ref = {contents = []}
>
> The non-generalizable status has been forgotten. What I'm not sure is
> whether this is only an artefact of the internal representation of
> levels to control generalization, or whether there are some deeper issues.
It's not really an artefact, just that there is no such thing as a
non-generalizable status: something that is not generalizable in some
context becomes generalizable in a larger context.
So you cannot rely on the generalizability obtained during the typing
of the module. Rather you must check whether the module
itself contains only non-expansive definitions. I.e. you cannot ignore
the definition of the module, as you are doing here.
Yet, modules are strange beasts for typing, so I wouldn't add the code
before thinking it through.
(Note that there is another way to handle non-generalizability,
without relying on a non-expansiveness predicate, raising the
non-generalizable level only when entering functions, and that might
solve the problem for free. Francois Pottier told me he was using
it. However it requires many small changes to type inference, and
doesn't mix well with the new "relaxed" value restriction.)
Jacques Garrigue
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-08 14:23 ` Jacques Garrigue
@ 2004-12-09 3:07 ` skaller
2004-12-09 4:53 ` Jacques Garrigue
0 siblings, 1 reply; 27+ messages in thread
From: skaller @ 2004-12-09 3:07 UTC (permalink / raw)
To: Jacques Garrigue; +Cc: Alain.Frisch, caml-list
On Thu, 2004-12-09 at 01:23, Jacques Garrigue wrote:
> Yet, modules are strange beasts for typing, so I wouldn't add the code
> before thinking it through.
I am curious as to the status of COQ support for verifying
assertions about proposed changes to the type system.
For example supposing you did 'think it through' and it
seemed right, would you be able to then extend an
existing COQ proof and attempt to prove your thinking
mechanically?
--
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850,
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-09 3:07 ` skaller
@ 2004-12-09 4:53 ` Jacques Garrigue
0 siblings, 0 replies; 27+ messages in thread
From: Jacques Garrigue @ 2004-12-09 4:53 UTC (permalink / raw)
To: skaller; +Cc: caml-list
From: skaller <skaller@users.sourceforge.net>
> On Thu, 2004-12-09 at 01:23, Jacques Garrigue wrote:
>
> > Yet, modules are strange beasts for typing, so I wouldn't add the code
> > before thinking it through.
>
> I am curious as to the status of COQ support for verifying
> assertions about proposed changes to the type system.
>
> For example supposing you did 'think it through' and it
> seemed right, would you be able to then extend an
> existing COQ proof and attempt to prove your thinking
> mechanically?
Unfortunately, I'm afraid we are still pretty far from that.
Supposing we could describe all the properties we need in Coq
(probably possible, but far from easy), a very long and harduous
proof is waiting.
If there is a breakthrough, I would be most happy to check everything,
as I know there are bugs in the compiler. I just discovered a stupid
unsoundness today.
Jacques Garrigue
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-08 10:53 ` Damien Doligez
2004-12-08 12:39 ` Alain Frisch
@ 2004-12-08 16:10 ` Xavier Leroy
1 sibling, 0 replies; 27+ messages in thread
From: Xavier Leroy @ 2004-12-08 16:10 UTC (permalink / raw)
To: caml-list
> Hmmm... Now I don't know whether it's safe or not, and I don't know
> whether someone checked its safety before excluding it from the value
> restriction code...
You word it in a slightly backward way: it is always safe to claim
that an expression is expansive and its type should not be
generalized; it's the converse (asserting that an expression is
non-expansive) that is potentially dangerous and requires some
semantic evidence that it is safe. The current treatment of "let
module" as being always expansive just errs on the safe side, in the
absence of this semantic evidence.
> >So I don't understand why the same cannot apply to local modules. If
> >the let-module-in were declared "safe" for the value restriction,
> >shouldn't
> >
> >let module M = struct let v = ref [] end in M.v
> >
> >yield a non-generalized type for the same reason as for the non-local
> >case (and not because of the value restriction) ?
I don't follow you here. So, OK, your expression E above
(E = let module M = struct let v = ref [] end in M.v) has type
alpha list ref for a fresh variable alpha. If we were to classify E
as non-expansive, we could do
let x = E in E'
and in E', x would have polymorphic type forall alpha, alpha list ref,
from which it is easy to break type safety.
So, your example shows that it would be unsafe to say that a "let
module M = A in B" expression is nonexpansive if B is nonexpansive.
One would need to inspect the module expression A to establish that it
is nonexpansive. This is what we do for ordinary "let" expressions:
"let x = A in B" is nonexpansive if both A and B are nonexpansive.
There are two concerns here. The practical one is that the module
language is quite complex and I really don't feel like implementing a
syntactic nonexpansiveness check for module expressions.
The conceptual concern is that the type system for the module language
is somewhat richer than that of the core language -- it has "deep"
polymorphism, subtyping and some forms of dependent types -- so it is
not entirely clear to me that the value restriction and the syntactic
nonexpansiveness criterion that work for the core language would also
work for the module language.
- Xavier Leroy
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-07 17:44 ` Damien Doligez
2004-12-07 18:08 ` Alain Frisch
@ 2004-12-07 18:13 ` William Lovas
2004-12-08 0:27 ` Jacques Garrigue
2004-12-07 18:41 ` Boris Yakobowski
2 siblings, 1 reply; 27+ messages in thread
From: William Lovas @ 2004-12-07 18:13 UTC (permalink / raw)
To: caml users
On Tue, Dec 07, 2004 at 06:44:36PM +0100, Damien Doligez wrote:
>
> On 7 Dec 2004, at 15:57, Andreas Rossberg wrote:
>
> >Is this really a counter-example? I don't see any problem with making
> >it polymorphic - it evaluates to ref, and ref can happily be
> >polymorphic.
>
> Yes, well I simplified it a bit too much. Try this instead:
>
> let module M = struct let v = ref [] end in M.v;;
I'm still not convinced. Yes, the type variable should not be generalized
in the above, by analogy with:
# ref [];;
- : '_a list ref = {contents = []}
But the `let module' in question -- or one similar in spirit, at least --
# let module M = struct let v = fun x -> x end in M.v;;
- : '_a -> '_a = <fun>
is analogous to the expression
# fun x -> x
- : 'a -> 'a = <fun>
in which the type variable *is* generalized.
The following behavior confuses me, too:
# let module M = struct let v = fun x -> x end in (M.v 5, M.v true);;
- : int * bool = (5, true)
This expression has type bool but is here used with type int
# let v =
let module M = struct let v = fun x -> x end in M.v
in
(v 5, v true);;
^^^^
This expression has type bool but is here used with type int
Why is the type variable generalized inside the `let module's body but not
generalized if we pass it to the outside?
So the `ref' example above as a counterexample is at the very least hiding
some of the story. What's really going on here?
William
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-07 18:13 ` William Lovas
@ 2004-12-08 0:27 ` Jacques Garrigue
0 siblings, 0 replies; 27+ messages in thread
From: Jacques Garrigue @ 2004-12-08 0:27 UTC (permalink / raw)
To: wlovas; +Cc: caml-list
From: William Lovas <wlovas@stwing.upenn.edu>
> On Tue, Dec 07, 2004 at 06:44:36PM +0100, Damien Doligez wrote:
> >
> > On 7 Dec 2004, at 15:57, Andreas Rossberg wrote:
> >
> > >Is this really a counter-example? I don't see any problem with making
> > >it polymorphic - it evaluates to ref, and ref can happily be
> > >polymorphic.
> >
> > Yes, well I simplified it a bit too much. Try this instead:
> >
> > let module M = struct let v = ref [] end in M.v;;
>
> I'm still not convinced. Yes, the type variable should not be generalized
> in the above, by analogy with:
>
> # ref [];;
> - : '_a list ref = {contents = []}
>
> But the `let module' in question -- or one similar in spirit, at least --
>
> # let module M = struct let v = fun x -> x end in M.v;;
> - : '_a -> '_a = <fun>
>
> is analogous to the expression
>
> # fun x -> x
> - : 'a -> 'a = <fun>
>
> in which the type variable *is* generalized.
Analogies don't help you here, because the typechecker doesn't work by
analogies, but by explicit rules.
If you're curious, there is a function is_nonexpansive in
typing/typecore.ml. Only expressions for which this function returns
true will be generalized. (This is a direct implementation of the
syntactic value-generalization scheme.)
Now, this function doesn't now about Texp_letmodule, so any use of
this construct will never be generalized. I don't know exactly why
this was omitted, but I see the combination of two possible reasons:
this requires some amount of extra code, and one must assess its
validity. Yet I suppose this could be done.
By the way, the code is already there for immediate objects, so the
alternative approach with polymorphic methods does work (but generates
more code).
# let o = object method v : 'a. 'a -> 'a = fun x -> x end in
fun x -> o#v x;;
- : 'a -> 'a = <fun>
Jacques Garrigue
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-07 17:44 ` Damien Doligez
2004-12-07 18:08 ` Alain Frisch
2004-12-07 18:13 ` William Lovas
@ 2004-12-07 18:41 ` Boris Yakobowski
2 siblings, 0 replies; 27+ messages in thread
From: Boris Yakobowski @ 2004-12-07 18:41 UTC (permalink / raw)
To: caml-list
On Tue, Dec 07, 2004 at 06:44:36PM +0100, Damien Doligez wrote:
>
> On 7 Dec 2004, at 15:57, Andreas Rossberg wrote:
>
> >Is this really a counter-example? I don't see any problem with making
> >it polymorphic - it evaluates to ref, and ref can happily be
> >polymorphic.
>
> Yes, well I simplified it a bit too much. Try this instead:
>
> let module M = struct let v = ref [] end in M.v;;
The question remains : why not generalize type variables which would be
generalized at the end of a non local module? :
# module M = struct let v = ref [] end;;
module M : sig val v : '_a list ref end
# module M = struct let v x = x end;;
module M : sig val v : 'a -> 'a end
# let module M = struct let v = ref [] end in M.v;;
- : '_a list ref = {contents = []}
# let module M = struct let v x = x end in M.v
(* This seems overly restrictive *);;
- : '_a -> '_a = <fun>
Besides:
# type t = {t : 'a. 'a -> 'a};;
type t = { t : 'a. 'a -> 'a; }
# let module M = struct let v x = x end in { t = M.v };;
- : t = {t = <fun>}
--
Boris
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [Caml-list] Type constraints
2004-12-07 7:12 ` [Caml-list] " Alain Frisch
2004-12-07 13:43 ` Damien Doligez
@ 2004-12-07 19:38 ` Jim Farrand
1 sibling, 0 replies; 27+ messages in thread
From: Jim Farrand @ 2004-12-07 19:38 UTC (permalink / raw)
To: Alain Frisch; +Cc: caml-list
On Tue, Dec 07, 2004 at 08:12:20AM +0100, Alain Frisch wrote:
> Maybe you can use local structures and signatures:
> (e :: s) ==>
> let module M : sig val v : s end = struct let v = e end in M.v;;
Thanks for this, I haven't had chance to code it up yet but suspect it
is exactly the solution I was looking for.
Thanks also to those who replied off list with similar hints.
REgards,
Jim
--
Jim Farrand
^ permalink raw reply [flat|nested] 27+ messages in thread
* Type constraints
@ 1997-05-29 18:56 Ernesto Posse
1997-05-30 7:41 ` Pascal Brisset
` (4 more replies)
0 siblings, 5 replies; 27+ messages in thread
From: Ernesto Posse @ 1997-05-29 18:56 UTC (permalink / raw)
To: Caml List
[My apologies for not including a French Version]
Hello. I have the folowing problem. I need to define some interrelated
types as follows:
type 'a node = {x: 'a; y: t1}
and t1 = A | B of t1*t1
and t2 = C | D of (string * t2) node
The interpreter prints the inferred type:
type 'a node = { x: 'a; y: t1 } constraint 'a = string * t2
type t1 = | A | B of t1 * t1
type t2 = | C | D of (string * t2) node
Now, if I add another constructor:
type 'a node = {x: 'a; y: t1}
and t1 = A | B of t1*t1
and t2 = C | D of (string * t2) node | E of bool node
I obtain this message:
Characters 98-102:
This type parameter bool should be an instance of type string * t2
A solution to this would be something like:
type ('a,'b) node = {x: 'a; y: 'b}
and t1 = A | B of t1*t1
and t2 = C | D of (string * t2, t1) node | E of (bool, t1) node
This works, but I am not sure to understand the type clash in the former
example. Why did the type synthetizer infer that constraint?
Thank you for any insights on this.
--
Ernesto Posse
Ingeniero de Sistemas y Computacion
(Systems and Computing Engineer)
Universidad de los Andes
Santafe de Bogota
Colombia
e-mail: mposada@impsat.net.co
^ permalink raw reply [flat|nested] 27+ messages in thread
* Type constraints
1997-05-29 18:56 Ernesto Posse
@ 1997-05-30 7:41 ` Pascal Brisset
1997-05-30 9:24 ` Didier Rousseau
` (3 subsequent siblings)
4 siblings, 0 replies; 27+ messages in thread
From: Pascal Brisset @ 1997-05-30 7:41 UTC (permalink / raw)
To: caml-list
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 852 bytes --]
Ernesto Posse writes:
« type 'a node = {x: 'a; y: t1}
« and t1 = A | B of t1*t1
« and t2 = C | D of (string * t2) node | E of bool node
«
« I obtain this message:
«
« Characters 98-102:
« This type parameter bool should be an instance of type string * t2
It may be compared to a similar expression at the term level:
# let rec f = fun x -> x
and g = f 1, f "1";;
^^^
This expression has type string but is here used with type int
In a recursive definition, occurrences of the defined idents have the
same type everywhere, i.e. the generalization (in your case, 'a is any
type) is done only ``at the end'' of the definition.
At the term level, ML+ is the (undecidable) solution to this kind of
recursive definition. I guess problems are similar at the type level.
A more precise answer from a Caml guru ?
--Pascal Brisset
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Type constraints
1997-05-29 18:56 Ernesto Posse
1997-05-30 7:41 ` Pascal Brisset
@ 1997-05-30 9:24 ` Didier Rousseau
1997-05-30 10:01 ` Vale'rie Me'nissier-Morain
` (2 subsequent siblings)
4 siblings, 0 replies; 27+ messages in thread
From: Didier Rousseau @ 1997-05-30 9:24 UTC (permalink / raw)
To: mposada; +Cc: caml-list
bonjour a tous,
Ernesto Posse wrote:
>
> [My apologies for not including a French Version]
>
> Hello. I have the folowing problem. I need to define some interrelated
> types as follows:
>
> type 'a node = {x: 'a; y: t1}
> and t1 = A | B of t1*t1
> and t2 = C | D of (string * t2) node
>
> The interpreter prints the inferred type:
>
> type 'a node = { x: 'a; y: t1 } constraint 'a = string * t2
> type t1 = | A | B of t1 * t1
> type t2 = | C | D of (string * t2) node
> ...
une solution est de declarer :
type 'a node = {x: 'a; y: t1}
and t1 = A | B of t1*t1
;;
type t2 = C | D of (string * t2) node | E of bool node
;;
Didier Rousseau
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Type constraints
1997-05-29 18:56 Ernesto Posse
1997-05-30 7:41 ` Pascal Brisset
1997-05-30 9:24 ` Didier Rousseau
@ 1997-05-30 10:01 ` Vale'rie Me'nissier-Morain
1997-05-30 11:09 ` Wolfgang Lux
1997-05-30 12:17 ` Jerome Vouillon
4 siblings, 0 replies; 27+ messages in thread
From: Vale'rie Me'nissier-Morain @ 1997-05-30 10:01 UTC (permalink / raw)
To: mposada; +Cc: caml-list
Why do you need to define t2 simultaneously to 'a node and t1?
The following session is ok in Caml Light
> Caml Light version 0.73
#type 'a node = {x: 'a; y: t1}
and t1 = A | B of t1*t1;;
Type node defined.
Type t1 defined.
#type t2 = C | D of (string * t2) node;;
Type t2 defined.
#type t2 = C | D of (string * t2) node | E of bool node;;
Type t2 defined.
#
or, if you prefer in Objective Caml
Objective Caml version 1.05
# type 'a node = {x: 'a; y: t1}
a nd t1 = A | B of t1*t1;;
type 'a node = { x: 'a; y: t1 }
type t1 = | A | B of t1 * t1
# type t2 = C | D of (string * t2) node;;
type t2 = | C | D of (string * t2) node
# type t2 = C | D of (string * t2) node | E of bool node;;
type t2 = | C | D of (string * t2) node | E of bool node
V. Ménissier-Morain
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Type constraints
1997-05-29 18:56 Ernesto Posse
` (2 preceding siblings ...)
1997-05-30 10:01 ` Vale'rie Me'nissier-Morain
@ 1997-05-30 11:09 ` Wolfgang Lux
1997-05-30 12:17 ` Jerome Vouillon
4 siblings, 0 replies; 27+ messages in thread
From: Wolfgang Lux @ 1997-05-30 11:09 UTC (permalink / raw)
To: mposada; +Cc: Caml List
> Hello. I have the folowing problem. I need to define some interrelated
> types as follows:
>
> type 'a node = {x: 'a; y: t1}
> and t1 = A | B of t1*t1
> and t2 = C | D of (string * t2) node
>
> The interpreter prints the inferred type:
>
> type 'a node = { x: 'a; y: t1 } constraint 'a = string * t2
> type t1 = | A | B of t1 * t1
> type t2 = | C | D of (string * t2) node
>
A simple solution to get rid of the type constraint in this case, is to
reorder the type definitions as follows:
type t1 = A | B of t1*t1
type 'a node = {x: 'a; y: t1}
type t2 = C | D of (string * t2) node
> Now, if I add another constructor:
>
> type 'a node = {x: 'a; y: t1}
> and t1 = A | B of t1*t1
> and t2 = C | D of (string * t2) node | E of bool node
>
> I obtain this message:
>
> Characters 98-102:
> This type parameter bool should be an instance of type string * t2
>
> A solution to this would be something like:
>
> type ('a,'b) node = {x: 'a; y: 'b}
> and t1 = A | B of t1*t1
> and t2 = C | D of (string * t2, t1) node | E of (bool, t1) node
>
> This works, but I am not sure to understand the type clash in the former
> example. Why did the type synthetizer infer that constraint?
I'm not absolutely sure on this, but it looks just like another case of
the monomorphic recursion restriction of the Hindley-Milner type system.
>
> Thank you for any insights on this.
>
Hope this helps.
Regards
Wolfgang
----
Wolfgang Lux WZH Heidelberg, IBM Germany
Phone: +49-6221-59-4546 Fax: +49-6221-59-3500
Internet: lux@heidelbg.ibm.com Office: mazvm01(lux)
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Type constraints
1997-05-29 18:56 Ernesto Posse
` (3 preceding siblings ...)
1997-05-30 11:09 ` Wolfgang Lux
@ 1997-05-30 12:17 ` Jerome Vouillon
4 siblings, 0 replies; 27+ messages in thread
From: Jerome Vouillon @ 1997-05-30 12:17 UTC (permalink / raw)
To: Ernesto Posse; +Cc: Caml List
On Thu, 29 May 1997, Ernesto Posse wrote:
> type 'a node = {x: 'a; y: t1}
> and t1 = A | B of t1*t1
> and t2 = C | D of (string * t2) node | E of bool node
>
> I obtain this message:
>
> Characters 98-102:
> This type parameter bool should be an instance of type string * t2
In the current release, in mutually recursive type definitions, all
occurrences of a type being defined (here, for instance, 'a node) must
have the same parameters.
This overly restrictive constraint will be removed in the next
release. In the meantime, as Didier Rousseau noticed, you can move
the definition of type t2 out of the recursive type definition:
type 'a node = {x: 'a; y: t1}
and t1 = A | B of t1*t1
type t2 = C | D of (string * t2) node | E of bool node
-- Jerome Vouillon
^ permalink raw reply [flat|nested] 27+ messages in thread
end of thread, other threads:[~2004-12-09 4:53 UTC | newest]
Thread overview: 27+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2004-12-06 19:55 Type constraints 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
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
-- strict thread matches above, loose matches on Subject: below --
1997-05-29 18:56 Ernesto Posse
1997-05-30 7:41 ` Pascal Brisset
1997-05-30 9:24 ` Didier Rousseau
1997-05-30 10:01 ` Vale'rie Me'nissier-Morain
1997-05-30 11:09 ` Wolfgang Lux
1997-05-30 12:17 ` Jerome Vouillon
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).