Re: [Caml-list] Weird types

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>]

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 = <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 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 = <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' (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 = <fun>
 > 	val t' : int -> (t2, t1, t3, t4, t5, t6, t7) sigma = <fun>
 > 
 > 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