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?

  • 1
    $\begingroup$ Take a look at "Generic Programming with Indexed Functors" as well, they have a different approach for parametrized datatypes. $\endgroup$ Commented Mar 23, 2022 at 7:51
  • 1
    $\begingroup$ I think "Fully Generic Programming Over Closed Universes of Inductive-Recursive Types" is also relevant. $\endgroup$ Commented Mar 23, 2022 at 7:59

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

  • 1
    $\begingroup$ Your first clarification actually reveals the problem of my approach: I was trying to have $Desc$, descriptions of datatypes, as a separate type from $Code$, the big sum describing all the type constructors. I'd never thought to define non-inductive types as functors that ignored their arguments. $\endgroup$ Commented Mar 22, 2022 at 18:34

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.