Dependently typed languages such as Agda support inductive families, also called indexed datatypes, which allow type parameters to vary between constructors. This can be used to define a set of relations between types, which can be used to constrain existentially. For example, we can capture the relation
$$\begin{align*} \mathsf{Unit} &\longmapsto \mathsf{Bool}\\ \mathsf{Nat} &\longmapsto \mathsf{Int} \end{align*}$$
in the following Agda type:
data Link: Set → Set → Set where
link-a: Link ⊤ Bool
link-b: Link ℕ ℤ
We can then define a type Tie
that pairs a value of type Link A B
with a function A → B
:
data Tie (L: Set → Set → Set): Set₁ where
tie: ∀ {A B} → L A B → (A → B) → Tie L
Just for further illustration, here are a few examples of working with these types:
tie₁ : Tie Link
tie₁ = tie link-a λ tt → true
tie₂ : Tie Link
tie₂ = tie link-b λ n → + n
app-tie : Tie Link → ℕ → Bool ⊎ ℤ
app-tie (tie link-a f) _ = inj₁ (f tt)
app-tie (tie link-b f) n = inj₂ (f n)
This is a useful technique, and this pattern is common in languages like Haskell (where inductive families correspond to GADTs). However, in Agda, the construction is somewhat awkward, as Tie
belongs to Set₁
rather than Set
due to the need to existentially embed A B : Set
in the tie
constructor.
I find this unsatisfying, as a simple rearranging of our types allows a definition of Tie
that belongs to Set
. Instead of defining Link
as an inductive family, we define it as a combination of an index and a type-returning function:
data LinkI : Set where
link-a′ : LinkI
link-b′ : LinkI
Link′ : LinkI → Set × Set
Link′ link-a′ = ⊤ ,′ Bool
Link′ link-b′ = ℕ ,′ ℤ
Now we can define a version of Tie
that contains no types and therefore belongs to Set
:
data Tie′ {I : Set} (L : I → Set × Set) : Set where
tie′ : (i : I) → uncurry′ Morphism (L i) → Tie′ L
At first blush, we seem to be able to do all the same things with this formulation:
tie′₁ : Tie′ Link′
tie′₁ = tie′ link-a′ λ tt → true
tie′₂ : Tie′ Link′
tie′₂ = tie′ link-b′ λ n → + n
app-tie′ : Tie′ Link′ → ℕ → Bool ⊎ ℤ
app-tie′ (tie′ link-a′ f) _ = inj₁ (f tt)
app-tie′ (tie′ link-b′ f) n = inj₂ (f n)
However, this indirect encoding is annoying to work with. Seeing as the transformation is entirely mechanical, intuitively it seems we ought to be able to somehow achieve Tie Link : Set
while retaining Link
as an indexed type, but it isn’t clear to me that this is actually possible.
Given the above context, my question is threefold:
Are
Tie
andTie′
meaningfully distinct, in the sense thatTie
allows doing things thatTie′
does not? If so, what?One can argue that
tie
does in fact containA B: Set
whiletie
does not, soTie
must surely belong toSet₁
. But the typesA
andB
can always be easily reconstructed fromLink A B
, so surely they don’t need to be stored, in a similar sense to that described in Inductive families need not store their indices. Is this reasoning flawed, or is this simply an implementation infelicity?Has the relationship between these two constructions been treated explicitly in any existing literature?