6
$\begingroup$

I've recently started independently learning type theory, using a combination of papers found online and ncatlab.org (but have not worked with category theory), and am about to start reading TAPL.

I'm interested in understanding how recursive types can be substituted for inductive types in dependent type theory (we assume dependent sums, dependent products, identity types and finite types 0, 1, 2 in our background theory), however I am unable to find a definition for recursive types that doesn't use unrestricted fixpoint operators and hence lack strong normalisation.

I've attempted to do this myself, but the dependent eliminator seems slightly too weak, and a restriction on if b then x else y such that the boolean expression is evaluated before x and y can be reduced seems to be required for normalisation.

$$\frac{A:\text{Type} \vdash F(A):\text{Type} \\ A\text{ is positive in }F(A)}{\mu A.F(A):\text{Type}}$$

$$\frac{a:F(\mu A.F(A))}{S(A):\mu A.F(A)}$$

$$\frac{B:\text{Type}, b:B \vdash C(b,B):\text{Type} \\ B:\text{Type}, e: \prod_{b:B}C(b,B))\vdash R(B,e) : \prod_{f:F(B)}C(f,F(B))}{rec(R):\prod_{a:\mu A.F(A)}C(a, \mu A.F(A))}$$

$$\frac{B:\text{Type}, b:B \vdash C(b,B):\text{Type} \quad a:\mu A.F(A)\\ B:\text{Type}, e: \prod_{b:B}C(b,B))\vdash R(B,e) : \prod_{f:F(B)}C(f,F(B))}{rec(R)S(a)=R(\mu A.F(A),rec(R))a:C(a, \mu A.F(A))}$$

Where A is positive in F(A) precisely when A does not occur in any type indexing any dependent product types in F(A).

Is my formulation correct? What is the correct way to formulate rules for normalising recursive types, and are there any references that I could look at that expand on these?

$\endgroup$
  • $\begingroup$ Ok, next thing in order to say is that you should not ask the same question twice. This is a duplicate of cstheory.stackexchange.com/questions/39592/… $\endgroup$ – Andrej Bauer Nov 22 '17 at 12:42
  • $\begingroup$ Deleted. However, I fail to see how this is a duplicate? There are formulations of (strictly positive) recursive types that are weakly normalising, so (with a reduction strategy) that doesn't seem to be a valid argument for why inductive types are generally preferred? $\endgroup$ – Emma Nov 22 '17 at 13:34
  • $\begingroup$ Could you please change the title of the question so that it refers to "(non-strictly) positive recursive types" or some such? $\endgroup$ – Andrej Bauer Nov 22 '17 at 14:32
8
$\begingroup$

Why are recursive types seldomly seen in dependent type theory?

The point of inductive types is precisely that you get normalization. Unrestricted recursive types simply lead to non-normalizing terms.

Given any type $A$, we may inhabit $A$ with a non-normalizing term as follows. Consider the recursive type $$D = D \to A.$$ The term $\omega \mathrel{{:}{=}} \lambda d : D . d \; d$ has type $D \to A$ and it also has type $D$, since they are equal. Therefore $\omega \; \omega$ has type $A$, and in addition $\omega \; \omega$ reduces to itself, giving a non-normalizing term.

If instead of $D = D \to A$ we have just $D \cong D \to A$ then an easy adaptation of the above argument leads to the same conclusion. You just have to coerce $d$ to have type $D \to A$.

Is this bad? If you're using type theory to write programs then it probably isn't that bad. It's actually kind of cool. But if you're using type theory to do reasoning, i.e., you want ot use types as propositions, then it's bad because every type has an inhabitant and so every propostion has a proof. It just depends on what you want from type theory.

What are the rules for recursive types?

$\newcommand{\Type}{\mathsf{Type}}$ Let us try to formulate the rules for recursive types. A reasonable attempt goes along the same lines as what you've suggested: $$\frac{\Gamma, X : \Type \vdash F(X) : \Type}{\Gamma\vdash \mu X . F(X) : \Type}$$ $$\frac{\Gamma \vdash e : F(\mu X . F(X))}{\Gamma \vdash S(e) : \mu X . F(X)}$$ $$\frac{\Gamma, y : \mu X . F(X) \vdash C(y) : \Type \qquad \Gamma, x : F(\mu X . F(X)) \vdash f(x) : C(S(x)) \quad \Gamma \vdash u : \mu X . F(X) }{\Gamma \vdash \mathsf{rec}_F([x . f(x)], u) : C(u)}$$ We shouldn't forget to ask about equations that we expect to hold. The $\beta$-rule would be $$\mathsf{rec}_F([x . f(x)], S(e)) = f(e)$$ and let us throw in an $\eta$-rule $$S(\mathsf{rec}_F([x . x], u)) = u.$$ The $\eta$-rule says that if we take apart $u : \mu X . F(X)$ and put it back together, we will get $u$. So far we have a map $S : F(\mu X . F(X)) \to \mu X . F(X)$, but we also want $R : \mu X . F(X) \to F(\mu X . F(X))$ together with $$S(R(u)) = u \qquad\text{and}\qquad R(S(e)) = e \tag{1}$$ These say that $S$ and $R$ form an isomorphism between $F(\mu X . F(X))$ and $\mu X . F(X)$. We can get such an $R$, namely $$R \mathbin{{:}{=}} \lambda y : F(\mu X . F(X)) . \mathsf{rec}_F([x . x], y).$$ Indeed, we have by the $\beta$-rule $$R(S(e)) = \mathsf{rec}_F([x . x], S(e)) = e$$ and by the $\eta$-rule $$S(R(u)) = S(\mathsf{rec}_F([x . x], u) = u.$$

We could have started with having $S$ and $R$ satisfying equations (1), and that would allow us to derive the eliminator as $$\mathsf{rec}_F ([x . f(x)], u) = f(R(u)).$$ Such an eliminator satisfies the $\beta$-rule and the $\eta$-rule, quite obviously. This should give us pause. We discovered that our rules say precisely that $\mu X . F(X)$ is isomorphic to $F(\mu X . F(X))$ and nothing else. This is not good, because the rules should fix the meaning of $\mu X . F(X)$ up to equivalence of types.

To see that the rules are no good, consider the case $F(X) = X$. Every type is a fixed point of $F$, and our rules say nothing about which one $\mu X . X$ should be. Indeed, we can take an arbitrary type $A$ and set $R$ and $S$ to be the identity maps. That will satisfy all the rules for $\mu X . X$.

We should somehow state which fixed point of $F$ we have in mind when we write down $\mu X . F(X)$. a reasonable choice would be to ask for the smallest or initial one. But what does that mean? In category theory it means that there is a unique homomorphism from the algebra $S : F(\mu X . F(X)) \to \mu X . F(X)$ to any other $F$-algebra. Here we rely on the fact that $F$ is a functor so that we can reasonably talk about $F$ applied to a map. But our $F$ is not going to be a functor in general because it might break covariance (try to extend $F(X) = X \to X$ so that it takes $f : A \to B$ to some $F(f) : F(A) \to F(B)$ and you will see what the problem is). We are stuck, as we have no good criterion for picking one of possible fixed points of $F$!

The way out is to decompose $F : \Type \to \Type$ according to covariant and contravariant arguments, $$F : \Type \times \Type^{\mathrm{op}} \to \Type.$$ For example $F(X) = X \to X$ becomes $F(X_1, X_2) = X_2 \to X_1$. But now it's not clear what a fixed point of $F$ might be. All this leads to Freyd's notion of algebraically compact categories and a beautiful theory surrounding them. The theory can be applied to categorical models of programming languages to explain how recursive types work there. When we throw in dependent types, then as far as I know, things break and nobody knows what to do. But I would love to be proved wrong!

The sort of recursive types we spoke about here goes under the name isorecursive types. The other option are equirecursive types, see the same link.

$\endgroup$
  • $\begingroup$ Thank you for your answer, however I'm interested in recursive types that are positive i.e. where $A$ does not occur on the left of any dependent product types, and these do not generally have this property. I've changed the question to clarify this. $\endgroup$ – Emma Nov 22 '17 at 13:24
  • $\begingroup$ Can you give an example of such a type constructor which is not an inductive type? $\endgroup$ – Andrej Bauer Nov 22 '17 at 14:31
  • $\begingroup$ Thank you for your answer. I lack the category theoretic background to understand most of what goes on when you introduce the category-theoretic notions, however, being unable to determine what the recursive type is using the constructors and eliminators, due to not being able to express the required isomorphisms is insightful to me, so thank you for your answer. $\endgroup$ – Emma Nov 22 '17 at 14:45
  • 1
    $\begingroup$ Inductive types are just a syntactic way of stating what it means to have strict positivity. Strict positivity is used for two purposes: (1) to make sure we know what it means to have an algebra, so that we can say that the inductive type is the initial algebra (although this is not how people in type theory talk, it is in essence what is going on), and (2) to have a not-too-complicated proof that such algebras exist. $\endgroup$ – Andrej Bauer Nov 22 '17 at 14:54
  • 1
    $\begingroup$ Your syntactic restriction seems similar to strict positivity, but not quite the same. For example, you could ask for a recursiv type given by $F(X) = \mathsf{nat} + \sum_{x : X} \mathsf{Id}_X(x,x)$. That would be weird. $\endgroup$ – Andrej Bauer Nov 22 '17 at 14:54
1
$\begingroup$

A pretty comprehensive reference is Peter Dybjer's Inductive Families paper that presents a very general class of inductive types (I've rarely seen them called "recursive types").

Note that positivity is subsumed by the condition: there exists a morphism

$$ \mathrm{map}:\Pi_{T\ U:\mathrm{Type}} (T\rightarrow U)\rightarrow F\ T\rightarrow F\ U$$

and it's reasonable to ask that every such family define an inductive family. I believe this is the view taken by Ralph Matthes in Monotone Fixed-Point Types And Strong Normalization.

$\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.