It turns out this can be implemented more elegantly in Ocaml (or "tagless-ly"), since Ocaml supports -rectypes command line option, which allow us to define types like type t=t->t. However, this is not enabled by default. Let me know if there's way to enable this...

Added, thanks!

I'm thinking about using type families to mimic the fold/unfold of recursive types, with some type functions making the projection automatic (like in DTALC). Not sure if it will work, but I'll try it out when I got some time.

Hi Johan, Thanks for the valuable feedback and suggestions for improvement! The idea actually comes from TaPL, which you may preveiw here, starting at page p. 260. Pierce noted that recursive types can encode the whole untyped lambda calculus, which inspires me with the idea that "haskell is the most untyped typed language". Here D is chosen probably to mean "domain" (as in footnotes it says that "D's definition is precisely the universal domains used in semantic models of the pure lambda calculus").

What is also worth noting here is that Haskell can't directly encode recursive types without type tags (say the type "\m.int->m", which denotes a term that can accept infinite many integer parameters), and that's why we do a lot of wrappings and unwrappings. In fact, in Pierce representation, there are not type tags and app and lam are both of type D. Also, the use of explicit type tags here actually makes the problem looks easier, probably too easier--as there is only one way to write down the code. But in the original presentation with all terms being of type D, it's very surprising to see what we can do with recursive types. It would thus be interesting to see if we can get rid of the type tags and come up with a way to encode "tagless recursive types", maybe using universal types?

Finally, your suggestions all make sense to me, and I'll update the problem soon. By the way, since I'm new here, what does a fork mean? Is it something like git's fork-commit-pull-request pipeline, or it just shows a variant of the solution?

ahh yes! At first I was thinking about abstraction in my mind but later found it conflicts with standard libraries and so rename it to lam, which stands for lambda. I'll update the description soon!

Do you mean the N in the definition of D? Since D is only a partial definition in the initial code (line 8), I commented it out. But bascailly it's just a primitive type added to our UTLC. In particular, N is Peano numbers, which is useful here because we can't directly inspect the concrete UTLC terms (consider for example, how do we know \f x-> x corresponds to 0 and output it if we don't even have 0 in the DSL). If you feel such explanation is necessary, I will update the initial code fragment to clarify this.