Re: type recursifs et abreviations cyclique and Co

Re: type recursifs et abreviations cyclique and Co

[Jason Hickey]

Although my French is not what I would like, I gather that the feature
of general recursive types in OCaml has been drawn back because it is
prone to error.  For instance, the type I originally proposed

    type x = x option

is not allowed because types of that form are prone to error.  The
solution would be to apply an explicit boxing:

    type x = X of x option.

I would like to make an argument against this policy.

1.  The interpretation of the general recursive type has a
    well-defined type theoretic meaning.  For instance, the type

        type x = x option

    is isomorphic to the natural numbers.  The _type_theory_ does not
    justify removing it from the language.  Why not issue a warning rather
    than forbidding the construction?  For instance, the following code is
    not forbidden:

        let flag = (match List.length [] with 0 -> true)

    even though constructions of this form are "prone to error,"
    and generate warning messages.

2.  The policy imposes a needless efficiency penalty on type
    abstraction.  For instance, suppose we have an abstract type

        type 'a t

    then we can't form the recursive type

        type x = x t

    without a boxing.  Although the type

        type x = X of x t

    is equivalent, it requires threading a lot of superfluous X's through
    the code, and ocaml will insert an extraneous boxing for each
    occurrence of an item of type x in t.  Consider an unlabeled
    abstract binary tree:

        type 'a t = ('a option) * ('a option)    (* abstract *)
        ...
        type node = X of node t

    Every node is boxed, with a space penalty that is
    linear in the number of nodes.

3.  If the type system can be bypassed with an extraneous boxing,

        type x = x t   ----->   type x = X of x t

    then what is the point?

4.  (Joke) All significant programs are "prone to error."  Perhaps the
    OCaml compiler should forbid them all!

    I use this construction extensively in Nuprl (theorem proving)
    and Ensemble (communications) applications; do I really need
    to change my code?

Jason

Re: recursive types

[Xavier Leroy]

Here is the straight dope (or my view of it, anyway) about recursive
types, or more precisely, the fact that all recursive type expressions
are no longer allowed in OCaml 1.06:

1- It is true that recursive (infinite) type expressions such as

        'a where 'a = 'a list (standing for the infinite type
         ... list list list list

can be added to the ML type system without causing major theoretical
difficulties.  In particular, unification and type inference work just
as well on recursive types (infinite terms) than on regular types
(finite terms).

2- "Classic" ML does not have recursive types, just finite terms as
type expressions.  Except some versions of Objective Caml, you won't
find any implementation of ML that accepts them.

3- The reason Objective Caml supports recursive types is that they are
absolutely needed by the object stuff.  More precisely, recursive
types naturally arise when doing type inference for objects (without
prior declarations of object types).  Hence, Objective Caml performs
type inference using full recursive types (cyclic terms) internally.

4- Still (and now comes the language design issue), one may decide to
impose extra restrictions on type expressions, such as "all cycles in
a type must go through an object type", thus prohibiting recursive
types that don't involve object types, such as ... list list list above.
In OCaml, we have experimented with several such restrictions.  I
think early releases (up to 1.04) had restrictions, though I don't
remember which; 1.05 had no restrictions at all, and was strongly
criticized for that (see below); 1.06 has the "all cycles must go
through an object type" restriction.

5- The main problem with unrestricted recursive types is that they
allow type inference to give nonsensical types to clearly wrong code,
instead of issuing a type error immediately.  For instance, consider
the function

        let f x y = if ... then x @ y else x

Assume I make a typo and type "@" instead of "::" :

        let f x y = if ... then x :: y else x

Any sane ML implementation reports a type error.  But OCaml 1.05 (the
one with unrestricted types) would accept the definition above, and
infer the deeply obscure type:

val f : ('a list as 'a) -> ('b list as 'b) list -> ('c list as 'c)

Calls to the function f will probably be ill-typed, so the error will
eventually be caught, but possibly very far from the actual error (the
definition of f).

Some users of OCaml 1.05 loudly complained that unrestricted recursive
types make the language much harder to use for beginners and
intermediate programmers.  We agreed that they had a strong point
here.  You don't want types such as the above for f.  Really.  Trust me.

So we and decided to go back to recursive types restricted to objects
only --- the reasoning being that this does not reject any "classic"
ML code (which type-checks without recursive types already), but still
lets the right types for objects being inferred.

6- Of course, we forgot that users would exploit the "unrestricted
recursive types" bug of OCaml 1.05, and come back at us claiming it's
a useful feature.  So, let's see how useful are recursive types that
are not objects.  I'm taking Jason Hickey's examples here.

>     type x = x option
> the type "x" should probably be isomorphic to the natural numbers

Such a type can be written more clearly as type x = Z | S of x
(or even better type x = int, but that's a different story).

> Consider an unlabeled abstract binary tree:
> 
>         type 'a t = ('a option) * ('a option)    (* abstract *)
>         ...
>         type node = X of node t

Again, I don't see the point of the 'a t type.  A much clearer way to
describe unlabeled binary trees is:

        type node = Empty | Node of node * node

Notice: no extra boxing here.

The point I'm trying to make here is that pretty much all the time, 
recursive types can be avoided ad clarity of the code can be improved
by using the right concrete types (sums or records) to hide the
recursion, rather than using generic sum or product types such as
"option" and "*", then obtain the desired recursive structure by using
recursive type expressions.

I know of only one or two cool examples where recursive type
expressions come in handy and avoid code duplication that the regular
ML type system forces you to do otherwise.

Now, in reply to Jason Hickey's points:

> 1.  The interpretation of the general recursive type has a
>     well-defined type theoretic meaning.

Yes, but this doesn't imply it's a desirable feature in a programming
language.

> Why not issue a warning rather than forbidding the construction?

That's one option, though issuing meaningful warnings is probably
harder than just rejecting the program.  Another option we discussed
is a command-line flag that changes the behavior of the type-checker
w.r.t. recursive types.

>    For instance, the following code is
>    not forbidden:
>        let flag = (match List.length [] with 0 -> true)
>    even though constructions of this form are "prone to error,"
>    and generate warning messages.

Right.  Some of us think all warnings should be errors, though.  In
this particular case, upward compatibility with the "classic ML" way
leads to accepting the program and just issue a warning.  For
recursive types, the same argument argues in favor of rejecting the
program.

> 2.  The policy imposes a needless efficiency penalty on type
>     abstraction.

Only if you don't hide the recursion inside the abstraction, and
insist on taking fixpoints outside the abstraction.  As I've shown
before, the penalty can almost always be avoided by writing your
concrete types in a "natural" style.  Anyway (warning--silly joke
ahead), since when type theorists are worried about efficiency? (end
of silly joke).

> 3.  If the type system can be bypassed with an extraneous boxing,
>         type x = x t   ----->   type x = X of x t
>     then what is the point?

The programmers write the "X" constructor explicitely in the program,
thus making their intentions clear.  It's completely different from an
inferred recursive type, which is more often than not an unintended
consequence of a coding error.

> 4.  (Joke) All significant programs are "prone to error."  Perhaps the
>     OCaml compiler should forbid them all!

This is an old Usenet-style argument.  Another (joke) conclusion is
that for the same reasons, we should turn off all type-checking and
error checking in the compiler.

>     I use this construction extensively in Nuprl (theorem proving)
>     and Ensemble (communications) applications; do I really need
>     to change my code?

We should have released 1.06 earlier; this would have left you less
time to exploit 1.05's bugs so thoroughly...  At any rate, I'd
certainly encourage you to think about the data structures you use,
and whether you couldn't rewrite them in a clearer way by getting rid
of recursive types and using Caml's concrete datatypes (sums and
records) instead.  Of course, if you come up with convincing real-life
examples (not just type-theoretic examples) of why recursive types are
useful, we'll reconsider.

- Xavier Leroy

Re: recursive types

[Jason Hickey]

Thanks for the well-presented argument.  One of the points you made is
that functions with inferred general recursive types are often
incorrect.  I agree, and I am willing to make sacrifices to tie down
type inference (although it seems a little extreme to remove the
offending constructions).

By that way, thanks for 1.06 release.  OCaml 1.05 has been solid and
reliable, and you have added many useful features to 1.06.  The language
and its type system have been clearly thought out.  Nice!

Xavier Leroy wrote:
> 
> Here is the straight dope...

-- 
Jason Hickey                    Email: jyh@cs.cornell.edu
Department of Computer Science  Tel: +1 (607) 255-4394
Cornell University

Re: recursive types

[Remi Vanicat]

"Jacques Le Normand" <rathereasy@gmail.com> writes:

> hello again list
> is it possible to have mutually recursive classes and types? I'm trying to
> implement the zipper, and this is what I came up with:

Not directly, but you can use polymorphism to have it:


class type ['a] node_wrapper =
object
  method identify : string
  method get_child_location : 'a
end

class virtual ['a] nodeable =
object(self)
  method virtual to_node_wrapper : 'a node_wrapper
end

type path = (location nodeable list * location * location nodeable list) option
and location = Loc of location nodeable * path

you could even do something like :


class type ['a] pre_node_wrapper =
object
  method identify : string
  method get_child_location : 'a
end

class virtual ['a] pre_nodeable =
object(self)
  method virtual to_node_wrapper : 'a pre_node_wrapper
end

type path = (location pre_nodeable list * location * location pre_nodeable list) option
and location = Loc of location pre_nodeable * path

class type node_wrapper = [location] pre_node_wrapper

class virtual nodeable = [location] pre_nodeable

(you could also make the type polymorphic, and the class
monomorphic if you declare the type before the class and class
type). 

You probably should come on the Beginner's list, where such question
could be answered (see http://groups.yahoo.com/group/ocaml_beginners)

--
Rémi Vanicat

recursive types

[Jacques Le Normand]

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

hello again list
is it possible to have mutually recursive classes and types? I'm trying to
implement the zipper, and this is what I came up with:

class type node_wrapper =
object
  method identify : string
  method get_child_location : location
end

class virtual nodeable =
object(self)
  method virtual to_node_wrapper : node_wrapper
end

type path = (nodeable list * location * nodeable list) option
and location = Loc of nodeable * path


which, of course, doesn't type check


a simpler test case would be

class a =
  val b : c
end

type c = a

thanks for all the help so far!
--Jacques

[-- Attachment #2: Type: text/html, Size: 723 bytes --]

Recursive types

[Swaroop Sridhar]

How are arbitrary recursive types implemented in caml? Is it done using 
an explicit fix point combinator "type" so that the unifier itself does 
not go into an infinite loop?

I apologize if this topic has been previously discussed, and I would 
really appreciate if somebody can point me at the relevant postings.

Thanks,
Swaroop.

recursive types

[nakata keiko]

Can I have recursive types going through both of "normal" types and
class types?

I would like to define something like

type exp = [`Num of obj |`Neg of obj] 
and class type obj = 
  object 
    method eql : exp ->  bool
  end

Thanks,
Keiko