From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id D9CE3BB81 for ; Mon, 6 Dec 2004 20:55:30 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id iB6JtUKG001634 for ; Mon, 6 Dec 2004 20:55:30 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id UAA24928 for ; Mon, 6 Dec 2004 20:55:29 +0100 (MET) Received: from galaxy.systems.pipex.net (galaxy.systems.pipex.net [62.241.162.31]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id iB6JtTog004561 for ; Mon, 6 Dec 2004 20:55:29 +0100 Received: from draco.dyndns.org (81-178-106-202.dsl.pipex.com [81.178.106.202]) by galaxy.systems.pipex.net (Postfix) with ESMTP id EAFADE000242 for ; Mon, 6 Dec 2004 19:55:28 +0000 (GMT) Received: from jim by draco.dyndns.org with local (Exim 4.42) id 1CbOxD-0004Dy-VR for caml-list@inria.fr; Mon, 06 Dec 2004 19:55:27 +0000 Date: Mon, 6 Dec 2004 19:55:27 +0000 From: Jim Farrand To: caml-list@inria.fr Subject: Type constraints Message-ID: <20041206195527.GA32094@draco.skynet> Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline X-Mail-Key: JimbosMagicMailKey X-Miltered: at nez-perce with ID 41B4B932.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 41B4B931.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; o'caml:01 run-time:01 run-time:01 ocaml:01 foo:01 foo:01 syntax:01 parsing:01 exception:01 polymorphic:01 polymorphic:01 expression:01 logical:01 dev:01 dev:01 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr X-Spam-Status: No, score=0.1 required=5.0 tests=FORGED_RCVD_HELO autolearn=disabled version=3.0.0 X-Spam-Level: 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 = # (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