Parameterized Datatypes in a Universe à la Tarski?

Question

I'm wondering, is there a way to make a Universe à la Tarski that models all of the types in an open type theory, where there can be user defined parameterized inductive types?

For context, I'm trying to write a syntactic model of a type theory I've got with a kind of type-case, essentially like Section 5.2 of this paper. I'm mechanizing the model in Agda, but I'm trying to abstract over the defined inductive types, so that I know my mechanization works for any set of inductive types.

The idea is that types in the source language are modeled in the target as an inductive-recursive type $Code\ \ell$, defined with an "elements-of" interpretation $El : Code \to Set$. To capture "all" the datatypes, there's a mutually-defined type $Desc$ of descriptions of inductive types, like in Diehls and Sheard or McBride:

data Desc ℓ : Set where
   End : Desc ℓ
   Arg : (c : Code ℓ) -> (El c -> Desc ℓ) ->  Desc ℓ
   Rec : Desc ℓ -> Desc ℓ

What's different than usual here is that Arg takes a code describing a type, not a type itself, which lets us model type-case stuff.

I'm wondering, is there a way to extend this to allow for parameterized inductive types? The usual trick with $Desc$ is to define a parameterized type as a function $(x : Params) \to Desc$. e.g. the description for $List$ is a function $DList : Set \to Desc$. But this doesn't work when Arg takes a $Code$ instead of a type, since (as far as I can see) this requires a bunch of mutual references between $Code$ and $Desc$ that break strict positivity.

Is this similar to anything that's been done? Is there a known solution to this, or is this pushing beyond what can be modeled with a single Tarski universe?

Answer 1

Arg : (c : Code) -> (El c -> Desc) ->  Desc

Are you sure this is what you mean? I think the usual constructor is closer to the following:

Arg : (c : Code) -> (Mu c -> Desc) ->  Desc

As for your original question, you could make Desc take a vector of parameters and add a new constructor to mean "a value of type this parameter". Because your sigma is taking a code now and if we don't want to rely on external datatypes we'll need a sum constructor too.

First let's get the options & imports out of the way

{-# OPTIONS --safe #-}

open import Data.Unit.Base using (⊤; tt)
open import Data.Product using (Σ-syntax; _×_; _,_)
open import Data.Nat.Base using (ℕ; _+_)
open import Data.Fin.Base using (Fin; zero)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Data.Vec.Base using (Vec; []; _∷_; lookup)

Then a big pile of mutually recursive description, decoding, and fixpoint operator. The new things are:

• the ps parameter and the p constructor to make use of a paremeter type
• the changed type of Arg (which I called σ)
• the + for sums

data Desc {n} (ps : Vec Set n) : Set
El : ∀ {n} {ps : Vec Set n} → Desc ps → Set → Set
data μ {n} {ps : Vec Set n} (d : Desc ps) : Set where
  mk : El d (μ d) → μ d

data Desc {n} ps where
  `■ : Desc ps
  `p : (k : Fin n) → Desc ps
  _`+_ : (d, e : Desc ps) → Desc ps
  `σ : (d : Desc ps) → (μ d → Desc ps) → Desc ps
  `x : Desc ps → Desc ps

El `■ x = ⊤
El {ps = ps} (`p k) x = lookup ps k
El (d `+ e) x = El d x ⊎ El e x
El (`σ d f) x = Σ[ v ∈ μ d ] El (f v) x
El (`x d) x = x × El d x

And then you can write list as

`List : (A : Set) → Desc (A ∷ [])
`List A = `■ `+ `σ (`p zero) λ _ → `x `■

I did not have the courage to also encode nat & define addition so I'm using an external definition for the example:

pattern nil = mk (inj₁ tt)
pattern _::_ x xs = mk (inj₂ (mk x , xs , tt))

sum : μ (`List ℕ) → ℕ
sum nil = 0
sum (n :: ns) = n + sum ns

Of course this has all sorts of annoying consequences as in:

1. how do I use e.g. the code for Bool (indexed by an empty vector) in a description indexed by a larger vector? I suspect the right answer here is: add a constructor that allows you to use the action of a thinning on the current vector of parameters to restrict it to a subvector (for Bool you'd pick the empty thinning that throws everything away).

2. can I write a generic map acting on the parameters that happen to be used in a positive manner? I suspect the right thing to do here is to demand for each parameter whether it is meant to be used in a positive, negative, or mixed variance and add restrictions to the way the p constructor can be used so that these declarations are respected.