[Camllist] Weird types

Berke Durak

TyngRuey Chuang
 JeanChristophe Filliatre

TyngRuey Chuang
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20010618 (07:14) 
From:  JeanChristophe Filliatre <JeanChristophe.Filliatre@l...> 
Subject:  Re: [Camllist] Weird types 
Actually, there is a typeable 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 = <fun> val gamma' : ('a, 'b, 'c) t > int = <fun> ====================================================================== 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 rank2 polymorphism. Hope this helps,  JeanChristophe FILLIATRE mailto:JeanChristophe.Filliatre@lri.fr http://www.lri.fr/~filliatr TyngRuey 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 = <fun> > > 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' (n1)) > and t' n = if n <= 0 then T i else T (t (n1)) > > 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 = <fun> > val t' : int > (t2, t1, t3, t4, t5, t6, t7) sigma = <fun> > > Troubles are, (t (2*k1)) 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 selfcontained code fragment is appended for your amusement. > Have fun! > > TyngRuey 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' (n1)) > and t' n = if n <= 0 then T i else T (t (n1)) > > 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/camlbugs FAQ: http://caml.inria.fr/FAQ/ > To unsubscribe, mail camllistrequest@inria.fr Archives: http://caml.inria.fr  Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ To unsubscribe, mail camllistrequest@inria.fr Archives: http://caml.inria.fr