# 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


Now IntObject is an alias for the type mu X. {val: int, add: (X -> 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:
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 -> 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 -> 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 -> X)} and {val: int, add: ((mu X. {val: int, add: (X -> X)) -> (mu X. {val: int, add: (X -> X)))}. Letting Y stand for mu X. {val: int, add: (X -> X)}, this can be more compactly written unfold : Y ~= {val: int, add: (Y -> Y)} with fold going the other direction.

You need unfold whenever you want to access any fields/methods. mu X. {val: int, add: (X -> X)} doesn't have any fields; {val: int, add: (Y -> Y)} does. Dually, whenever you want to make an IntObject, you need to use fold. A value of type {val: int, add: (Y -> 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 -> 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.

• Thank you for taking the time to answer this question. I'm a bit confused how this works in other cases though. If I have a function let f = \x -> x.add, my type system infers the type {add: A | B} -> A, aka any record that has an add field, and potentially any other fields, and it returns the type of that add field. I'm unsure how this would work with IntObject. f(IntObject(1)) requires an unfold but f({add: 1}) does not. – Enrico Borba Apr 8 at 14:36
• f(IntObject(1)) is a type error. Presumably your point is that you don't want your users to have to (or be able to) insert these fold and unfold calls. The simplest solution is to just not have (naked) record types in the surface language. This would amount to having fold be incorporated into record construction and unfold in field access. This may cause issues with record extension. Another solution is to try to insert fold and unfold as needed. This basically amounts to a form of subtyping with all the issues that entails, but less so if you plan to have subtyping anyway. – Derek Elkins Apr 8 at 15:07
• I was hoping to try to avoid subtyping, and I do not allow for record extensions. I'm okay with having fold incorporated into record construction. I guess all records would then have the type mu X. {...}, where some records don't use X at all in their body. I think this makes sense. I'm still unsure how I would handle nested unfold calls, but I think I can figure it out. Thank you for your help! – Enrico Borba Apr 8 at 15:10