Relationship between inductive families and type-returning functions

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 existentials. 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 formula

As mentioned by Andrej, this is an instance of transporting along an equivalence of families and display maps. In this specific case, we have an equivalence of graphs and relations.

open import Function
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Level renaming (zero to lzero; suc to lsuc)

-- type of relations on a set
Rel : ∀{i j} → Set i → Set (i ⊔ lsuc j)
Rel {i}{j} V = V → V → Set j

-- type of graphs with set of vertices V
record Graph {i j}(V : Set i) : Set (i ⊔ lsuc j) where
  field
    E   : Set j   -- edges
    src : E → V   -- source vertex
    tgt : E → V   -- target vertex
open Graph

Rel→Graph : ∀ {i j V} → Rel {i}{j} V → Graph {i}{i ⊔ j} V
Rel→Graph R = record {
  E   = ∃₂ λ s t → R s t ;
  src = proj₁ ;
  tgt = proj₁ ∘ proj₂ }

Graph→Rel : ∀ {i j V} → Graph {i}{j} V → Rel {i}{i ⊔ j} V
Graph→Rel {V} G s t = ∃ λ e → (G .src e ≡ s) × (G .tgt e ≡ t)

Note that we can only define the round-tripping functions if i ≤ j, since then the output i ⊔ j level becomes j, and the trip is well-typed. Your Link definition does not fit into this, but it's possible to just redefine it as Link : Set → Set → Set₁ without loss of generality (as the two definitions are equivalent).

If the levels check out, we can show that round-tripping in both directions yields equivalent relations and graphs respectively. We don't need to know anything about the internals of the relations and graphs involved; this equivalence always holds.

Your transformation makes use of the fact that the set of edges for the graph is equivalent to a small set, since the relation only has two possible edges.

open import Data.Unit
open import Data.Bool
open import Data.Integer
open import Data.Nat

data Link : Set → Set → Set where
  link-a : Link ⊤ Bool
  link-b : Link ℕ ℤ

-- the graph of Link
Link' : Graph Set
Link' = Rel→Graph Link

-- an equivalent graph with smaller edges
Link'' : Graph Set
Link'' = record {
  E   = Bool ;
  src = λ {false → ⊤; true → ℕ} ;
  tgt = λ {false → Bool; true → ℤ} }

Now, anything which depends on an edge only needs to depend on a Bool. In particular, Tie' Link'' : Set.

record Tie {j} (R : Rel {_}{j} Set) : Set (lsuc j) where
  field
    E   : ∃₂ λ A B → R A B
    fun : proj₁ E → proj₁ (proj₂ E)

record Tie' {j} (G : Graph {_}{j} Set) : Set j where
  field
    E   : G .E
    fun : G .src E → G .tgt E

The equivalence of graphs and relations generalizes to relations of any arity, and also to multiple relations of arbitrary arities, where relations can be indexed over other relations. In general, the equivalence says that for each telescope of dependent n-ary relations, there is a direct category $C$ such that the telescope is equivalent to the set of functors from $C$ to $\textbf{Set}$.

In the case of graphs, $C$ has two objects and two arrows between them, going in the same direction, so a functor $F : [C,\textbf{Set}]$ consists of two sets $V,E$ and two functions $src, tgt : E \rightarrow V$, so we can see that every $F$ is a graph.

Are Tie and Tie′ meaningfully distinct, in the sense that Tie allows
doing things that Tie′ does not?

They are equivalent, we get one from the other by transporting the parameter along the graph-relation equivalence.

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.

If we're working in cubical Agda, the graph-relation equivalence can be proven using univalence. Then, every possible construction which depends on a relation can be transported to another which depends on a graph. Additionally, everything which depends on Link can be transported to depend on Rel→Graph Link. So at least this part works completely automatically.

However, the resizing part is not automatic, i.e. we have to prove that Rel→Graph Link is equivalent to Link'' with the small set of edges. It is not true in general that the set of edges for a relation is smaller than the set of vertices. Probably it's possible to have a conservative algorithm which tries to find such resizings, I don't think it has been researched.

... 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?

The technique in "Inductive types need not store their indices" is related but not exactly the same thing. In that paper, the transformation is a bit more restricted & specific thing, as there the point is to convert an inductive type family to a purely recursive one. The family-display map translation can be also used to get rid of indices, but that works in a "non-algorithmic" and different way. A classic example is vectors.

Let's have Vec A : ℕ → Set. We have an equivalence between ℕ → Set and Σ Set λ A → (A → ℕ) (as another case of the family

StackExchange Computer Science Q#132664, answer score: 4