# Pi-type over a list in dependent type theory

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.

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

• Thank you, the simple definition of ∈ is really all I needed to clear up my confusion. I also found this paper helpful, which establishes some connections between lists and finite sets: firsov.ee/finset/finset.pdf
– Max
May 3, 2021 at 15:17

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.

• This solution is probably what the OP wanted, mine is probably is not. Apr 29, 2021 at 21:06
• My attempted solution with iterated Sigma-types was gaslighting and due to a confusion on my side, I was really only wondering about how to express membership in a list. Hence I chose Andrej's answer, but thanks for your response ice1000!
– Max
May 3, 2021 at 15:14