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 -> IntObject)

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:


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,


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.


1 Answer 1


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.

  • $\begingroup$ 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. $\endgroup$ Apr 8, 2019 at 14:36
  • $\begingroup$ 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. $\endgroup$ Apr 8, 2019 at 15:07
  • $\begingroup$ 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! $\endgroup$ Apr 8, 2019 at 15:10
  • $\begingroup$ Depending on your type system it may not be too hard to introduce a limited form of subtyping to automatically unfold types (most likely recursing covariantly inside records) at applications. I think you'll need to restrict these implicit unfolds to annotated types though, otherwise small program transformations could affect the result. $\endgroup$
    – max
    Sep 17, 2021 at 11:27
  • $\begingroup$ You could do some special casing in your type inference algorithm. For example if something expects a mu-type and it gets something that is obviously not a mu-type (like a record), then it should fold. If it expects a record type, but it gets a mu-type, then unfold. This is easier to do in a bidirectional typechecking algorithm. This does not work for all cases, but it could be practical enough to avoid subtyping. $\endgroup$
    – Labbekak
    Jan 26, 2022 at 8:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.