Can abstract concepts be represented by types in mathematics?

Question

I am reading about type theory along with abstraction and am wondering how they relate. Am i right in thinking that an abstract concept (from the result of abstraction) can be represented by a type in type theory?

Answer 1

The TLDR is that abstraction and abstract object (SEP) is probably best understood as a process of eliminating facts or structure to get to something simpler. Mathematical objects are abstract objects that represent other things.

For instance, in computer science, we have 1's and 0's and at the physical layer of the ISO OSI, the physical layer is conceived of in terms of electronics. But if I want to talk about sending email, I don't do it in the language or semantics of binary arithmetic encoded by elecromechanical circuits, I do it in terms of SMTP. Thus, we consider the email grounded in computer hardware. Email is an abstraction because quite physically, there is no piece of mail like there is in snail mail. Email is an abstract object that corresponds to physical letters. 'Email' makes it simpler to think and talk about computers than talking about binary strings.

In mathematics, we do the same. We learn naive set theory, for instance, and that appeals to our intuitions about collections and items in collections and the relations that govern them. But then we make it rigorous and call it ZFC or NBG or whatever. You can make your own theory if you want. But, along come category theorists and say, you guys are making it complicated. There are only 7 primitive ideas (think in terms of nodes and edges of a graph), and all of the rest is detail. Thus category theory abstracts over ZF, ZFC, and NBG (and others) and makes things simpler. Thus, a category is a mathematical object which abstracts from other mathematical objects.

Mathematical abstraction can also occur when consider physical objects. Take a pocket full of change and then imagine stacking up the coins on a counter. At first, we can use a set {x:x is the set of all coins in your pocket} and then switch over to a sequence (x:x is the set of all coins in your pocket from lowest to highest). And then we can do math with these symbolic abstractions of physical circumstances. For example, it's true that {a,b,c,d}!=(a,b,c,d) because sets don't account for order or repetition {a,b,c,d}=={d,a,b,c,b,a} but sequences do (a,a,b,c,d)!=(a,b,c,d,a). Of course, from there math springs to life with various theories like partially-ordered sets, real analysis, and so on. These sorts of abstractions are usually presumptions in the axiomatic method.

Oh, and yes, types are just sets that have a rule that says members of the set have to be of a certain sort, have a certain structure, or obey a certain standard. For instance, in modern computer languages, both integers and double floats are two primitve types to a compiler. We use types because it prevents problems (some types cannot belong to other types which stops Russell's paradoxesque problems in compilation) and because it allows for type checking, autounboxing, casting, etc. which are datatype operations that are governed by the type system. If you've worked in Python and C/C++ the latter is much more rigorous in its type system.