* Type constraints
@ 1997-05-29 18:56 Ernesto Posse
1997-05-30 7:41 ` Pascal Brisset
` (4 more replies)
0 siblings, 5 replies; 7+ 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] 7+ messages in thread
* Type constraints
1997-05-29 18:56 Type constraints Ernesto Posse
@ 1997-05-30 7:41 ` Pascal Brisset
1997-05-30 9:24 ` Didier Rousseau
` (3 subsequent siblings)
4 siblings, 0 replies; 7+ 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] 7+ messages in thread
* Re: Type constraints
1997-05-29 18:56 Type constraints 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; 7+ 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] 7+ messages in thread
* Re: Type constraints
1997-05-29 18:56 Type constraints 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; 7+ 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] 7+ messages in thread
* Re: Type constraints
1997-05-29 18:56 Type constraints 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; 7+ 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] 7+ messages in thread
* Re: Type constraints
1997-05-29 18:56 Type constraints Ernesto Posse
` (3 preceding siblings ...)
1997-05-30 11:09 ` Wolfgang Lux
@ 1997-05-30 12:17 ` Jerome Vouillon
4 siblings, 0 replies; 7+ 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] 7+ messages in thread
* Type constraints
@ 2004-12-06 19:55 Jim Farrand
0 siblings, 0 replies; 7+ 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] 7+ messages in thread
end of thread, other threads:[~2004-12-06 19:55 UTC | newest]
Thread overview: 7+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
1997-05-29 18:56 Type constraints 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
2004-12-06 19:55 Jim Farrand
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).