[Caml-list] Weird types

[Caml-list] Weird types

[Berke Durak]

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
admit that this is an expressly constructed pathologic case. However
it's derived from the much less pathologic following :

type min = Min of (int -> int -> int)
type max = Max of (int -> int -> int)
type ('a,'b,'c) game_tree =
type Leaf of 'c | Branch of 'a * 'c * ('b,'a,'c) game_tree list
type ('a,'b,'c) game = Game of 'a * 'b * ('a,'b,'c) game

let min = Min(compare)
let max = Max((fun x y -> - compare x y))

let bad_game =
	Game(min,max,
			Branch(max,None,[Branch(max,None,[Leaf(None)]);
			Branch(max,None,[Branch(min,None,[Leaf(None)])])]))

let a_game =
	Game(min,max,
		Branch(max,
    	       ref None,
        	   [Branch(min,
					   ref None,
                	   [Leaf(ref (Some 6.12389));
						Leaf(ref (Some 3.49348))]);
				Branch(min,
					   ref None,
        	           [Leaf(ref (Some 1.372645));
						Branch(max,
        	                   ref None,
        	                   [Leaf(ref (Some 1.481743));
								Leaf(ref (Some 2.481743));
								Leaf(ref (Some 3.481743));
								Leaf(ref (Some 4.481743))])])])

where the typing is used to ensure that each level in the game tree
contains only nodes of the same type and that no two consecutive
levels are of the same type.
--
Berke Durak
-------------------
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

[Caml-list] Weird types

[Berke Durak]

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
admit that this is an expressly constructed pathologic case. However
it's derived from the much less pathologic following case :

type min = Min of (int -> int -> int)
type max = Max of (int -> int -> int)
type ('a,'b,'c) game_tree =
	  Leaf of 'c
	| Branch of 'a * 'c * ('b,'a,'c) game_tree list
type ('a,'b,'c) game = Game of 'a * 'b * ('a,'b,'c) game_tree

let min = Min(compare)
let max = Max((fun x y -> - compare x y))

let bad_game =
	Game(min,max,
			Branch(max,None,
				[Branch(max,None,[Leaf(None)]);
				 Branch(max,None,[Branch(min,None,[Leaf(None)])])])

let a_game =
	Game(min,max,
		Branch(max,
    	       ref None,
        	   [Branch(min,
					   ref None,
                	   [Leaf(ref (Some 6.12389));
						Leaf(ref (Some 3.49348))]);
				Branch(min,
					   ref None,
        	           [Leaf(ref (Some 1.372645));
						Branch(max,
        	                   ref None,
        	                   [Leaf(ref (Some 1.481743));
								Leaf(ref (Some 2.481743));
								Leaf(ref (Some 3.481743));
								Leaf(ref (Some 4.481743))])])])

where the typing is used to ensure that each level in the game tree
contains only nodes of the same type and that no two consecutive
levels are of the same type.
--
Berke Durak
-------------------
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

Re: [Caml-list] Weird types

[Tyng-Ruey Chuang]

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

Re: [Caml-list] Weird types

[Jean-Christophe Filliatre]

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

Re: [Caml-list] Weird types

[Tyng-Ruey Chuang]

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 = <fun>
> val gamma' : ('a, 'b, 'c) t -> int = <fun>
> ======================================================================

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

Re: [Caml-list] Weird types

[Didier Remy]

Tyng-Ruey Chuang <trc@iis.sinica.edu.tw> writes:

> 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 = <fun>
> > val gamma' : ('a, 'b, 'c) t -> int = <fun>
> > ======================================================================
> 
> Interesting! But then size of the duplicated code grows exponentially.

Actually, you can share a little more: 

        let gamma_body gamma = function 
           | A _ -> 0
           | B x -> 1 + gamma x

        let rec gamma  x = gamma_body gamma' x 
            and gamma' x = gamma_body gamma  x;;
        ;;

and a for three parameters: 

        type ('a, 'b, 'c) sigma = 
          | I of 'a * 'b * 'c 
          | T of ('b, 'a, 'c) sigma
          | P of ('b, 'c, 'a) sigma

        let body gT gP = function
           | I _ -> 0
           | T x -> 1 + gT x
           | P x -> 1 + gP x

        let rec abc s = body bac bca s
            and acb s = body cab cba s
            and bac s = body abc acb s
            and bca s = body cba cab s
            and cab s = body acb abc s
            and cba s = body bca bac s
        ;;

Didier
-------------------
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