With equirecursive types are there downsides to making all types potentially recursive?

Question

By this I mean to ask, is it a bad idea to have all type constructor term expressions abstracted with $\mu$ just in case they need to be recursive? For example,

$Bool : Type;$

$Bool = (\mu Bool' . (Unit \lor Unit));$

The value constructors would still just be $(inj_0 unit)$ and $(inj_1 unit)$ in a system with equirecursive types, right? It seems like it would just be $O(x + 1)$ for an $O(x)$ type checking algorithm using unification, or maybe not even that.

I understand why $Bool$ is not written this way by default, especially considering recursive types are usually added to a theory after-the-fact and therefore the value constructors would differ depending on the variant of the recursive type theory. It's much less intuitive to read $(\mu X . \tau)$ than just $\tau$ when programming or proving theorems but are there any reasons of real consequence for not doing this? I can't find any.

The reason I ask this question is because I am writing a program to translate a functional programming language into a core dependent type theory with equirecursive types.

Answer 1

My advice would be to make sure that your translation function is compositional and straightforward, i.e., for a typical construct $A * B$ the translation function $t$ should have the form $t(A * B) = s(t(A), t(B))$, where $s$ is the translation of $*$. Thus the translation should follow the syntax of the input language. If you want to perform any "optimizations", those should come as convinient tactics that get used after the translation phase. This will make it easier to pove that your translation works correctly.

Concretely, if your input language has a construct for defining recursive types, such as data in Haskell, then you should translate those to $\mu \cdots$ even if they are not actually using the recursion, because that is what they are. You can always have a simple lemma afterwards which shows that $\mu$ can be omitted in certain cases. If you set up your tactics the right way, the theorem prover will simplify things by itself (and do much more if needed). But you should not put $\mu$ in front of a definition that cannot be recursive, such as newtype. In other languages, for example in Ocaml, the only way to introduce a new type is with type, which may be recursive, so there you'd put $\mu$ in front of everything.

Answer 2

You can put the fixed point operator in front of whatever you want if you don't use the formal parameter (just like you can add and remove for alls and exists arbitrarily in logic if their formal parameter isn't used).

There is (in my opinion, not knowing your application that well) no advantage or disadvantage to always including a dummy fixed point in a system with equirecursive types. The theory doesn't change, and in practice nothing changes either because you can syntactically check if the formal parameter is used, and if not, special case the logic to be faster/use less memory/whatever.

edit: I had a bit of trouble understanding this question. If you want to know if you should restrict the syntax of types to always have a fixed point, I think you should not: types with forced irrelevant fixed points are unnecessarily ugly/complicated/nonstandard for no good reason.