patternModerate
In Agda's GADT, are "parameterized" and "indexed" different semantically?
Viewed 0 times
semanticallygadtareagdaindexeddifferentandparameterized
Problem
I know they have different scoping:
That's not what I'm caring about. Are they different semantically?
data a (n : Set) : Set where
introA : a n
data b : Set -> Set where
introB : {n : Set} -> b nThat's not what I'm caring about. Are they different semantically?
Solution
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:
-
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.
-
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 )).$$
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:
-
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.
-
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 )).$$
Context
StackExchange Computer Science Q#98529, answer score: 10
Revisions (0)
No revisions yet.