From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id VAA20759; Wed, 11 Jul 2001 21:49:44 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 VAA20765 for ; Wed, 11 Jul 2001 21:49:44 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id f6BJnh904050; Wed, 11 Jul 2001 21:49:43 +0200 (MET DST) Received: (from xleroy@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id VAA20757; Wed, 11 Jul 2001 21:49:42 +0200 (MET DST) Date: Wed, 11 Jul 2001 21:49:42 +0200 From: Xavier Leroy To: Christian RINDERKNECHT Cc: caml-list@inria.fr Subject: Re: [Caml-list] Question on typing Message-ID: <20010711214942.C20109@pauillac.inria.fr> References: <20010711155215.B23575@hugo.int-evry.fr> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Mailer: Mutt 1.0i In-Reply-To: <20010711155215.B23575@hugo.int-evry.fr>; from rinderkn@hugo.int-evry.fr on Wed, Jul 11, 2001 at 03:52:15PM +0200 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk > I have a question about typing, but which is not uniquely related to > Caml. > Could someone tell me the reason why a type variable cannot be used as > a type constructor, like in: > > type 'a t = K of bool 'a;; > > or > > type 'a t = {x : 'a 'a};; The latter is ill-sorted :-) > I suspect non-decidability of type inference (higher-order > unification), but I am not an expert of that topic. Also, is type > verification undecidable? Type verification is decidable and not difficult; you basically get the type system known as F_omega, which is contained as a subset in all higher-order logical frameworks such as Coq, as well as in Cardelli's experimental language Quest from the late 80s. As for type inference, one could indeed fear that it involves (undecidable) higher-order unification. I seem to remember that it does not, actually -- at least in the situation you outline above, i.e. with explicit declarations of type constructors. I'm away from my big file of research papers at INRIA, but I believe these ideas have been explored in Haskell ("constructor classes"), in particular by Mark Jones, and found to be quite tractable. - Xavier Leroy ------------------- Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr