0
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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 ?

$\endgroup$
1
  • $\begingroup$ 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 $\endgroup$
    – Max
    May 3 at 15:17
2
$\begingroup$

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.

$\endgroup$
2
  • 1
    $\begingroup$ This solution is probably what the OP wanted, mine is probably is not. $\endgroup$ Apr 29 at 21:06
  • 1
    $\begingroup$ 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! $\endgroup$
    – Max
    May 3 at 15:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.