Pi-type over a list in dependent type theory

Question

In a formalization I need to create an inductive type which has a term for each element in a list, something like this (I'll use Agda in the following, but everything here is standard dependent type theory):

data DataType : Type where
  inj : (xs : List A) → (x : {! xs !}) → DataType

Of course, we cannot have a Pi type over x : xs in the middle since xs is a term and not a type, so we cannot quantify over it.

We can use singletons to get an n-tuple from a list as follows:

Singleton : (x : A) → Type
Singleton x = Σ[ y ∈ A ] (y ≡ x)

list→type : List A → Type
list→type [] = ⊥
list→type (x ∷ []) = Singleton x
list→type (x ∷ y ∷ xs) = Singleton x × list→type (y ∷ xs)

That way a list 1 ∷ 2 ∷ 3 ∷ [] is turned into the tuple (s1, s2, s3), from which can recover the numbers in the list. However, this tuple is still just one term, so we will only have a single inj (s1, s2, s3) in our data type above when using list→type xs in the Pi type above.

How can we get a different inhabitant in DataType for each element of the list? Is there a standard way to deal with that? Or do I fundamentally misunderstand something? It's of course a bit awkward to mix a data structure understanding of "collection" with the basic doctrine of regarding types as collections (with explicit term constructors), but it still should be possible to reconcile both understandings I hope.

Answer 1

You can define an auxiliary predicate x ∈ ℓ whose elements are all the positions in ℓ at which x appears. With that in hand, you can do it as follows:

data List (A : Set) : Set where
  [] : List A
  _::_ : A → List A → List A

infixr 5 _::_
infix 4 _∈_

data _∈_ {A} (x : A) : List A → Set where
  ∈-head : ∀ {ℓ} → x ∈ x :: ℓ
  ∈-tail : ∀ {y} {ℓ} → x ∈ ℓ → x ∈ y :: ℓ

data DataType (A : Set) : Set where
  inj : (xs : List A) → ∀ x → x ∈ xs → DataType A

data Five : Set where
  one two three four five : Five

mylist = two :: three :: two :: five :: []

demo : DataType Five
demo = inj mylist two ∈-head

demo' : DataType Five
demo' = inj mylist two (∈-tail (∈-tail ∈-head))

Is that what you had in mind? If not, you should explicitly state how many elements you expect DataType A ℓ to have. As many as there are elements of ℓ?

Answer 2

You asked several questions.

You asked about a type indexed by a list, so you can do this.

data DataType (A : Type) (F : A -> Type) : List A -> Type where
  empty : DataType A F []
  _bla_ : forall {xs} {x} -> DataType A F xs -> F x -> DataType A F (x ∷ xs)

Where F is a type family that is indexed by the elements of the list.

Apart from that, you mentioned tuples. Probably you want a sized vector (Data.Vec in stdlib) for tuples. For instance, Vec Nat 3 is such a type that 1 ∷ 2 ∷ [] and 1 ∷ 2 ∷ 3 ∷ 4 ∷ [] are both invalid instances, only 1 ∷ 2 ∷ 3 ∷ [] is.