4
$\begingroup$

What's the most pragmatic encoding for inductive-inductive types such as for a universe of types?

In pseudo Coq syntax.

Inductive U :=
| unit
| Sigma (A: U) (B: El A -> U)
with El: U -> Set:=
| tt: El unit
| pair (a: El A): El (B a) -> El (Sigma A B)
.
$\endgroup$
3
  • $\begingroup$ Encoding in what sense? Plain lambda calculus? Or something else? $\endgroup$ Oct 18, 2022 at 1:24
  • $\begingroup$ @FrançoisG.Dorais in dependent type theory with indexed inductive types. I am most familiar with Coq but it seems silly to restrict to it. Not sure Coq would have any features in particular better for the task. Maybe polymorphic cumulativity? $\endgroup$ Oct 18, 2022 at 4:59
  • $\begingroup$ Related (though not an exact answer to the question): effectfully.blogspot.com/2016/10/insane-descriptions.html $\endgroup$ Oct 19, 2022 at 7:57

2 Answers 2

7
$\begingroup$

Your example signature is negative recursive in the second field of Sigma so it can't be encoded in total languages.

For internal universes, the usual solution is to use induction-recursion instead. In Agda:

open import Data.Product
open import Data.Unit

data U : Set
El : U → Set

data U where
  unit  : U
  sigma : (A : U) → (El A → U) → U

El unit = ⊤
El (sigma a b) = Σ (El a) λ x → El (b x)

Induction-recursion has a reasonably concise generic scheme which can be represented in Agda.

On the other hand, inductive-inductive signatures have no known representation which is concise enough to be actually usable in Agda (for generic programming). The most concise specification is to say that signatures are type contexts in a "strictly positive" dependent type theory. Possible embeddings of this in Agda are rather difficult and tedious for practical programming purposes.

$\endgroup$
3
$\begingroup$

To complement András' answer, and especially if you want to stay in Coq, you can also define such an internal universe using indexed inductive types only. Basically, you replace the definitions of both U and El by a unique indexed inductive type, from which you can recover U and El after the fact.

Record Unit : Set := {}.

#[universes(polymorphic), projections(primitive)]
  Record Σ {A : Type} {B : A -> Type} : Type :=
    { fst : A ; snd : B fst }.
Arguments Σ : clear implicits.

Inductive Udec : Set -> Type@{Set + 1} :=
  | _unit : Udec Unit
  | _sigma {ElA : Set} (A : Udec ElA) {ElB : ElA -> Set}
      (B : forall a, Udec (ElB a)) : Udec (Σ ElA ElB).

Definition U@{i | Set < i } : Type@{i} := Σ@{i i} Set Udec.
Definition El (code : U) : Set := code.(fst).

Definition unit : U :=
  {| fst := _ ; snd := _unit |}.
Definition sigma (A : U) (B : El A -> U) : U :=
  {| fst := _; snd := _sigma A.(snd) (fun a => (B a).(snd)) |}.

Note that I have been somewhat explicit with universes, to showcase the fact that this encoding needs to bump universe levels: U cannot live at the lower level (Set) in this version, while it can in the inductive-recursive one. This is because the constructors of Udec must contain types.

$\endgroup$
3
  • $\begingroup$ I feel like there has to be a better way of doing this but I can't figure it out 🤷‍♀️. It doesn't feel right to pattern match on types but unrolling things a bit so Udec is constructed with algebras doesn't really work. Maybe you want parametricity for that sort of impredicative encoding? $\endgroup$ Oct 20, 2022 at 0:59
  • $\begingroup$ I'm not sure of what you mean? This does not pattern match on types? And this is also not impredicative, all you need are two (predicative) universe levels? $\endgroup$ Oct 20, 2022 at 18:45
  • $\begingroup$ yeah you don't need need impredicativity. What I meant about pattern match on types is have indexing by a type. Iirc you would want to work with isomorphisms or functions instead $\endgroup$ Nov 6, 2022 at 5:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.