A formal identification between tuples and lists with an application to list-arithmetic categories (Q1346222)

We may say with confidence that in many papers about general programming languages either the distinction between \(n\)-tuples and lists of length \(n\) is avoided, or those objects are identified, but only at an intuitive level. That type of identification, considered formally, leads to non- trivial problems, making difficult the typing of the functions used to deal with lists, i.e., \(hd\), \(tl\), cons\dots In this paper, following computational intuitions, we present a construction of a list subject as a coproduct. This idea is the key concept that permits us to prove directly some of the presented results about list-arithmetic categories. This is a most useful construction because we construct recursive objects on the basis of the expected semantics of a list object.