cyclic types

cyclic types

[Radu Grigore]

Why are cyclic types forbidden?

I was forced to use the definition:
  type forest = Forest of forest StringMap.t | Empty
where I would have rather used
  type forest = forest StringMap.t
The error is:
  The type abbreviation tree is cyclic

I can see that the later would require type annotations such as
  StringMap.empty : forest
because otherwise the compiler could never infer that some expression
has type forest.  But this is a rather minor nuisance compared to the
need to match Forest/Empty all over the place. You could write:

let rec make n sf = match n, sf with
  [], [] -> StringMap.empty : forest
| nh :: nt, sfh :: sft ->
  let m = make nt sft in
  StringMap.add nh sfh m
| _ -> failwith "n and sf should have the same number of elements";;

let rec iter func frst =
  let nf el sub_frst = func el; iter func sub_frst in
  StringMap.iter nf frst;;
 
Instead of what you need to write now:

let rec make n sf = match n, sf with
  [], [] -> Empty
| nh :: nt, sfh :: sft -> begin
    match make nt sft with
      Empty -> Forest (StringMap.add nh sfh StringMap.empty)
    | Forest m -> Forest (StringMap.add nh sfh m) end
| _ -> failwith "blabla..";;

let rec iter func frst =
  let nf el sub_frst = func el; iter func sub_frst in
  match frst with
    Empty -> ()
  | Forest m -> StringMap.iter nf m;;

It feels strange to be forced to explicitly treat the case of an empty
map, which is what actually happens in the code that compiles. The
first version of make/iter seems better, but it does not compile :(

Also, the type definition
  type forest = forest StringMap.t option
fails with the same error (cyclic type) although it looks a lot like
the version that works. Why?

-- 
regards,
 radu
http://rgrig.idilis.ro/

Re: cyclic types

[Radu Grigore]

On Sat, 29 Jan 2005 14:15:43 +0200, Radu Grigore <radugrigore@gmail.com> wrote:
> I was forced to use the definition:
>   type forest = Forest of forest StringMap.t | Empty

I realized now that
  type forest = Forest of forest StringMap.t
works just as well. The code would look a lot like the version I
wanted but it would still have some unnecessary
constructions/deconstructions.

-- 
regards,
 radu
http://rgrig.idilis.ro/

Re: [Caml-list] cyclic types

[Remi Vanicat]

On Sat, 29 Jan 2005 14:15:43 +0200, Radu Grigore <radugrigore@gmail.com> wrote:
> Why are cyclic types forbidden?
> 
> I was forced to use the definition:
>   type forest = Forest of forest StringMap.t | Empty
> where I would have rather used
>   type forest = forest StringMap.t
> The error is:
>   The type abbreviation tree is cyclic

You can use the -rectypes of the ocaml compiler or toplevel to allow
cyclic type.

Re: [Caml-list] cyclic types

[brogoff]

On Sat, 29 Jan 2005, Remi Vanicat wrote:
> On Sat, 29 Jan 2005 14:15:43 +0200, Radu Grigore <radugrigore@gmail.com> wrote:
> > Why are cyclic types forbidden?
> >
> > I was forced to use the definition:
> >   type forest = Forest of forest StringMap.t | Empty
> > where I would have rather used
> >   type forest = forest StringMap.t
> > The error is:
> >   The type abbreviation tree is cyclic
>
> You can use the -rectypes of the ocaml compiler or toplevel to allow
> cyclic type.

This comes up relatively frequently, and it is known that having -rectypes
as the default is not a good idea. However, wouldn't explicit typing of
this case sidestep the known problems and eliminate the need for a
-rectypes option here?

-- Brian

Re: [Caml-list] cyclic types

[Radu Grigore]

On Sat, 29 Jan 2005 09:12:59 -0800 (PST), brogoff <brogoff@speakeasy.net> wrote:

> This comes up relatively frequently, and it is known that having -rectypes
> as the default is not a good idea. However, wouldn't explicit typing of
> this case sidestep the known problems and eliminate the need for a
> -rectypes option here?

For now I have setteled for
  type forest = Forest of forest StringMap.t

Can you give an example of why rectypes by default is dangerous?

-- 
regards,
 radu
http://rgrig.idilis.ro/

Re: [Caml-list] cyclic types

[skaller]

On Sun, 2005-01-30 at 04:12, brogoff wrote:
> On Sat, 29 Jan 2005, Remi Vanicat wrote:
> > On Sat, 29 Jan 2005 14:15:43 +0200, Radu Grigore <radugrigore@gmail.com> wrote:
> > > Why are cyclic types forbidden?
> > >
> > > I was forced to use the definition:
> > >   type forest = Forest of forest StringMap.t | Empty
> > > where I would have rather used
> > >   type forest = forest StringMap.t
> > > The error is:
> > >   The type abbreviation tree is cyclic
> >
> > You can use the -rectypes of the ocaml compiler or toplevel to allow
> > cyclic type.
> 
> This comes up relatively frequently, and it is known that having -rectypes
> as the default is not a good idea. However, wouldn't explicit typing of
> this case sidestep the known problems and eliminate the need for a
> -rectypes option here?

Do you mean something like:

	type rec forest = forest StringMap.t

where the 'rec' means 'just this type is meant to be cyclic'
(and treat that type as if -rectypes had been given)?

[or types, if there is an 'and' given]


-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net

Re: [Caml-list] cyclic types

[Damien Doligez]

On Jan 29, 2005, at 18:33, Radu Grigore wrote:

> For now I have setteled for
>   type forest = Forest of forest StringMap.t
>
> Can you give an example of why rectypes by default is dangerous?

IIRC, rectypes are off by default because they trade a small increment
in expressive power for a large degradation of the intelligibility of
type-checking error messages.  I don't think they are dangerous in the
sense of breaking the type system.

-- Damien

Re: [Caml-list] cyclic types

[brogoff]

On Sun, 30 Jan 2005, Damien Doligez wrote:
> On Jan 29, 2005, at 18:33, Radu Grigore wrote:
> > Can you give an example of why rectypes by default is dangerous?
>
> IIRC, rectypes are off by default because they trade a small increment
> in expressive power for a large degradation of the intelligibility of
> type-checking error messages.  I don't think they are dangerous in the
> sense of breaking the type system.

Right, that's what I meant. They certainly don't break the type system.
There was a fairly lengthy discussion of this topic about 5 years ago, but
since browsing the archives now is a lot harder than when I started, I'll let
someone else dig up the pointer.

In almost all cases, you can achieve the effect of -rectypes by introducing
an extra constructor.

I think the degradation in intelligibility you mention is only in the case of
-rectypes being the default. If (optional) type annotations could drive the
inference, I think we'd have the best of both worlds. It seems like
FPL type systems are going to have to move in the direction of the more
programmer supplied annotations anyways.

-- Brian

Re: [Caml-list] cyclic types

[Radu Grigore]

On Sun, 30 Jan 2005 00:47:23 +0100, Damien Doligez
<damien.doligez@inria.fr> wrote:

> IIRC, rectypes are off by default because they trade a small increment
> in expressive power for a large degradation of the intelligibility of
> type-checking error messages.  I don't think they are dangerous in the
> sense of breaking the type system.

Thank you.

Only one (small) problem remains. I do not understand this:

# type t = t StringMap.t option;;
The type abbreviation t is cyclic
# type t = Some of t StringMap.t | None;;
type t = Some of t StringMap.t | None


-- 
regards,
 radu
http://rgrig.idilis.ro/

Re: [Caml-list] cyclic types

[brogoff]

On Sat, 30 Jan 2005, skaller wrote:
> On Sun, 2005-01-30 at 04:12, brogoff wrote:
> > This comes up relatively frequently, and it is known that having -rectypes
> > as the default is not a good idea. However, wouldn't explicit typing of
> > this case sidestep the known problems and eliminate the need for a
> > -rectypes option here?
>
> Do you mean something like:
>
> 	type rec forest = forest StringMap.t
>
> where the 'rec' means 'just this type is meant to be cyclic'
> (and treat that type as if -rectypes had been given)?

No, I meant just accept the cyclic types as we do now with -rectypes, but
annotate the functions that use them, something like this (pseudo OCaml)

type ('a, 'b) t = 'a * (('a , 'b) t -> 'b) list

let foo : 'a -> (('a * ('b -> 'c) list as 'b) -> 'c = fun n m ->
    (List.assoc n m) m

Nice huh, the type is longer than the actual code :-(. Anyways, I rememeber
someone complaining about the overhead of the connstructor wrapping in order to
do this in real OCaml (that is, without -rectypes) and this does away with that.

If it were just cyclic types, it wouldn't be a big deal, but there are other
places that explicit types driving the typing could pay off. There are a couple
of ways to  get nonuniform recursion in OCaml but (with the exception of perhaps
the *experimental* recursive module feature) they're clunky workarounds. The
right way is just to annotate the functions with their types.

-- Brian

Re: [Caml-list] cyclic types

[William Lovas]

On Sun, Jan 30, 2005 at 08:05:23AM +0200, Radu Grigore wrote:
> Only one (small) problem remains. I do not understand this:
> 
> # type t = t StringMap.t option;;
> The type abbreviation t is cyclic
> # type t = Some of t StringMap.t | None;;
> type t = Some of t StringMap.t | None

The first is a type abbreviation, while the second is a datatype
declaration.  They both introduce a new type, in some sense: the first does
so by asserting its equality to some existing type, while the second does
so by defining one or more coercions from existing types to the new type
(i.e. constructors).  Only the second can refer to the type being defined
on the right-hand side, for the reasons mentioned earlier.

cheers,
William

Re: [Caml-list] cyclic types

[Xavier Leroy]

> For now I have setteled for
>   type forest = Forest of forest StringMap.t

This is a very reasonable thing to do.  That, or compile with -rectypes.

> Can you give an example of why rectypes by default is dangerous?

Recursive types don't break type soundness and are handled fine by the
OCaml typechecker -- objects and variants use them in an essential way.

The "danger" is that they cause obviously wrong code to pass
type-checking and receive "impossible" recursive types, so you notice
the problem not at the point of definition of the bad code, but at
point of use.  A simplified example is this:

      let f x = x :: x

where the author of that code really intended

      let f x = x @ x

With -rectypes, the wrong definition (with ::) is accepted with type

val f : ('a list as 'a) -> 'a list = <fun>

and it's only when you try to apply f to a "normal" list that the
problem arises, with a hard-to-understand error message:

f [1;2;3];;
   ^
This expression has type int but is here used with type 'a list as 'a

- Xavier Leroy

Re: [Caml-list] cyclic types

[sejourne_kevin]

Xavier Leroy a écrit :
>>For now I have setteled for
>>  type forest = Forest of forest StringMap.t
> 
> 
> This is a very reasonable thing to do.  That, or compile with -rectypes.
> 
> 
>>Can you give an example of why rectypes by default is dangerous?
> 
> 
> Recursive types don't break type soundness and are handled fine by the
> OCaml typechecker -- objects and variants use them in an essential way.
> 
> The "danger" is that they cause obviously wrong code to pass
> type-checking and receive "impossible" recursive types, so you notice
> the problem not at the point of definition of the bad code, but at
> point of use.  A simplified example is this:
> 
>       let f x = x :: x
> 
> where the author of that code really intended
> 
>       let f x = x @ x
> 
> With -rectypes, the wrong definition (with ::) is accepted with type
> 
> val f : ('a list as 'a) -> 'a list = <fun>
> 
> and it's only when you try to apply f to a "normal" list that the
> problem arises, with a hard-to-understand error message:
> 
> f [1;2;3];;
>    ^
> This expression has type int but is here used with type 'a list as 'a
> 
> - Xavier Leroy


It should be nice this kind of explanations is available in the 
documentation of the compiler rather than on a mailing list.

Kévin

Re: [Caml-list] cyclic types

[Christophe Raffalli]

[-- Attachment #1: Type: text/plain, Size: 3501 bytes --]


> 
>       let f x = x :: x
> 
> where the author of that code really intended
> 
>       let f x = x @ x
> 
> With -rectypes, the wrong definition (with ::) is accepted with type
> 
> val f : ('a list as 'a) -> 'a list = <fun>
> 
> and it's only when you try to apply f to a "normal" list that the
> problem arises, with a hard-to-understand error message:
> 
> f [1;2;3];;
>    ^
> This expression has type int but is here used with type 'a list as 'a
> 

Why do you think 'a list as 'a is an <<"impossible" recursive types>> ?
It is a very nice representation of ordinals up to epsilon_0 (curious, 
see the code below)

Why not this restriction: accept a recursive type 't as 'a only if
access to 'a in t needs to expand a definition. I mean, the cyclicity 
check at the end of unification could check that one traverses 
definition. I am not sure how OCaml treat type annotation, this will 
work only if the compiler does its best to use all type annotation.

'a list as 'a is illegal

and let f x = x @ x is illegal

type ord = ord list is legal (all type definition should be legal)

let f (x:ord) = x @ x is legal

code for curious:
--------------------------8<----------------
(* need -rectypes *)

(*
   a very short representation of ordinals up to epsilon_0 as a fixpoint 
of list
*)
type ord = ord list


(* comparison: you must normalize ordinal before comparison *)
let rec compare  (o1:ord) (o2:ord) = match o1, o2 with
   | [], [] -> 0
   | [], _ -> -1
   | _, [] -> 1
   | x::o1', y::o2' ->
       match compare x y with
	-1 -> compare o1' o2
       | 1 -> compare o1 o2'
       | 0 -> compare o1' o2'

let lesseq o1 o2 = compare o1 o2 <= 0

(* compute the normal form of an ordinal*)
let rec normalize (o1:ord) =
   List.sort (fun x y -> compare y x) (List.map normalize o1)

let zero = ([] : ord)
let un = ([[]] : ord)
let deux = ([[];[]] : ord)
let omega = ([[[]]] : ord)
let deux_omega = ([[[]];[[]]] : ord)
let omega_square = ([[[];[]]] : ord)
let omega_to_the_omega = ([[[[]]]] : ord)

let addition (o1:ord) (o2:ord) = o1 @ o2

let rec multiplication (o1:ord) (o2:ord) = match o1, o2 with
   [], _ -> [] (* zero * o2 = zero *)
| _, [] -> [] (* o1 * zero = zero *)
| ([]::o1'), _ -> (* (1 + o1') * o2 = o2 + o1' * o2 *)
   addition o2 (multiplication o1' o2)
| _, ([]::o2') -> (* o1 * (1 + o2') = o1 + o1 * o2' *)
   addition o1 (multiplication o1 o2')
| (o1''::o1'),(o2''::o2') ->
     (* (w^o1'' + o1')*(w^o2'' + o2') = w^(o1''+o2'') + o2'*w^o1'' +
             o1'*w^o2'' + o1'*o2' *)
     (addition o1'' o2'')::(multiplication [o1''] o2')@
     (multiplication o1' [o2''])@(multiplication o1' o2')

(* test *)
let _ = compare [[]] [[];[]]
let _ = compare [[[]];[]] [[];[[]]]
let _ = compare [[[]]] [[];[[]]]
let _ = compare omega_to_the_omega omega_square
let _ = normalize [[];[[]]]
let _ = normalize [[[];[]];[];[[]]]
let quatre = multiplication deux deux
let quatre_omega = multiplication omega quatre
let big = normalize (multiplication omega_to_the_omega quatre_omega)


-- 
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
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution
can check this signature. The public key is
stored on www.keyserver.net
---------------------------------------------

[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 252 bytes --]