Recursive types

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.

Re: [Caml-list] Recursive types

[Jacques Garrigue]

From: Swaroop Sridhar <swaroop@cs.jhu.edu>

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

No, types are just implemented as (cyclic) graphs.
All functions in the type checker have to be careful about not going
into infinite loops. There are various techniques for that, either
keeping a list/set of visited nodes, or using some mutable fields.
A few years ago, infinite loops were a commonly reported bug :-)

Jacques Garrigue

Re: [Caml-list] Recursive types

[Keiko Nakata]

From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>

> From: Swaroop Sridhar <swaroop@cs.jhu.edu>
> 
> > How are arbitrary recursive types implemented in caml? 
> 
> No, types are just implemented as (cyclic) graphs.
> All functions in the type checker have to be careful about not going
> into infinite loops. There are various techniques for that, either
> keeping a list/set of visited nodes, or using some mutable fields.

I am very interested in this subject.
Since 1) I can define type abbreviations almost artitrary,
as in  type t = < m : t > ; and 2) type abbreviations can have parameters
as in type 'a t = < m : 'a > , 
just keeping a list/set of visited nodes does not seem to be enough,
especially for structual types.
So I think the type checker does some very clever thing.

Regards,
Keiko.

Re: [Caml-list] Recursive types

[Alain Frisch]

Keiko Nakata wrote:
> I am very interested in this subject.
> Since 1) I can define type abbreviations almost artitrary,
> as in  type t = < m : t > ; and 2) type abbreviations can have parameters
> as in type 'a t = < m : 'a > , 
> just keeping a list/set of visited nodes does not seem to be enough,
> especially for structual types.

Structural loops (those that don't cross a datatype) cannot be
arbitrary. The parameters cannot change:

# type 'a t = < m : 'a t >;;
type 'a t = < m : 'a t >
# type 'a t = < m : ('a * 'a) t>;;
In the definition of t, type ('a * 'a) t should be 'a t

The restriction ensures that structural recursive types are necessarily
regular. So standard coinductive algorithms (implemented by keeping
track of visited nodes or by memoization) are ok.

-- Alain

Re: [Caml-list] Recursive types

[Keiko Nakata]

From: Alain Frisch <Alain.Frisch@inria.fr>
> 
> The restriction ensures that structural recursive types are necessarily
> regular. So standard coinductive algorithms (implemented by keeping
> track of visited nodes or by memoization) are ok.

Thanks for the reply.

I think that it is not easy to know when to apply eta-expansion, 
namely, to replace a type name with its underlying definition.

For instance, to check equivalence betweeen the types t and s below:
 type t = < m : t * t >
 type 'a tuple = 'a * 'a
 type s = < m : s tuple >

the algorithm should memorize that t * t and s tuple are equivalent,
and then expands s tupl into s * s  
so as to check between t * t and s * s? 

When type abbreviations are more verobse as in 

 type 'a id = 'a 
 type 'a tuple = 'a id * 'a id 
 type u = < m : < m : u tuple> * < m : u tuple> > 

it seems difficult to know when to memorize in what representations
and when to eta-expand by the definitions.

I know easy standard coinductive algorithms found in textbooks,
but how to handle abbreviations is still unclear for me.

With best regards,
Keiko.

Re: [Caml-list] Recursive types

[Jacques Garrigue]

From: Keiko Nakata <keiko@kurims.kyoto-u.ac.jp>

> I think that it is not easy to know when to apply eta-expansion, 
> namely, to replace a type name with its underlying definition.
> 
> For instance, to check equivalence betweeen the types t and s below:
>  type t = < m : t * t >
>  type 'a tuple = 'a * 'a
>  type s = < m : s tuple >
> 
> the algorithm should memorize that t * t and s tuple are equivalent,
> and then expands s tupl into s * s  
> so as to check between t * t and s * s? 

No need to memorize equivalences: s tuple expands at its head to s * s.
The type checker guarantees that it is always safe to expand the head
of a type (i.e., definitions are well-founded.)
But you're right that abbreviations complicate the unification
algorithm a lot.
In order for unification to succeed above, t must expand to
(< m: 'a * 'a> as 'a), and s too. But to print nicely types we must
keep the abbreviations. This is done by memoizing expansions inside 
the abbreviations themselves. I.e., the expansion of t is actually:
  (< m : t[t='a] * t[t='a] > as 'a)
and that of s is
  (< m : s[s='b] tuple[s='b]> as 'b)
where [t='a] is an internal annotation to the abbreviation. So when
unifying, you can actually check the underlying type of an
abbreviation. But maintaining these abbreviations is rather
involved...
Fo instance abbreviations must be propagated:
  type u = <m : w> and w = u * u
will expand to
  (<m : w[u='a]> as 'a)
so that, if we expand w, we fall back to
  (<m : u[u='a] * u[u='a]>)

Jacques Garrigue

Re: [Caml-list] Recursive types

[Keiko Nakata]

From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>

> No need to memorize equivalences: s tuple expands at its head to s * s.
> The type checker guarantees that it is always safe to expand the head
> of a type (i.e., definitions are well-founded.)

Thanks for the reply.

> In order for unification to succeed above, t must expand to
> (< m: 'a * 'a> as 'a), and s too. But to print nicely types we must
> keep the abbreviations. This is done by memoizing expansions inside 
> the abbreviations themselves. 

This is a pretty nice feature of the type checker.
When programming with polymorphic variants,
the last part of typing error messages, 
which tells me incompatibilities of types using abbreviating names,
always helps me a lot.

With best regards,
Keiko 

Re: [Caml-list] Recursive types

[Swaroop Sridhar]

Jacques Garrigue wrote:
> No, types are just implemented as (cyclic) graphs.
> All functions in the type checker have to be careful about not going
> into infinite loops. There are various techniques for that, either
> keeping a list/set of visited nodes, or using some mutable fields.

Thanks for the clarification. In order to ensure that I understand you 
correctly, can you please look into the following unification algorithm 
and see if it is reasonably correct?

Considering a language with integers, records and type variables.
Let record types be unified by structural unification.

My representation of type is (please forgive my sloppy syntax at times):

type KindUnion = Integer | Tvar | Record
type 'a option = None | Some 'a

type TYPE =
  { id: int;
         (* unique ID *)

    kind: kindUnion;
         (* type of this type: integer/ tvar/ record *)

    components: mutable vector of TYPE
         (* vector of types containing legs of a record *)

    typeArgs: mutable vector of TYPE
         (* vector of types containing type-arguments / type-parameters
            of a record *)
         (* example
               type ('a, 'b) rec = { a: 'a->'b; b: int}
                     typeArgs          components
         *)

    link: mutable (TYPE option)
         (* to link unified types *)

    unf: mutable (TYPE option)
         (* This is a marker used by the unifier.
            Initially, this field is set to `None' for all types.
            If we are attempting to unify t1 and t2, the unifier
            will mark t1-> unf = Some t2, and t2-> unf = Some t1
            so that we detect them next time when we recurse *)
}

I also assume that a function repr is defined that will traverse the 
links so that (repr t) will provide the "final" type.

So, now the Unifier algorithm can be written as (in some hypothetical 
algorithmic language):

Unify (first:TYPE, second: TYPE)
    will return true on Unification false if not.

1. Start
2. let t1 = repr first
    let t2 = repr second

3.  (* The unifier will set unf field on the way in and will
        clear it on its way out. So, first test if we have a
        recursive case *)

    if(t1.unf != None and t2.unf != None)
        if(t1.unf == t2.unf)
	  return true
        endif
        if(t2.unf == t1.unf)
           return true
        else
           return false
        endif
    endif


4. (* set the unf fields *)
    if(t1.unf == None and t2.unf != None)
        t1.unf := Some t2
    else
      if(t2.unf == None and t1.unf != None)
        t2.unf := Some t1
      else
        t1.unf = Some t2
        t2.unf = Some t1
      endif
    endif

5. match (t1.kind, t2.kind) with

    case (Integer, Integer) ->
            return true

    case (Tvar, _ )  ->
            t1->link = Some t2
            return true

    case (_, Tvar) ->
            t2->link = Some t1
            return true

    case (Record, Record) ->
            if the record lengths don't match
               return false

            for each i in 0 to t1.components.size()
               Unify (t1.components[i], t2.components[i])
               if Unification fails, return false

            for each i in 0 to t1.typeArgs.size()
               Unify (t1.typeArgs[i], t2.typeArgs[i])
               if Unification fails, return false
	   return true

    case (_, _)  ->
            return false

6. t1.unf = None
    t2.unf= None

7. Stop

Is this algorithm correct? If not, how should it be fixed?

> A few years ago, infinite loops were a commonly reported bug :-)

I read a couple of postings about this issue. I understand that one can 
hurt oneself with a type being parameterized itself. I also read that 
the type system needs to deal with this in order to support objects. 
Aren't recursive types necessary even to do a simple linked list like:

type llist = {contents: int; link : mutable llist}

Thanks again,
Swaroop.

Re: [Caml-list] Recursive types

[Jacques Garrigue]

From: Swaroop Sridhar <swaroop.sridhar@gmail.com>

> Thanks for the clarification. In order to ensure that I understand you 
> correctly, can you please look into the following unification algorithm 
> and see if it is reasonably correct?

There is a problem with your algorithm:
the way you check the unf field is buggy (you dereference both sides),
but this seems a trivial a trivial error.
More importantly, even corrected it will fail when unifying a loop of
length 3 with a loop of length 2:
   t1 = (int * (int * 'a) as 'a)
   t2 = (int * (int * (int * 'b)) as 'b)
when you reach the inner 'b, you have already unrolled t1, so it also
has its unf field set, but not to t2...

The approach in ocaml is simpler: link at each type node, so that
already unified types will look equal. As a result, after unification
you have only a loop of length 1.

> > A few years ago, infinite loops were a commonly reported bug :-)
> 
> I read a couple of postings about this issue. I understand that one can 
> hurt oneself with a type being parameterized itself. I also read that 
> the type system needs to deal with this in order to support objects. 
> Aren't recursive types necessary even to do a simple linked list like:
> 
> type llist = {contents: int; link : mutable llist}

Note in this case: the definition of llist is nominal, so this type is
only iso-recursive, which is much easier to handle.
The difficulties only appears with
  type llist = < contents: int; link : llist >

Jacques Garrigue

Re: [Caml-list] Recursive types

[Swaroop Sridhar]

Jacques Garrigue wrote:
> There is a problem with your algorithm ... 
> The approach in ocaml is simpler: link at each type node, so that
> already unified types will look equal. 

Let me have another take at the algorithm :

Unify (first:TYPE, second: TYPE)
    will return true on Unification false if not.

1. Start
2. let t1 = repr first
    let t2 = repr second

3. match (t1.kind, t2.kind) with

    case (Integer, Integer) ->
            return true

    case (Tvar, _ )  ->
            t1.link = Some t2
            return true

    case (_, Tvar) ->
            t2.link = Some t1
            return true

    case (Record, Record) ->

            if the record lengths don't match
               return false

  	   t1.link = t2  (***** linked speculatively *****)

            for each i in 0 to t1.components.size()
               Unify (t1.components[i], t2.components[i])
               if Unification fails,
			t1.link = None
			unlink all types that were linked until now
			return false
	      endif

            for each i in 0 to t1.typeArgs.size()
               Unify (t1.typeArgs[i], t2.typeArgs[i])
               if Unification fails,
			unlink all types that were linked until now
			return false
	      endif

        return true

    case (_, _)  ->
            return false

4. Stop

Is this correct/ similar to what Ocaml does?

> Note in this case: the definition of llist is nominal, so this type is
> only iso-recursive, which is much easier to handle.

We might have syntactic restrictions (ex: one of ML's restriction that 
recursion can occur only across variant constructor boundaries, etc) so 
that arbitrary recursion is disallowed. However, from an implementation 
standpoint, I *think* that the above implementation of the unifier is 
easier to do even in the case of iso-recursive types. Is this true?

I thought of introducing explicit fold/unfold operations into the 
algorithm, but it seemed to do more work. If I am wrong, can you please 
suggest modifications to the above algorithm that works (better) only 
for iso-recursive types.

Thanks,
Swaroop.

Re: [Caml-list] Recursive types

[Swaroop Sridhar]

A (small) correction, I forgot to write the base case that will allow 
for termination:

> 
> Unify (first:TYPE, second: TYPE)
>    will return true on Unification false if not.
> 
> 1. Start
> 2. let t1 = repr first
>    let t2 = repr second

   2.5  if t1 equals t2
	   return true
> 
> 3. match (t1.kind, t2.kind) with
> 
>    case (Integer, Integer) ->
>            return true
> 
>    case (Tvar, _ )  ->
>            t1.link = Some t2
>            return true
> 
>    case (_, Tvar) ->
>            t2.link = Some t1
>            return true
> 
>    case (Record, Record) ->
> 
>            if the record lengths don't match
>               return false
> 
>         t1.link = t2  (***** linked speculatively *****)
> 
>            for each i in 0 to t1.components.size()
>               Unify (t1.components[i], t2.components[i])
>               if Unification fails,
>             t1.link = None
>             unlink all types that were linked until now
>             return false
>           endif
> 
>            for each i in 0 to t1.typeArgs.size()
>               Unify (t1.typeArgs[i], t2.typeArgs[i])
>               if Unification fails,
>             unlink all types that were linked until now
>             return false
>           endif
> 
>        return true
> 
>    case (_, _)  ->
>            return false
> 
> 4. Stop

Swaroop.

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

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

[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 

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