 Assuming a domain of entities, contexts are finite lists of entities. If \(c\) is a context of length \(n\), then we refer to its elements as \(c[0]\), \(\ldots ,c[n-1]\), and to its length as \(\lvert c\rvert\). We will refer to the type of contexts of length \(i\) as \([e]^i\). If \(c\) is a context in \([e]^i\), then objects of type \(\{0, \ldots ,i-1\}\) can serve as indices into \(c\). If \(c \in[e]^i\) and \(j \in \{0, \ldots ,i-1\}\), then \(c[j]\) is the object of type e that occurs at position \(j\) in the context. A key operation on contexts is extension with an element. If \(c :: [e]^i\) and \(x :: e\) (\(c\) is a context of length \(i\) and \(x\) is an entity) then \(c\mcaret x\) is the context of length \(i+1\) that has elements \(c\)[0], \(\ldots ,c[i-1], x\). Thus \(\mcaret\) is an operator of type \([e]^i \rightarrow e \rightarrow[e]^{i+1}\). Also note that types like \([e]^i\) are in fact polymorphic types, with \(i\) acting as a type variable. See Milner 1978.