6
$\begingroup$

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.

$\endgroup$
10
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – Anthony May 22 '11 at 18:47
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer May 23 '11 at 4:16
5
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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