Re: [Camllist] Weird types
 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 (08:06) 
From:  TyngRuey Chuang <trc@i...> 
Subject:  Re: [Camllist] Weird types 
JeanChristophe FILLIATRE wrote: > 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> > ====================================================================== Interesting! But then size of the duplicated code grows exponentially. For example, for a 3ary 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 7ary 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 languagesupported polymorphic recursions will help here. However, I believe the general problem of typing polymorphic recursive functions had been shown to be undecidable. TyngRuey Chuang  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