# In Agda's GADT, is “parameterized” and “indexed” different semantically?

I know they have difference in scoping:

data a (n : Set) : Set where
introA : a n

data b : Set -> Set where
introB : {n : Set} -> b n


That's not what I'm caring about. Are they different semantically?

Yes and no.

The obvious difference is that indexed types are able to vary in the result type of each constructor. So you can do:

data T : ℕ → Set where
t : T 5


You can do this with a parameterized type by taking an argument:

data T (n : ℕ) : Set where
t : n ≡ 5 → T n


But ≡ is itself an indexed type, so you need something indexed at the bottom (≡ can be seen as the fundamental indexed type, though, if you want).

In older versions of Agda, there was another difference, where parameterized types could be smaller than indexed types on some occasions. For instance, your type b would be illegal, and would have to be:

data b : Set → Set1 where
introB : {n : Set} → b n


This is because in general data types that contain values of Set must be large to avoid paradox. However, Agda now has a fairly sophisticated analysis that can tell that the value of the contained n is determined by the visible result type of the constructor, and so is 'safe'/equivalent to a parameterized type. So it allows it to be small, and this is no longer a difference between indexed and parameterized types.

So, up to this analysis possibly failing (which it probably can, but I don't know how to trick it), indexed types are more general, I believe.

The following explanation lacks mathematicial precision but should explain what is going on.

A GADT is a special case of a recursive type. A recursive type $$T$$ is a solution of a type equation of the form $$T = \Phi(T).$$ (If this is not clear, please ask.) Sometimes $$\Phi$$ depends on a parameter $$p : P$$ of some given type $$P$$, so we have a parameterized equation $$T = \Phi(p, T).$$ Now the solution $$T$$ is not just a type, because it depends on $$p$$, so we get a dependent type $$T : P \to \mathsf{Type}$$ such that $$T(p) = \Phi(p, T(p))$$ for all $$p : P$$.

We may also consider recursive equations in collections other than $$\mathsf{Type}$$. For example, an equation in $$\mathsf{Type} \times \mathsf{Type}$$ is a mutual recursive type $$(T_1, T_2) = \Phi(T_1, T_2).$$ The types $$T_1$$ and $$T_2$$ can be arbitrarily entangled, i.e., there is no guarantee that we can separate the equation into two equations $$T_1 = \Phi_1(T_1)$$ and $$T_2 = \Phi_2(T_2)$$. If we could separate like that, we would be back to the previous case of a parameterized fixed-point equation (the parameters ranging over $$\{1, 2\}$$).

We could similarly solve simultaneously for three, four, etc. types. In general, given any type $$I$$, we can solve an equation which is simultaneous in $$I$$-many types $$T_i$$, one for each index $$i : I$$, which gives us an indexed equation $$(T_i)_{i : I} = \Phi((T_i)_{i : I}).$$ The above notation is a bit ugly and it would be better to write $$T = \Phi(T)$$ where it is understood that the uknown $$T$$ is a dependent type $$T : I \to \mathsf{Type}$$ indexed by $$I$$. Again, there is no guarantee that we can disentangle the equation into $$I$$-many separate equations of the form $$T_i = \Phi_i(T_i)$$.

The two kinds of equations translate back to recursive and inductive type definitions. Let us write $$\mathsf{rec}_U\,\Phi$$ for the solution of a fixed-point equation $$X = \Phi(X)$$, where $$X : U$$ and $$\Phi : U \to U$$. We now have:

1. Given a map $$\Phi : A \to \mathsf{Type} \to \mathsf{Type}$$, the type family $$R : A \to \mathsf{Type}$$ given by $$R = \lambda a : A \,.\, \mathsf{rec}_{\mathsf{Type}}\,(\lambda X : \mathsf{Type} \,.\, \Phi(a, X))$$ is a recursive type with a parameter $$a : A$$, as in the first case.

2. Given a map $$\Psi : (A \to \mathsf{Type}) \to (A \to \mathsf{Type})$$, the type family $$Q : A \to \mathsf{Type}$$ given by $$Q = \mathsf{rec}_{A \to \mathsf{Type}}\,(\lambda F : A \to \mathsf{Type} \,.\, \Psi(F))$$ is a recursive type with index $$a : A$$, as in the second case.

It should be clear that $$R$$ and $$Q$$ are not the same thing. In $$R$$ we solve one fixed-point equation in $$\mathsf{Type}$$ for each parameter $$a : A$$, whereas in $$Q$$ we solve a single fixed-point equation in $$A \to \mathsf{Type}$$. As a sanity check you should try to translate your examples to the above notation.

Lastly, the indexed recursive types are more general than the parametrized ones. Indeed, $$R = \lambda a : A \,.\, \mathsf{rec}_{\mathsf{Type}}\,(\lambda X : \mathsf{Type} \,.\, \Phi(a, X))$$ can be written as $$R = \mathsf{rec}_{A \to \mathsf{Type}}\,(\lambda F : A \to \mathsf{Type} \,.\, \lambda a : A \,.\, \Phi(a, F(a))).$$ In the other direction, an indexed recursive type $$Q$$ as above may be converted to a parameterized one precisely when $$\Psi$$ can be separated, which means that it has the form $$\Psi(F) = \lambda a : A \,.\, \Psi'(a, F(a))$$ for some $$\Psi' : A \times \mathsf{Type} \to \mathsf{Type}$$, in which case we have $$Q = \lambda a : A \,.\, \mathsf{rec}_{\mathsf{Type}} (\lambda X \,.\ \Psi'(a, X )).$$