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 JAA12000; Mon, 18 Jun 2001 09:14:30 +0200 (MET DST) 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 JAA12338 for ; Mon, 18 Jun 2001 09:14:29 +0200 (MET DST) Received: from ext.lri.fr (ext.lri.fr [129.175.15.4]) by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id f5I7ETn23937 for ; Mon, 18 Jun 2001 09:14:29 +0200 (MET DST) Received: from pc803.lri.fr (IDENT:root@pc803 [129.175.8.114]) by ext.lri.fr (8.11.1/jtpda-5.3.2) with ESMTP id f5I7EN508722 ; Mon, 18 Jun 2001 09:14:23 +0200 (MET DST) Received: by pc803.lri.fr (8.9.3/feuille) id JAA17952 ; Mon, 18 Jun 2001 09:14:24 +0200 X-Authentication-Warning: localhost.localdomain: filliatr set sender to filliatr@pc803 using -f From: Jean-Christophe Filliatre MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <15149.43599.979056.554953@pc803> Date: Mon, 18 Jun 2001 09:14:23 +0200 (MEST) To: Tyng-Ruey Chuang Cc: caml Subject: Re: [Caml-list] Weird types In-Reply-To: <3B2B9947.4B5EF0C3@iis.sinica.edu.tw> References: <20010616013618.A13696@localhost.localdomain> <3B2B9947.4B5EF0C3@iis.sinica.edu.tw> X-Mailer: VM 6.49 under Emacs 20.4.1 Reply-To: Jean-Christophe.Filliatre@lri.fr (Jean-Christophe Filliatre) Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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 = ====================================================================== In gamma, argument is of type ('a,'b,'c) t and gamma' is called on x of type ('b,'a,'c) t; and gamma' is calling gamma similarly. Of course, it duplicated code, which is bad practice, but avoids Obj.magic, which is also bad practice :-) Similar (although different) typing issues are discussed in a nice paper by Chris Okasaki (which can be accessed at http://www.cs.columbia.edu/~cdo/papers.html#icfp99) but are solved using rank-2 polymorphism. Hope this helps, -- Jean-Christophe FILLIATRE mailto:Jean-Christophe.Filliatre@lri.fr http://www.lri.fr/~filliatr Tyng-Ruey Chuang writes: > Berke Durak wrote: > > > > I have a type > > > > 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 > > > > and a function > > > > let rec gamma = function > > I _ -> 0 | > > T x -> 1 + (gamma x) | > > P x -> 1 + (gamma x) > > > > and want a version of gamma that works on the following data > > > > type t1 = X1 and t2 = X2 and t3 = X3 and > > t4 = X4 and t5 = X5 and t6 = X6 and t7 = X7 > > > > let data = I(X1,X2,X3,X4,X5,X6,X7) > > > > and that is under 10K of length. Any clever way to solve this ? .... > > > I am not sure people at INRIA will recommend this, but one can > use Obj.magic to coerce the compiler to accept unsafe value definitions. > For example, > > let rec gamma s = > match s with > I _ -> 0 > | T x -> 1 + Obj.magic gamma x > | P x -> 1 + Obj.magic gamma x > > will be inferred as > > val gamma : ('a, 'b, 'c, 'd, 'e, 'f, 'g) sigma -> int = > > In this particular case, function gamma is safe to have the above type > because, by its definition, values of types 'a, 'b, 'c, 'd, 'e, 'f, and > 'g > are always ignored. > > If we define > > let i = I (X1, X2, X3, X4, X5, X6, X7) > let rec t n = if n <= 0 then i else T (t' (n-1)) > and t' n = if n <= 0 then T i else T (t (n-1)) > > then (t (2*k)) will return a "length (2*k)" sigma value, and > (t' (2*k+1)) will return a "length (2*k+1)" sigma value. Functions t > and t' are nicely inferred by the compiler to have types > > val t : int -> (t1, t2, t3, t4, t5, t6, t7) sigma = > val t' : int -> (t2, t1, t3, t4, t5, t6, t7) sigma = > > Troubles are, (t (2*k-1)) also has length (2*k). > Also, (t' (2*k)) has length (2*k+1). This is no good, > but one probably cannot do better. > > It can also be inferred that sigma values of the same length may > not have the same type. (P (t (2*k))) and (t' (2*k+1)) both have > length (2*k+1), but with different types: > > let t'10k1 = t' 10001 > let t10k = t 10000 > let pt10k = P t10k > > let (u, v) = (gamma pt10k, gamma t'10k1) > > We get > > val t'10k1 : (t2, t1, t3, t4, t5, t6, t7) sigma = ... > val t10k : (t1, t2, t3, t4, t5, t6, t7) sigma = ... > val pt10k : (t7, t1, t2, t3, t4, t5, t6) sigma = ... > val u : int = 10001 > val v : int = 10001 > > > By the way, people call type constructors like sigma "irregular": > sigma is applied to different type expresions at the two sides > of the its own type equation. > > A self-contained code fragment is appended for your amusement. > Have fun! > > Tyng-Ruey Chuang > > -------------------- > > 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 > > let rec gamma s = > match s with > I _ -> 0 > | T x -> 1 + Obj.magic gamma x > | P x -> 1 + Obj.magic gamma x > > type t1 = X1 > and t2 = X2 > and t3 = X3 > and t4 = X4 > and t5 = X5 > and t6 = X6 > and t7 = X7 > > let i = I (X1, X2, X3, X4, X5, X6, X7) > let rec t n = if n <= 0 then i else T (t' (n-1)) > and t' n = if n <= 0 then T i else T (t (n-1)) > > let t'10k1 = t' 10001 > let t10k = t 10000 > let pt10k = P t10k > > let (u, v) = (gamma pt10k, gamma t'10k1) > ------------------- > 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 ------------------- 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