Isoecursive Types When to Fold and Unfold I'm trying to implement recursive types into my programming language. I've implemented extensible rows and was hoping to add some recursive typing in order to get something like this or self within a record (thus imitating objects). Recursive types would only occur in record definitions, like

record IntObject:
  val: int
  add: (IntObject -&gt; IntObject)


Now IntObject is an alias for the type mu X. {val: int, add: (X -&gt; X)}.

This represents an IntObject with a field val that has the type of a primitive integer, and an add method that takes in an IntObject and returns another IntObject, so I can use it like so:

IntObject(1).add(IntObject(2))


The definition of add would be something like.

record IntObject:
  def add(self, other):
    return IntObject(self.val + other.val)


Like in Python, instance method invocations have a reference to the object calling the method implicitly passed in as the first parameter. I'm not sure how Python does this, but I was thinking of doing the partial application of the instance methods at object creation. Therefore,

IntObject(1)


creates a record like this (using Haskell lambda syntax)

{val: 1, add: \other -&gt; IntObject.add(self, other)}


I tried reading TAPL's section on recursive types, and isorecursion seems much easier to implement, especially since I will only allow records to have recursive types. What I'm unsure about is when to add folds and unfolds. TAPL says


  In Java each class definition implicitly introduces a recursive type, and invoking a method on an object involves an implicit unfold.


This is exactly what I want to do. If invoking a method introduces an unfold, that means that there needs to be a fold somewhere, and I'm unsure where to introduce that fold.

If this question is too vague, specifically since I probably haven't given enough information about the current state of my language, a general answer would suffice. Any advice regarding where to introduce folds and unfolds in an OOP language, say Java, would help a ton.
As you've stated, the type of IntObject is mu X. {val: int, add: (X -&gt; X)}. fold and unfold witness the isomorphism between a recursive type and its body, i.e. in this case between mu X. {val: int, add: (X -&gt; X)} and {val: int, add: ((mu X. {val: int, add: (X -&gt; X)) -&gt; (mu X. {val: int, add: (X -&gt; X)))}. Letting Y stand for mu X. {val: int, add: (X -&gt; X)}, this can be more compactly written unfold : Y ~= {val: int, add: (Y -&gt; Y)} with fold going the other direction.

You need unfold whenever you want to access any fields/methods. mu X. {val: int, add: (X -&gt; X)} doesn't have any fields; {val: int, add: (Y -&gt; Y)} does. Dually, whenever you want to make an IntObject, you need to use fold. A value of type {val: int, add: (Y -&gt; Y)} is not an IntObject, but fold can inject that value into the type IntObject. In particular, any time you new up an IntObject, i.e. invoke the constructor to create an object.

Basically, your IntObject(i) "really means" something like 

let self = fold({val: i, add: \other -&gt; IntObject.add(self, other)}) in self


Similarly, your add method would look like:

def add(self, other):
    return IntObject(unfold(self).val + unfold(other).val)


where we'd use the definition of IntObject just mentioned above.