<p>You can define an auxiliary predicate <code>x ∈ ℓ</code> whose elements are all the positions in <code>ℓ</code> at which <code>x</code> appears. With that in hand, you can do it as follows:</p>
<pre><code>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))
</code></pre>
<p>Is that what you had in mind? If not, you should explicitly state how many elements you expect <code>DataType A ℓ</code> to have. As many as there are elements of <code>ℓ</code>?</p>

CC BY-SA 4.0
2021-05-03T15:17:21.140Z
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: http://firsov.ee/finset/finset.pdf
Max
CC BY-SA 4.0
2021-04-29T12:13:39.123Z
2021-04-29T12:13:39.123Z
Andrej Bauer
<p>You asked several questions.</p>
<p>You asked about a type indexed by a list, so you can do this.</p>
<pre><code>data DataType (A : Type) (F : A -&gt; Type) : List A -&gt; Type where
  empty : DataType A F []
  _bla_ : forall {xs} {x} -&gt; DataType A F xs -&gt; F x -&gt; DataType A F (x ∷ xs)
</code></pre>
<p>Where <code>F</code> is a type family that is indexed by the elements of the list.</p>
<p>Apart from that, you mentioned tuples. Probably you want a sized vector (<code>Data.Vec</code> in stdlib) for tuples. For instance, <code>Vec Nat 3</code> is such a type that <code>1 ∷ 2 ∷ []</code> and <code>1 ∷ 2 ∷ 3 ∷ 4 ∷ []</code> are both invalid instances, only <code>1 ∷ 2 ∷ 3 ∷ []</code> is.</p>

CC BY-SA 4.0
2021-04-29T21:06:44.170Z
This solution is probably what the OP wanted, mine is probably is not.
Andrej Bauer
CC BY-SA 4.0
2021-05-03T15:14:09.930Z
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
CC BY-SA 4.0
2021-04-29T12:39:16.360Z
2021-04-29T12:39:16.360Z
ice1000
<p>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):</p>
<pre><code>data DataType : Type where
  inj : (xs : List A) → (x : {! xs !}) → DataType
</code></pre>
<p>Of course, we cannot have a Pi type over <code>x : xs</code> in the middle since <code>xs</code> is a <em>term</em> and not a type, so we cannot quantify over it.</p>
<p>We can use singletons to get an n-tuple from a list as follows:</p>
<pre><code>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)
</code></pre>
<p>That way a list <code>1 ∷ 2 ∷ 3 ∷ []</code> is turned into the tuple <code>(s1, s2, s3)</code>, from which can recover the numbers in the list. However, this tuple is still just one term, so we will only have a single <code>inj (s1, s2, s3)</code> in our data type above when using <code>list→type xs</code> in the Pi type above.</p>
<p>How can we get a different inhabitant in <code>DataType</code> 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 &quot;collection&quot; 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.</p>

<type-theory><dependent-type><agda>
Pi-type over a list in dependent type theory
Max
# Pi-type over a list in dependent type theory

(Asked by: username_0 on 2021-04-29)

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.

**Tags:** type-theory, dependent-type, agda


---

## 2 answers

### Answer by username_1 on 2021-04-29. Score: 0 | Accepted answer

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

> **Comments:**
> **username_0**: 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: http://firsov.ee/finset/finset.pdf  

---

### Answer by username_2 on 2021-04-29. Score: 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.

> **Comments:**
> **username_1**: This solution is probably what the OP wanted, mine is probably is not.  
> **username_0**: 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 username_2!  

---

