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 KAA13248; Mon, 18 Jun 2001 10:06:24 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id KAA13535 for ; Mon, 18 Jun 2001 10:06:23 +0200 (MET DST) Received: from iiserv.iis.sinica.edu.tw (iiserv.iis.sinica.edu.tw [140.109.20.250]) by nez-perce.inria.fr (8.11.1/8.10.0) with ESMTP id f5I86HL19913 for ; Mon, 18 Jun 2001 10:06:17 +0200 (MET DST) Received: from iota.iis.sinica.edu.tw (iota [140.109.20.164]) by iiserv.iis.sinica.edu.tw (8.11.1/8.11.1) with ESMTP id f5I88MX23702; Mon, 18 Jun 2001 16:08:22 +0800 (CST) Received: (from trc@localhost) by iota.iis.sinica.edu.tw (8.8.8+Sun/8.8.8) id QAA18021; Mon, 18 Jun 2001 16:04:32 +0800 (CST) From: Tyng-Ruey Chuang Message-Id: <200106180804.QAA18021@iota.iis.sinica.edu.tw> Subject: Re: [Caml-list] Weird types To: caml-list@inria.fr Date: Mon, 18 Jun 2001 16:04:32 +0800 (CST) Cc: trc@iis.sinica.edu.tw (Tyng-Ruey Chuang), Jean-Christophe.Filliatre@lri.fr (Jean-Christophe Filliatre) In-Reply-To: <15149.43599.979056.554953@pc803> from "Jean-Christophe Filliatre" at Jun 18, 2001 09:14:23 AM X-Mailer: ELM [version 2.5 PL2] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Jean-Christophe FILLIATRE wrote: > Actually, there is a type-able way of writing this function, which > consists in duplicating it into two functions, like this: > > ====================================================================== > type ('a,'b,'c) t = > | A of 'a * 'b * 'c > | B of ('b, 'a, 'c) t > > let rec gamma = function > | A _ -> 0 > | B x -> 1 + gamma' x > > and gamma' = function > | A _ -> 0 > | B x -> 1 + gamma x > ====================================================================== > > which gives the expected types: > > ====================================================================== > val gamma : ('a, 'b, 'c) t -> int = > val gamma' : ('a, 'b, 'c) t -> int = > ====================================================================== Interesting! But then size of the duplicated code grows exponentially. For example, for a 3-ary type constructor sigma type ('a, 'b, 'c) sigma = I of 'a * 'b * 'c | T of ('b, 'a, 'c) sigma | P of ('b, 'c, 'a) sigma one need to define the 6 equivalent "length" functions gamma_xxx, where xxx ranges from {abc, acb, bac, bca, cab, cba}, by let rec gamma_abc s = match s with I _ -> 0 | T x -> 1 + gamma_bac x | P x -> 1 + gamma_bca x and gamma_acb s = match s with I _ -> 0 | T x -> 1 + gamma_cab x | P x -> 1 + gamma_cba x and gamma_bac s = match s with I _ -> 0 | T x -> 1 + gamma_abc x | P x -> 1 + gamma_acb x and gamma_bca s = match s with I _ -> 0 | T x -> 1 + gamma_cba x | P x -> 1 + gamma_cab x and gamma_cab s = match s with I _ -> 0 | T x -> 1 + gamma_acb x | P x -> 1 + gamma_abc x and gamma_cba s = match s with I _ -> 0 | T x -> 1 + gamma_bca x | P x -> 1 + gamma_bac x For the original definition of 7-ary sigma type ('a,'b,'c,'d,'e,'f,'g) sigma = I of 'a * 'b * 'c * 'd * 'e * 'f * 'g | T of ('b,'a,'c,'d,'e,'f,'g) sigma | P of ('b,'c,'d,'e,'f,'g,'a) sigma one probably will need 7! = 5040 equivalent "length" functions that are recursively defined among themselves! I guess language-supported polymorphic recursions will help here. However, I believe the general problem of typing polymorphic recursive functions had been shown to be undecidable. Tyng-Ruey Chuang ------------------- 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