Mutually Recursive Classes

Mutually recursive classes

1. Forward-declare the classes (you could get away with forward-declaring only one of them, but for good form do both).
   
2. Forward-declare the methods (ditto).
   

class Class1;
class Class2;

class Class1
{
  Class2* Class2_ptr;
public:
  void Class1_method();
};

class Class2
{
  Class1* Class1_ptr;
public:
  void Class2_method();
};

void Class1::Class1_method()
{
  //...
  (*Class2_ptr).Class2_method();
  //...
}

void Class2::Class2_method()
{
  //...
  (*Class1_ptr).Class1_method();
  //...
}

How to define mutually recursive types

Mutually recursive definitions must be separated by and. This goes for both let definitions and type definitions:

type cellInfo('a) = {
  index: int,
  column: column('a),
  id: string
}

and cellInfoFn('a) = cellInfo('a) => ReasonReact.reactElement

and column('a) = {
  header: string,
  accessor: accessor('a),
  id: option(string),
  cell: cellInfoFn('a),
};

Mutual recursion between objects in Python

So, I think the issue here is that names and objects are being conflated. I would maybe use a structure where the task objects are organized in a dictionary and a string or an enumeration are used as keys. This way you can refer to names before they are assigned.

class TaskManager:
    def __init__(self, tasks=None):
        self.tasks = tasks or {}

    def register(self, name, task):
        self.tasks[name] = task

    def execute(self, name):
        self.tasks[name].effect()

mutually dependent local classes (or mutually recursive lambdas)

Since the answer seems to be: "it is not possible to have clean mutually dependent local classes", it turns out that the workaround I like the most is to move the logic outside the structs themselves. As suggested by remyabel in the comments of the question, it can be done by creating a third class, but my favorite approach is to create mutually recursive lambda functions, since it makes possible to capture variables (hence makes my life easier in my real case usage). So it looks like:

#include <functional>
#include <iostream>

int main()
{
    struct B;
    struct A { B * b; };
    struct B { A * a; };

    std::function< void(A *) > foo;
    std::function< void(B *) > bar;

    foo = [&] (A * a) 
    {
        std::cout << "calling foo" << std::endl;
        if(a->b) { bar(a->b); }
    };
    bar = [&] (B * b)
    {
        std::cout << "calling bar" << std::endl;
        if(b->a) { foo(b->a); }
    };

    A a = {0};
    B b = {&a};
    foo(&a);
    bar(&b);

    return 0;
}

That compiles and prints:

calling foo
calling bar
calling foo

Note that the type of the lambdas must be manually specified because type inference doesn't work well with recursive lambdas.

prove decreases clause of mutually recursive class functions

Defining mutable linked heap-allocated data structures in Dafny is not very common except as an exercise. So you should consider whether a datatype would serve you better, as in

datatype RoseTree = Node(children: seq<RoseTree>)

function height(r: RoseTree): int
{
  if r.children == [] then
    1
  else
    var c := set i | 0 <= i < |r.children| :: height(r.children[i]);
    assert height(r.children[0]) in c;
    assert c != {};
    SetMax(c) + 1
}

If you insist on mutable linked heap-allocated data structures, then there is a standard idiom for doing that. Please read sections 0 and 1 of these lecture notes and check out the modern version of the example code here.

Applying this idiom to your code, we get the following.

class RoseTree {
    var NodeType: int
    var id: string
    var children: array<RoseTree>
    ghost var repr: set<object>

    predicate Valid()
      reads this, repr
      decreases repr
    {
      && this in repr
      && children in repr
      && (forall i | 0 <= i < children.Length :: 
            children[i] in repr 
          && children[i].repr <= repr 
          && this !in children[i].repr 
          && children[i].Valid())
    }

    constructor(nt: int, id: string, children: array<RoseTree>) 
      requires forall i | 0 <= i < children.Length :: children[i].Valid()
      ensures Valid()
    {
        this.NodeType := nt;
        this.id := id;
        this.children := children;
        this.repr := {this, children} + 
          (set i | 0 <= i < children.Length :: children[i]) +
          (set x, i | 0 <= i < children.Length && x in children[i].repr :: x);
    }
}

function SetMax(s: set<int>): int 
  requires s != {}
  ensures forall x | x in s :: SetMax(s) >= x
{
  var x :| x in s;
  if s == {x} then
    x
  else
    var y := SetMax(s - {x});
    assert forall z | z in s :: z == x || (z in (s - {x}) && y >= z);
    if x > y then x else y
}

function height(node: RoseTree): nat
  requires node.Valid()
  reads node.repr
{
  if node.children.Length == 0 then 
    1 
  else 
    var c := set i | 0 <= i < node.children.Length :: height(node.children[i]);
    assert height(node.children[0]) in c;
    assert c != {};
    SetMax(c) + 1
}

---

do all instances of a class have the constructor ensure statements applied implicitly or only if explicitly constructed using the constructor?

I'm not sure if I understand this question. I think the answer is "no", though. Since a class might have multiple constructors with different postconditions.

Understanding the Mutual Recursion Issue for the Return Type of Functions

As far as function definitions go, all you need is an appropriate forward declaration:

class A;
class B;

class A
{
    B foo();
};

class B
{
    A bar();
};

This will compile with no issues. Feel free to chop this up into two separate header files, with an appropriate forward declaration instead of an #include.

Note that the reason you can't declare class members the same way is because this will effectively have a class contain itself. Unfortunately, if that was possible, the end result would be a massive black hole that will swallow all life as we know it, and we certainly don't want that to happen...

Anyway, the other point that you need to keep in mind is you are affected here by your Java background. Classes work fundamentally different in C++ than they do in Java, despite the deceivingly similar syntax. You're better off forgetting everything you know about how classes work in Java. Otherwise you'll keep getting off track, like that. In Java, a similar set of declarations does not result in a class effectively containing itself, but in C++ it does. This is because in Java every class instance is really a pointer to a class, but in C++ it is the class itself, in flesh and blood.

In C++, the real equivalent to this kind of a recursive class declaration would be:

class A
{
    std::shared_ptr<B> b;
};

class B
{
    std::shared_ptr<B> A;
};

(ignoring for the moment the requisite forward declarations that apply here, too).

And this'll work in C++ equally well as it works in Java (the std::shared_ptr<> part is the equivalent of Java's object reference counting, sort-of). This is what's equivalent to your similar construct in Java.

how to define mutually-recursive class and exception in ocaml

Here's a brainstorming suggestion. Since OCaml uses structural typing for classes, you can declare the class as a type before defining the exception. Here's a sketch that works for me:

class type c = object method m : unit end

exception E of c * c

class myclass =
    object (self)
    method m : unit = raise (E ((self :> c), (self :> c)))
    end

Granted this is a bit cumbersome.

how to solve the recursion problem when specifying type hints for classes from different files

You need to use two techniques that are specific to type hinting in python, 1) forward references, and 2) importing types within a TYPE_CHECKING guard (check e.g. this post for a longer explanation of its implications). The first one allows you to reference a type that is not know to the interpreter at runtime, and the latter resolves types in a "type checking context".

Long story short:

models1.py

from dataclasses import dataclass
from typing import TYPE_CHECKING

if TYPE_CHECKING:
    from models2 import Second

@dataclass
class First:
    attribute: "Second"

models2.py

from dataclasses import dataclass
from typing import TYPE_CHECKING

if TYPE_CHECKING:
    from models1 import First

@dataclass
class Second:
    attribute: "First"

Executing the files with python3.8 or higher should work without any issues^[1], and can work in python3.7 as well with a __futures__ import. Running mypy on the files should work without any issues, too:

$ mypy models1.py models2.py
Success: no issues found in 2 source files 

---

^{[1] _{As comments have pointed out, creating actual instances of your First/Second classes that would also pass a type check is impossible, but I assume that this is a toy example and your real code has, for example, one of the attribues as Optional.}}

---

Related Topics