<p>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). </p>

<p>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.</p>

<p><strong>edit</strong>: 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. </p>

CC BY-SA 3.0
2011-05-22T04:09:37.807Z
2011-05-22T04:16:19.137Z
2011-05-22T04:16:19.137Z
Christopher Monsanto
<p>My advice would be to make sure that your translation function is  <em>compositional</em> and <em>straightforward</em>, 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 <em>after</em> the translation phase. This will make it easier to pove that your translation works correctly.</p>

<p>Concretely, if your input language has a construct for defining recursive types, such as <code>data</code> 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 <code>newtype</code>. In other languages, for example in Ocaml, the only way to introduce a new type is with <code>type</code>, which may be recursive, so there you'd put $\mu$ in front of everything.</p>

CC BY-SA 3.0
2011-05-22T18:47:21.587Z
Thank you for both points. Regarding your first paragraph, I actually just realised that last night as I was falling asleep. And as a follow up (maybe I should post seperately), do you know of formalisms for defining transformation from one formal language to another? I know automata such as Moore or Meeley machines can be used to do this, but what about something more declarative? Most term rewriting systems I've looked at seem to provide an image (inverse) of what I'm looking for.

Regarding your second paragraph, perfect, that's exactly what I was thinking.
Anthony
CC BY-SA 3.0
2011-05-23T04:16:18.263Z
Are you using an actual tool, such as Coq or Agda, or is this "theory"? If you are using a tool, I would expect the translation to be a simple primitive recursion on the syntax of the input language. That is, if you view the input and output syntax as two inductive types, your translation becomes a map from one to the other. I am not sure you want to fiddle with automata in a theorem prover that already has powerful induction mechanisms.
Andrej Bauer
CC BY-SA 3.0
2011-05-22T07:09:54.990Z
2011-05-22T07:09:54.990Z
Andrej Bauer
<p>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,</p>

<p>$Bool : Type;$</p>

<p>$Bool = (\mu Bool&#39; . (Unit \lor Unit));$</p>

<p>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.</p>

<p>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.</p>

<p>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.</p>

<type-theory><functional-programming><type-inference>
With equirecursive types are there downsides to making all types potentially recursive?
Anthony
# With equirecursive types are there downsides to making all types potentially recursive?

(Asked by: username_0 on 2011-05-21)

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.

**Tags:** type-theory, functional-programming, type-inference

---

## 2 answers

### Answer by username_2 on 2011-05-22. Score: 10 | Accepted answer

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.

> **Comments:**
> **username_0**: Thank you for both points. Regarding your first paragraph, I actually just realised that last night as I was falling asleep. And as a follow up (maybe I should post seperately), do you know of formalisms for defining transformation from one formal language to another? I know automata such as Moore or Meeley machines can be used to do this, but what about something more declarative? Most term rewriting systems I've looked at seem to provide an image (inverse) of what I'm looking for.  Regarding your second paragraph, perfect, that's exactly what I was thinking.  
> **username_2**: Are you using an actual tool, such as Coq or Agda, or is this "theory"? If you are using a tool, I would expect the translation to be a simple primitive recursion on the syntax of the input language. That is, if you view the input and output syntax as two inductive types, your translation becomes a map from one to the other. I am not sure you want to fiddle with automata in a theorem prover that already has powerful induction mechanisms.  

---

### Answer by username_1 on 2011-05-22. Score: 5

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.


---

