[Caml-list] Cyclic ?!

[Caml-list] Cyclic ?!

[Oleg]

Hi

I'm puzzled by the following compiler behavior:

If I define bin_tree as

type 'a bin_tree = 
           Empty
         | Node of 'a bin_tree * 'a * 'a bin_tree

the compiler accepts it. OTOH if I define it as

type 'a bin_tree = ('a bin_tree * 'a * 'a bin_tree) option

It gives an error: "The type abbreviation bin_tree is cyclic".
Why??? And what's the difference between the two, really?

Thanks
Oleg
-------------------
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/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

RE: [Caml-list] Cyclic ?!

[Michael Hicks]

If memory serves, ML datatypes elegantly overload about three distrinct
type-theoretic constructs.  In particular, the variant tags in the data
type definition double as the "witnesses" to coercions between an
iso-recursive type and its "unrolling" of one level.  Without going into
detail, this is why you can define something like

type foo = Rec of foo;;

but you can't define

type foo = foo;;

The latter definition is in the style of "equi-recursive" types, in
which a recursive type is equivalent any number of its unrollings.  This
formulation is harder to typecheck, as I recall.  There is a similar
analogy between the two definitions of bin_tree that you present.

Mike

-----Original Message-----
From: owner-caml-list@pauillac.inria.fr
[mailto:owner-caml-list@pauillac.inria.fr] On Behalf Of Oleg
Sent: Wednesday, August 14, 2002 10:20 PM
To: caml-list@inria.fr
Subject: [Caml-list] Cyclic ?!

Hi

I'm puzzled by the following compiler behavior:

If I define bin_tree as

type 'a bin_tree = 
           Empty
         | Node of 'a bin_tree * 'a * 'a bin_tree

the compiler accepts it. OTOH if I define it as

type 'a bin_tree = ('a bin_tree * 'a * 'a bin_tree) option

It gives an error: "The type abbreviation bin_tree is cyclic".
Why??? And what's the difference between the two, really?

Thanks
Oleg
-------------------
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/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
-------------------
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/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Cyclic ?!

[Oleg]

Hi

I'm not sure I understand you. If the two definitions are equivalent WRT 
Empty <-> None & Node <-> Some name substitution, then the fact that the 
compiler accepts one, but not the other must be a bug, yes?

Regards
Oleg

On Thursday 15 August 2002 10:31 am, Michael Hicks wrote:
> If memory serves, ML datatypes elegantly overload about three distrinct
> type-theoretic constructs.  In particular, the variant tags in the data
> type definition double as the "witnesses" to coercions between an
> iso-recursive type and its "unrolling" of one level.  Without going into
> detail, this is why you can define something like
>
> type foo = Rec of foo;;
>
> but you can't define
>
> type foo = foo;;
>
> The latter definition is in the style of "equi-recursive" types, in
> which a recursive type is equivalent any number of its unrollings.  This
> formulation is harder to typecheck, as I recall.  There is a similar
> analogy between the two definitions of bin_tree that you present.
>
> Mike
>
> -----Original Message-----
> From: owner-caml-list@pauillac.inria.fr
> [mailto:owner-caml-list@pauillac.inria.fr] On Behalf Of Oleg
> Sent: Wednesday, August 14, 2002 10:20 PM
> To: caml-list@inria.fr
> Subject: [Caml-list] Cyclic ?!
>
> Hi
>
> I'm puzzled by the following compiler behavior:
>
> If I define bin_tree as
>
> type 'a bin_tree =
>            Empty
>
>          | Node of 'a bin_tree * 'a * 'a bin_tree
>
> the compiler accepts it. OTOH if I define it as
>
> type 'a bin_tree = ('a bin_tree * 'a * 'a bin_tree) option
>
> It gives an error: "The type abbreviation bin_tree is cyclic".
> Why??? And what's the difference between the two, really?
>
> Thanks
> Oleg
> -------------------
> 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/
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
-------------------
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/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Cyclic ?!

[Markus Mottl]

On Thu, 15 Aug 2002, Oleg wrote:
> I'm not sure I understand you. If the two definitions are equivalent WRT 
> Empty <-> None & Node <-> Some name substitution, then the fact that the 
> compiler accepts one, but not the other must be a bug, yes?

This is not a bug, because you can have the compiler typecheck it using
the command-line flag "-rectypes".

You'll certainly want to know now why this isn't standard behaviour.
Type inference of recursive types is actually neither a theoretical
problem nor an implementation difficulty (basically, I think, you just
need to drop the occurs check during type unification - please correct
me if I'm wrong).

The problem rather is that programmers can accidently write down
meaningless expressions for which the compiler infers absolutely crazy
types. If I remember correctly, OCaml already had the more general rule
by default in some ancient version, but the developers found that this
generality caused more confusion than benefits to programmers...

Regards,
Markus Mottl

-- 
Markus Mottl                                             markus@oefai.at
Austrian Research Institute
for Artificial Intelligence                  http://www.oefai.at/~markus
-------------------
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/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Cyclic ?!

[Brian Smith]

Hi,

Markus Mottl wrote:
> On Thu, 15 Aug 2002, Oleg wrote:
> 
>>I'm not sure I understand you. If the two definitions are equivalent WRT 
>>Empty <-> None & Node <-> Some name substitution, then the fact that the 
>>compiler accepts one, but not the other must be a bug, yes?
> 
> This is not a bug, because you can have the compiler typecheck it using
> the command-line flag "-rectypes".
> 
> The problem rather is that programmers can accidently write down
> meaningless expressions for which the compiler infers absolutely crazy
> types. If I remember correctly, OCaml already had the more general rule
> by default in some ancient version, but the developers found that this
> generality caused more confusion than benefits to programmers...

But, if this is the case, then wouldn't that still apply to other parts 
of a program using recursive types? In other words, if I use one 
recursive type, then I must use -rectypes, but that means that the 
"extra strict checking" that O'Caml normally does won't help me in the 
rest of my program, where I might use recursive types accidently and 
thus cause O'Caml to infer "absolutely crazy types".

I think, instead of a command-line option, it would be better to provide 
a syntactical annotation on each type definition where this behavior is 
desired. That way, the default strict checking would always apply, but 
it can be overridden by somebody that knows they really really want a 
recursive type.

What do you think?

- Brian



-------------------
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/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

[Caml-list] Recursive types (Was Cyclic ?!)

[Christophe Raffalli]

Note: there is a nice exercise at the end of the mail ...

There is a better solution then -rectypes that the developper could 
implement :

Let the us write recursive type annotation in programs, but
when doing the loop detection in the unification used by the 
type-checker, each loop should go
through a type variable that has been created by one of these type 
anotation.

So the only thing you have to add to the type-checker is a marker on 
type variables introduced by the user: if the user write (e : ... as 'a) 
then 'a is marked.

This mark is propagated by unification and the loop detection is 
modified as I suggested.

Therefore, the type-checker will not introduce recursive types by itself 
and the cost is not to much (I have in mind a unification algorithm 
using graph unification followed by loop detection, I do not know if 
this is what OCaml uses, but I guess it is).

--

By the way, here is a nice program using recursive types:
run l n where l is a list of functions from positive int to positive int 
and n is a nat will produce a list of int of size n such that all the 
functions in l are increasing on that list ...

The program prints the lists it tries before finding the good one.

Exercise: try to remove the need for -rectypes ... keeping the same 
algorithm.

--
(* an algorithm extracted (by hand) from the proof of Dickson's lemma *)
(* by C. Raffalli *)
(* compile with ocamlc -rectypes *)

let lem1 f e k =
   let rec k' x q = k (x : int) ((f,k')::q) in
   e k'

let lem2 f u x = lem1 f (u (x : int))

let rec dickson lf =
   match lf with
     [] -> (fun x k -> k x [])
   | f::lf -> lem2 f (dickson lf)

let rec extract n u k =
   match n with
     0 -> k []
   | x ->
     let k' l =
       match l with
	[] -> u 0 (fun x lx -> k [x,lx])
       |	(y, ly)::_ -> u (y+1) (fun z lz -> k ((z,lz)::l))
     in
     extract (x - 1) u k'

let weak_dickson lf n = extract n (dickson lf)

let rec decidable' acc = function
     (y, (ly : (((int -> int) * (int -> 'a -> 'c)) list as 'a)))::l ->
       match l with
	[] -> y::acc
       |	(x,(lx : 'a))::_ ->
	  let rec test lx' ly' =
	    match lx', ly' with
               [], [] -> decidable' (y::acc) l
	    | (((fx : int -> int),( kx : int -> 'a -> 'c))::lx'), (((fy : int -> 
int), (ky : int -> 'a -> 'c))::ly') ->
		if not (fx == fy) then failwith "bug: the function should be the same !";
		if fx x < fx y then
		  ky x lx' else test lx' ly'
	  in test lx ly

let print_list f l =
   List.iter (fun x -> print_int (f x); print_string ", ") l;
   print_newline ()

let count = ref 0

let reset () =
   print_string "Number of tries:"; print_int !count; print_newline ();
   count := 0

let decidable l =
   print_list fst l;
   incr count;
   decidable' [] l;


let run l n =
   let r = weak_dickson l n decidable in
   reset ();
   r
--



-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
-------------------
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/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Cyclic ?!

[John Max Skaller]

Oleg wrote:

> Hi
> 
> I'm puzzled by the following compiler behavior:
> 
> If I define bin_tree as
> 
> type 'a bin_tree = 
>            Empty
>          | Node of 'a bin_tree * 'a * 'a bin_tree
> 
> the compiler accepts it. OTOH if I define it as
> 
> type 'a bin_tree = ('a bin_tree * 'a * 'a bin_tree) option
> 
> It gives an error: "The type abbreviation bin_tree is cyclic".
> Why??? And what's the difference between the two, really?


No semantic difference at all.
But there is a syntactic difference:
ocaml (without -rectypes) only allows cycles across
"object boundaries", that includes across variant
constructor names.

In the 'option' case,
the constructor name in 'option' type (namely "Some")
isn't explicitly separating the LHS and RHS parts of
the declaration. The syntax checker doesn't know
what 'option' is yet, it's just an arbitrary
polymorphic type: it could be:

	type 'a option = 'a

in which case, there really is an error.
Note that a polymorphic type (like option)
could be abstract -- in which case we
don't know it's internals, and there is no
choice but to reject the above style
in that case (assuming we want to enforce the
'no recursion except across object boundaries' rule).

So it seems the check is done *before* the lookup
for the meaning of 'option' which is why
I called it a 'syntax check' -- it is based
entirely on the shape of the declaration
in the abstract -- without considering the meaning
of the subterms.

This makes the rule robust in the face of
substitution (changing 'option' to 'id' for
example, where 'a id = 'a)


-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850


-------------------
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/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners