2
$\begingroup$

Please excuse my naïveté, I have no higher math education, just a curious observer. In type theories, types are treated as set-like because they're unordered collections. Yet, the putative motive in modern (constructivist) type theories is to get mathematics closer to computation, but in a computer, there can never exist an unordered collection. All data is stored and operated on in some order, sequentially. We may have a function that does not care about the order of the data it operates on, but the data then still has some arbitrary ordering. So why are all foundational math theories based on unordered collections rather than ordered?

$\endgroup$
  • 2
    $\begingroup$ "All data is stored and operated on in some order". In this part of the question you refer to an unordered collection of "all data". :) $\endgroup$ – Dag Oskar Madsen Jul 10 '17 at 7:58
  • 1
    $\begingroup$ As an analogy, sorting algorithms "operate on ordered collections". But the algorithms themselves, which is what the theory is about, are not linearly ordered in any interesting way. $\endgroup$ – Andrew Polonsky Jul 10 '17 at 13:19
  • 2
    $\begingroup$ I guess my sticking point is that, in set theory, if I declare some arbitrary set X = {a,b,c} then those elements are not in the order a then b then c. Yet as humans we have no ability to reason about such a set until I put it on paper in some arbitrary order, whether that's {a,b,c} or {b,c,a}. If you ask me "is the element "a" in set X?" I have to scan over the set in some arbitrary order, that is I need some algorithm that respects the arbitrary ordering to find the element "a" (imagine the set being much bigger so as I really would need an algorithm to find if an element is in X). $\endgroup$ – Brandon Brown Jul 10 '17 at 16:40
  • 1
    $\begingroup$ Fair point, I'm thinking more along the lines of Per Martin Löf -like intensional type theories. e.g. homotopy type theory. $\endgroup$ – Brandon Brown Jul 10 '17 at 22:24
  • 1
    $\begingroup$ If, in fact, "as humans we have no ability to reason about such a set until I put it on paper in some arbitrary order," then I must not be human. Most of my reasoning about sets involves neither an ordering nor any attempt to write down all the members of the sets. $\endgroup$ – Andreas Blass Jul 11 '17 at 1:59
2
$\begingroup$

"the putative motive in type theories is to get mathematics closer to computation": there is certainly not a single motive for type theories: first type theories were developped long before computers.

Foundational math theories also usually try to avoid as much as possible unnecessary assumptions. So if a theory does not need order on its objects, it is usually better not to add such a useless order.

$\endgroup$

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.