From: Jim Farrand <jim@farrand.net>
To: caml-list@inria.fr
Subject: Type constraints
Date: Mon, 6 Dec 2004 19:55:27 +0000 [thread overview]
Message-ID: <20041206195527.GA32094@draco.skynet> (raw)
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
next reply other threads:[~2004-12-06 19:55 UTC|newest]
Thread overview: 27+ messages / expand[flat|nested] mbox.gz Atom feed top
2004-12-06 19:55 Jim Farrand [this message]
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
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=20041206195527.GA32094@draco.skynet \
--to=jim@farrand.net \
--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).