9 ms·

Types versus sets in math and programming languages

107 points by classified 5y ago

triska 5y ago
This strikes me as a quite language-specific treatise, and may indicate a shortcoming or particularity of the syntax or semantics of the described programming language (i.e., Disco) rather than an essential conceptual difference. For comparison, in Prolog, a type is indeed a set of terms! For example, the type "integer" truly denotes the set of integers, and if an argument has the type "integer", then we know that the predicate can only hold if that argument is an element of this type. Quoting from the Prolog ISO standard: 7.1 Types The type of any term is determined by its abstract syntax (6.1.2). Every term has one of the following mutually-exclusive types: V (variables), I (integers), F (floating point values), A (atoms), CT (compound terms). A term with type I, F, or A is an atomic term. and further: 7.1.2 Integer An integer is a member of a set I (see 6.1.2 c) where I is a subset of ℤ characterized by one or three parameters. Prolog also has type errors: "There shall be a Type Error when the type of an argument or one of its components is incorrect, but not a variable." For example, in Scryer Prolog, we get: ?- length(Ls, a). caught: error(type_error(integer,a),length/2) This is because the second argument of length/2 must be an element of the set I of integers. Since the atom 'a' is not an integer, the relation does not hold in this case. Declaratively, a type error is equivalent to silent failure: It means that the relation cannot hold for this type of argument, and so every specialization of the query will also not hold, whereas a generalization or an instantiation with a term of a different type may succeed. This view readily carries over to logic variables. For example, using library(clpz), we get: ?- X #> 3. clpz:(X in 4..sup). And we get a type error if we try to instantiate the thus constrained variable X to a term that is not an element of ℤ: ?- X #> 3, X = a. caught: error(type_error(integer,a),unknown(a)-1) So, indeed, types denote sets of terms that are acceptable as arguments. The example in the article, i.e., ℕ, could be regarded as an element of the set of atoms in Prolog, and therefore have the type atom. In indeed, for example Trealla Prolog answers: ?- atom(ℕ). true.
- elliekelly 5y ago
  Only tangentially related, every once in a while I look for a book, video, or even course that concisely explains the “language” of mathematical notation. As someone who is largely self-taught when it comes to the more advanced math it’s frustrating that so many resources assume a basic level of notational knowledge/understanding so they just skip right over it and you’re left piecing it together using context clues and LaTex crib sheets.
  - kmill 5y ago
    For better or for worse, piecing things together using context clues never seems to really end :-) One useful heuristic is the "unambiguous parse rule." You think about different ways something might be read (even if you have no idea what it's trying to say yet) and try to work out which one would lead to the least ambiguity. This is helpful also when trying to figure out how to write using newly learned notation yourself. A good technique is to just not get frustrated. All math starts impenetrable. Read ahead, try to get a glimpse of an idea of what's going on. Go back, find other sources about the same thing, find sources about similar things. If the original source was worth anything, eventually it'll reveal itself. Sometimes you realize you weren't the target audience and you were supposed to have been exposed to more introductory material and you wish they had cited one, but anyway, you found it. Another thing is that sometimes you just need to ask an expert, someone who's steeped in the culture. math.stackexchange.com is open to notation questions, but the guidance you can get in-person can be much more nuanced. I actually like running into new notation (supposing I'm not on a deadline trying to figure something out...), be it math or a programming language. You're trying to solve the puzzle of the purpose of the notation, what function does it serve, why someone ever thought this was a good idea. I've exposed myself to a lot of bits of obscure programming languages over the years, which makes it easier to guess what things might mean. Maybe one more thing: math notation tends to be invented for specific purposes, and maybe most of it doesn't carry over from subject to subject. Arithmetic, function application, summations, integrals, and set notation are fairly universal though.
- tel 5y ago
  This is an old yarn distinguishing sets and types, extrinsic and intrinsic, "run time" and "compile time". The idea of a runtime procedure `?- atom(_)` which determines `true.` or `false.` is fundamentally an extrinsic property, thus "set like". Intrinsically defined objects are defined through (possibly inductive) construction or (possibly coinductive) destruction rules. Typically a notion of set arises from having some larger universe of things and restricting them via predicates. The notion of types arises from having a system of building (co)inductive definitions and then utilizing that system. Sets are thus, in a sense, fundamentally based on a closed world (said universe) and types an open world (each new utilization of the rules system introduces a novel type).
tromp 5y ago
I think calling the type of natural numbers ℕ instead of Natural is causing the confusion. Students would be less tempted to write {1,2} ⊆ Natural as the right side looks like a type name rather than a value . Haskell helps to maintain the distinction by using capitals for type names and lower case for variable names. I would seem natural to write: naturals :: Set Natural naturals = {0,1..} {1,2} ⊆ naturals
- mjburgess 5y ago
  You're downvoted, but what you've said is basically the point-of and conclusion-to the article. `N` denotes a set and `Natural` denotes a type, and one cannot be eliminated to the other in all contexts of use.
klodolph 5y ago
Coming from the mathematics side of things, > In a math class, we typically tell students that ℕ is a set. I think the approach is a bit glib. There are some caveats—a student with more mathematical experience would think of ℕ as a set, or a type, or as objects in various categories. It’s also worth asking a student what 1∪2 is. Most people will look at that and just tilt their head, even though common foundations for mathematics treat 1 and 2 as sets. It turns out most people don’t want to work in foundations, and want to think of 1 and 2 as non-sets. The same applies in the other direction, upwards, when you think of ℕ as a type (even though it is also a set).
- vkazanov 5y ago
  My math is shallow at best but... 1∪2 would become just 2 with integers represented as sets in certain foundational theories, right?
  - hansvm 5y ago
    Yes. One common definition is equivalent to each natural to being the set containing all preceding naturals. With that view 2={0,1} and 1={0}, so their union is just 2.
  - Spivak 5y ago
    Yep! But notation depends a lot on the author to some extent. You will find people who treat 1U2 as {1}U{2} because it’s less annoying to write. It’s the same reason languages have an .add method on sets so you don’t have to write. s = s.union(set(s))
    - deleted 5y ago
      [deleted]
    - alisonkisk 5y ago
      who writes 1U2 instead of {1,2} ? When would {1}U{2} ever appear in ant context except for the first day of Intro to Set Theory?
k__ 5y ago
Half-OT: What's the reason rationals aren't used often in programming?
- mjburgess 5y ago
  You mean full-precision integer representations? A percentage is effectively this -- and floats are often multipliers on integers which are "holding the precision". However it isn't clear what standards sorts of arithmetical use cases storing two integers helps with (over, say, integer & float, etc.).
  - k__ 5y ago
    I'm not sure either, that's why I asked. :D
    - mjburgess 5y ago
      I'm not an expert but, certainly, (1) limited memory on historical machines necessitated a small-width representation of a real number; (2) limited cpus meant simple operations needed to be applied to this small-width representation in one go. Ie., your CPU is just a system for taking bit patterns and producing new bit patterns: (0000 0000) -> (1010 0101). So you want each individual number to be of a size the processor can operate on in one pass. By using two integers you gain some capacity (ie., you can still overflow), but lose memory and compute performance.
- hansvm 5y ago
  Rationals are typically slower (gcd operations) and prone to memory explosion if the set of possible denominators isn't extremely nice. If approximate answers suffice then a scheme like floats or doubles is usually good enough. If approximate answers suffice and floats or doubles have undesirable properties (weird density distributions, ranges larger than what your application needs, ...) then it's easy to hack something together with a few _bounded_ integer types which has better properties for your specific needs. In most other practical applications some kind of a fixed-precision decimal suffices. It's a bit slower than floats and might have undesirable memory characteristics, but broad classes of real-world numbers which need to be represented exactly (like financial data) are nicely represented. Compared with those (and other) schemes, what advantages do rationals have? Chiefly, they admit an exact representation of any rational number. If you can mitigate the downsides (e.g., by not having many possible denominator prime factors) and need those benefits then rationals might be a good fit. One practical situation where I occasionally like to use rationals is in account data -- credits, currencies, .... It lends itself to forward compatibility when new features are desired (most often that the smallest atomic unit in a currency changes or that some niche system wants to offer transactions for 1/3 of a unit). Such changes usually have small, nice, compatible denominators, so you don't have unbounded memory issues. More importantly, all such operations are exact by definition without any extra work on my part (the biggest challenges are in display and formatting if your business admits those sorts of oddities).
mjburgess 5y ago
I think a clearer way of putting is this: types are not a mathematical notion. So "Bool" is not the same as "{On, Off}" nor "{0, 1}" nor "{Up, Down}" etc. We can reduce a type to a set of all constructible values; likewise we can reduce english to the "big infinity" of all possible sentences expressed in all possible universes. But english isnt this set. If one had this set, E, then you could reduce the question of whether a conversation (C) is valid english to set-membership, "is C in E?" but this misses whether the conversation is actually about anything. Likewise "me" can occur in an infinite number of sets (Person, RandomObjectsOnEarth, ...), but that "me in Person" is the "valid question" has nothing to do with "me in Person" -- and everything to do with the semantics of me/Person. "Person" is about "me". It is for this reason that values have "principal types" in programming languages; ie., the "set" which happens to be about the value. Insofar as mathematics is employed to model reality we have to introduce non-mathematical devices to constrain its application, types may be understood as the formal mechanism to do this.
- Ericson2314 5y ago
  Types absolutely are a mathematical notion. Formal systems like the calculus of construction and Martin Löf Type Theory are well studdied.
  - mjburgess 5y ago
    That doesn't have much to do with my point. There is no mathematical encoding of natural world semantics: the sense in which "Person" and "MostIntelligentSpecies" are different cannot be expressed mathematically. (p in Person) obtains as does (p in MostIntelligentSpecies) but Person cannot be eliminated for MostIntelligentSpecies The article itself makes this point, but then tries to compromise with the mathematical reduction "to sets". It would be clearer just to state that this is a reduction rather than an elimination.
kuprel 5y ago
I don’t think you need the distinction for the natural numbers. Int32 is a type. The natural numbers are the set of positive integers that don’t overflow the int type used to express them.
- Ericson2314 5y ago
  This language is surely going to use bignums to avoid all that nonsense.
amw-zero 5y ago
It might help to consider the history of types and sets. Sets (and consequently modern math and logic) have not been around for as long as we might think. Maybe we had them in different forms, but sets as we know them today were born in 1874 in this paper: https://srjcstaff.santarosa.edu/~jomartin/IrratFiles/Cantors1874Paper.pdf https://srjcstaff.santarosa.edu/~jomartin/IrratFiles/Cantors.... Around 1901, Bertrand Russell discovered a paradox in this formulation of sets, so-called Russel's Paradox: https://en.wikipedia.org/wiki/Russell's_paradox https://en.wikipedia.org/wiki/Russell's_paradox. There are then many ways of dealing with this paradox. The most widely accepted way is to just reformulate the axioms, which was done with Zermelo-Frankel set theory: https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t.... When people use the word "mathematics" today, they generally implicitly mean that ZFC is being used. It's the most widely accepted mathematical foundation we have. Another path was proposed by Russell himself, and that is the notion of "type." By restricting the way in which certain operations and their arguments can be considered "valid," his own paradox can be avoided. So from the beginning, sets are about _collecting_, and types are about _restricting_.
- ProfHewitt 5y ago
  Types are about rigorously constructing mathematical abstractions from primitive types defined up to a unique isomorphism. In fact, types have become the primary foundation of Computer Science. Russell introduced the crucial concept of the order of a proposition to block his famous paradox as follows: Without orders on propositions, the paradoxical predicate I’mNotSelfApplicable (such that I’mNotSelfApplicable[I’mNotSelfApplicable]⇔¬I’mNotSelfApplicable[I’mNotSelfApplicable]) could be constructed using the following recursive definition: I’mNotSelfApplicable:Predicate<i>≡¬I’mNotSelfApplicable[I’mNotSelfApplicable] Since I’mNotSelfApplicable is a predicate variable in the definition, ¬I’mNotSelfApplicable[I’mNotSelfApplicable]:Predicate<i+1>. Consequently, I’mNotSelfApplicable:Predicate<i>⇒I’mNotSelfApplicable:Predicate<i+1> which is a contradiction meaning that I'mNotSelfApplicable does not exist. See video: https://www.youtube.com/watch?v=AJP1VL7shiI https://www.youtube.com/watch?v=AJP1VL7shiI
- ProfHewitt 5y ago
specialist 5y ago
> Sets are characterized by the \in relation: we can ask which items are elements of a set and which are not. > Types, on the other hand, are characterized by how elements of the type are built: we can construct elements of a type (and deconstruct them) in certain ways specific to the type. Huh. So sets vs types are like folksonomies vs taxonomies? Neat. -- Tangent: > Disco> {1,2} ⊆ {1,2,3} Dumb question: How are you entering mathematically symbols? My hobby language recognizes both "!=" and "≠" as "not equal", and I use a font with ligatures to render them the same.
Ericson2314 5y ago
I feel like the author should just write call Set FiniteSet, and then a lot of confusion would go away! https://golem.ph.utexas.edu/category/2021/06/large_sets_1.html https://golem.ph.utexas.edu/category/2021/06/large_sets_1.ht... also, I highly recommend this series for anyone interested in sets outside of set theory.
raphlinus 5y ago
From the title, I thought it was going to be an extension of this discussion: https://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista https://mathoverflow.net/questions/376839/what-makes-depende... It's not, exactly, but some of the concepts do overlap. In particular, the idea of being able to write things in a "natural" mathematical style, then have them translate to an obsessively precise internal representation, is essentially the problem of "elaboration" as described in the top answer.
nolta 5y ago
Here's a nice video with a little more detail on the difference between intensional/extensional: https://www.youtube.com/watch?v=bNG53SA4n48 https://www.youtube.com/watch?v=bNG53SA4n48
piinbinary 5y ago
> So types are prior to sets: types provide a universe of values, constructed in orderly ways, that we can work with; only then can we start picking out certain values to place them in a set. What about uninhabited types? Or types where the constructor is not enough to determine the entire type? e.g. data MyType a b = MyConstructor { myField :: a }
- tel 5y ago
  What's the question? For uninhabited types there's a universe (empty), ways to construct (no ways), ways to work with (any way), and you can (tautologically) pick out values and put them in sets. Constructors aren't first order meaningful (except in higher-kinded calculi) but for any concrete types `A` and `B`, `MyType A B` is a type with a universe of values (isomorphic to `A`'s universe), ways to construct and use (again, isomorphic to `A`s), and we can place them in sets.
  - piinbinary 5y ago
    I think I see now. So the author wasn't saying that construction of values is what defines the type. Rather it is a necessary step before you can start talking about sets of values. (And you can talk about a type without knowing how to construct it, so that makes types different from sets?)
    - tel 5y ago
      I think I see what the question is now. A type is defined by picking how its values are introduced and/or used. It doesn’t mean that those rules have to be actually productive. In fact there are many kinds of uninhabited types (the empty type being the simplest, but in languages with rich type systems there are many others).
didibus 5y ago
Isn't the confusion just that the Disco language uses the same symbol for its type that math uses for a very commonly known set? The symbol ℕ commonly refers to a set, but on Disco it suddenly refers to a type, it's not surprising that the confusion arises, especially since Disco also includes the concept of sets. > The set of natural numbers, denoted ℕ This is mostly how math refers to it, you can see both set and type here, the set of type natural numbers is denoted ℕ, thus "natural number" is the type and "ℕ" is the set. The type describes the rules for what is included in the set (in this case: all natural numbers), and the set is the list of all things that are included (each of the natural numbers themselves). The set of <type> is denoted <notation>
- alisonkisk 5y ago
  It gets even weirder when Brent (an expert in Haskell and math, both of which feature infinite sets!) expresses concern that he'll have to add infinite sets to his language, as though that wasn't totally obvious from the start.
chobytes 5y ago
Honestly philosophers getting ahold of set theory is probably one of the worst things to happen to it. I feel like it can be hard for people to take set theory seriously when the conversation about it is dominated by this kind of drivel. Basically this kind of dichotomy, and this image of set theory as the source of all truth in math or whatever... is essentially a myth made up by people peddling their own (new and improved!) foundations project as the source of all truth.
kazinator 5y ago
> keyword "ℕ" cannot be used as an identifier It looks to me like the guy has an outbreak of reservedkeyworditis the language that he's trying to handwave around with some talking point about sets versus type. But a syntax error of a reserved keyword being used in some phrase structure that calls for a a non-reserved identifier doesn't have anything to do with type semantics. The phrase structure of the A ⊆ B syntax could allow B to be certain keywords, such as ℕ, which is treated as a set in that context in the appropriate way (via an implicit conversion or whatever). We know what A ⊆ N means; what the programmer is asking. The requirement is not unclear. Moreover, it is doable. The question is do you do that, or not.
- jdmichal 5y ago
  That struck me too. My initial impression was to simply implement "Set s ⊆ Type t" as something like "∀i: sᵢ instanceof t"

107 points by classified 5y ago

This strikes me as a quite language-specific treatise, and may indicate a shortcoming or particularity of the syntax or semantics of the described programming language (i.e., Disco) rather than an essential conceptual difference. For comparison, in Prolog, a type is indeed a set of terms! For example, the type "integer" truly denotes the set of integers, and if an argument has the type "integer", then we know that the predicate can only hold if that argument is an element of this type. Quoting from the Prolog ISO standard: 7.1 Types The type of any term is determined by its abstract syntax (6.1.2). Every term has one of the following mutually-exclusive types: V (variables), I (integers), F (floating point values), A (atoms), CT (compound terms). A term with type I, F, or A is an atomic term. and further: 7.1.2 Integer An integer is a member of a set I (see 6.1.2 c) where I is a subset of ℤ characterized by one or three parameters. Prolog also has type errors: "There shall be a Type Error when the type of an argument or one of its components is incorrect, but not a variable." For example, in Scryer Prolog, we get: ?- length(Ls, a). caught: error(type_error(integer,a),length/2) This is because the second argument of length/2 must be an element of the set I of integers. Since the atom 'a' is not an integer, the relation does not hold in this case. Declaratively, a type error is equivalent to silent failure: It means that the relation cannot hold for this type of argument, and so every specialization of the query will also not hold, whereas a generalization or an instantiation with a term of a different type may succeed. This view readily carries over to logic variables. For example, using library(clpz), we get: ?- X #> 3. clpz:(X in 4..sup). And we get a type error if we try to instantiate the thus constrained variable X to a term that is not an element of ℤ: ?- X #> 3, X = a. caught: error(type_error(integer,a),unknown(a)-1) So, indeed, types denote sets of terms that are acceptable as arguments. The example in the article, i.e., ℕ, could be regarded as an element of the set of atoms in Prolog, and therefore have the type atom. In indeed, for example Trealla Prolog answers: ?- atom(ℕ). true.

elliekelly 5y ago
Only tangentially related, every once in a while I look for a book, video, or even course that concisely explains the “language” of mathematical notation. As someone who is largely self-taught when it comes to the more advanced math it’s frustrating that so many resources assume a basic level of notational knowledge/understanding so they just skip right over it and you’re left piecing it together using context clues and LaTex crib sheets.
- kmill 5y ago
  For better or for worse, piecing things together using context clues never seems to really end :-) One useful heuristic is the "unambiguous parse rule." You think about different ways something might be read (even if you have no idea what it's trying to say yet) and try to work out which one would lead to the least ambiguity. This is helpful also when trying to figure out how to write using newly learned notation yourself. A good technique is to just not get frustrated. All math starts impenetrable. Read ahead, try to get a glimpse of an idea of what's going on. Go back, find other sources about the same thing, find sources about similar things. If the original source was worth anything, eventually it'll reveal itself. Sometimes you realize you weren't the target audience and you were supposed to have been exposed to more introductory material and you wish they had cited one, but anyway, you found it. Another thing is that sometimes you just need to ask an expert, someone who's steeped in the culture. math.stackexchange.com is open to notation questions, but the guidance you can get in-person can be much more nuanced. I actually like running into new notation (supposing I'm not on a deadline trying to figure something out...), be it math or a programming language. You're trying to solve the puzzle of the purpose of the notation, what function does it serve, why someone ever thought this was a good idea. I've exposed myself to a lot of bits of obscure programming languages over the years, which makes it easier to guess what things might mean. Maybe one more thing: math notation tends to be invented for specific purposes, and maybe most of it doesn't carry over from subject to subject. Arithmetic, function application, summations, integrals, and set notation are fairly universal though.
tel 5y ago
This is an old yarn distinguishing sets and types, extrinsic and intrinsic, "run time" and "compile time". The idea of a runtime procedure `?- atom(_)` which determines `true.` or `false.` is fundamentally an extrinsic property, thus "set like". Intrinsically defined objects are defined through (possibly inductive) construction or (possibly coinductive) destruction rules. Typically a notion of set arises from having some larger universe of things and restricting them via predicates. The notion of types arises from having a system of building (co)inductive definitions and then utilizing that system. Sets are thus, in a sense, fundamentally based on a closed world (said universe) and types an open world (each new utilization of the rules system introduces a novel type).

tromp 5y ago

I think calling the type of natural numbers ℕ instead of Natural is causing the confusion. Students would be less tempted to write {1,2} ⊆ Natural as the right side looks like a type name rather than a value . Haskell helps to maintain the distinction by using capitals for type names and lower case for variable names. I would seem natural to write: naturals :: Set Natural naturals = {0,1..} {1,2} ⊆ naturals

mjburgess 5y ago
You're downvoted, but what you've said is basically the point-of and conclusion-to the article. `N` denotes a set and `Natural` denotes a type, and one cannot be eliminated to the other in all contexts of use.

klodolph 5y ago

Coming from the mathematics side of things, > In a math class, we typically tell students that ℕ is a set. I think the approach is a bit glib. There are some caveats—a student with more mathematical experience would think of ℕ as a set, or a type, or as objects in various categories. It’s also worth asking a student what 1∪2 is. Most people will look at that and just tilt their head, even though common foundations for mathematics treat 1 and 2 as sets. It turns out most people don’t want to work in foundations, and want to think of 1 and 2 as non-sets. The same applies in the other direction, upwards, when you think of ℕ as a type (even though it is also a set).

vkazanov 5y ago
My math is shallow at best but... 1∪2 would become just 2 with integers represented as sets in certain foundational theories, right?
- hansvm 5y ago
  Yes. One common definition is equivalent to each natural to being the set containing all preceding naturals. With that view 2={0,1} and 1={0}, so their union is just 2.
- Spivak 5y ago
  Yep! But notation depends a lot on the author to some extent. You will find people who treat 1U2 as {1}U{2} because it’s less annoying to write. It’s the same reason languages have an .add method on sets so you don’t have to write. s = s.union(set(s))
  - deleted 5y ago
    [deleted]
  - alisonkisk 5y ago
    who writes 1U2 instead of {1,2} ? When would {1}U{2} ever appear in ant context except for the first day of Intro to Set Theory?

k__ 5y ago

Half-OT: What's the reason rationals aren't used often in programming?

mjburgess 5y ago
You mean full-precision integer representations? A percentage is effectively this -- and floats are often multipliers on integers which are "holding the precision". However it isn't clear what standards sorts of arithmetical use cases storing two integers helps with (over, say, integer & float, etc.).
- k__ 5y ago
  I'm not sure either, that's why I asked. :D
  - mjburgess 5y ago
    I'm not an expert but, certainly, (1) limited memory on historical machines necessitated a small-width representation of a real number; (2) limited cpus meant simple operations needed to be applied to this small-width representation in one go. Ie., your CPU is just a system for taking bit patterns and producing new bit patterns: (0000 0000) -> (1010 0101). So you want each individual number to be of a size the processor can operate on in one pass. By using two integers you gain some capacity (ie., you can still overflow), but lose memory and compute performance.
hansvm 5y ago
Rationals are typically slower (gcd operations) and prone to memory explosion if the set of possible denominators isn't extremely nice. If approximate answers suffice then a scheme like floats or doubles is usually good enough. If approximate answers suffice and floats or doubles have undesirable properties (weird density distributions, ranges larger than what your application needs, ...) then it's easy to hack something together with a few _bounded_ integer types which has better properties for your specific needs. In most other practical applications some kind of a fixed-precision decimal suffices. It's a bit slower than floats and might have undesirable memory characteristics, but broad classes of real-world numbers which need to be represented exactly (like financial data) are nicely represented. Compared with those (and other) schemes, what advantages do rationals have? Chiefly, they admit an exact representation of any rational number. If you can mitigate the downsides (e.g., by not having many possible denominator prime factors) and need those benefits then rationals might be a good fit. One practical situation where I occasionally like to use rationals is in account data -- credits, currencies, .... It lends itself to forward compatibility when new features are desired (most often that the smallest atomic unit in a currency changes or that some niche system wants to offer transactions for 1/3 of a unit). Such changes usually have small, nice, compatible denominators, so you don't have unbounded memory issues. More importantly, all such operations are exact by definition without any extra work on my part (the biggest challenges are in display and formatting if your business admits those sorts of oddities).

mjburgess 5y ago

I think a clearer way of putting is this: types are not a mathematical notion. So "Bool" is not the same as "{On, Off}" nor "{0, 1}" nor "{Up, Down}" etc. We can reduce a type to a set of all constructible values; likewise we can reduce english to the "big infinity" of all possible sentences expressed in all possible universes. But english isnt this set. If one had this set, E, then you could reduce the question of whether a conversation (C) is valid english to set-membership, "is C in E?" but this misses whether the conversation is actually about anything. Likewise "me" can occur in an infinite number of sets (Person, RandomObjectsOnEarth, ...), but that "me in Person" is the "valid question" has nothing to do with "me in Person" -- and everything to do with the semantics of me/Person. "Person" is about "me". It is for this reason that values have "principal types" in programming languages; ie., the "set" which happens to be about the value. Insofar as mathematics is employed to model reality we have to introduce non-mathematical devices to constrain its application, types may be understood as the formal mechanism to do this.

Ericson2314 5y ago
Types absolutely are a mathematical notion. Formal systems like the calculus of construction and Martin Löf Type Theory are well studdied.
- mjburgess 5y ago
  That doesn't have much to do with my point. There is no mathematical encoding of natural world semantics: the sense in which "Person" and "MostIntelligentSpecies" are different cannot be expressed mathematically. (p in Person) obtains as does (p in MostIntelligentSpecies) but Person cannot be eliminated for MostIntelligentSpecies The article itself makes this point, but then tries to compromise with the mathematical reduction "to sets". It would be clearer just to state that this is a reduction rather than an elimination.

kuprel 5y ago

I don’t think you need the distinction for the natural numbers. Int32 is a type. The natural numbers are the set of positive integers that don’t overflow the int type used to express them.

Ericson2314 5y ago
This language is surely going to use bignums to avoid all that nonsense.

amw-zero 5y ago

It might help to consider the history of types and sets. Sets (and consequently modern math and logic) have not been around for as long as we might think. Maybe we had them in different forms, but sets as we know them today were born in 1874 in this paper: https://srjcstaff.santarosa.edu/~jomartin/IrratFiles/Cantors1874Paper.pdf https://srjcstaff.santarosa.edu/~jomartin/IrratFiles/Cantors.... Around 1901, Bertrand Russell discovered a paradox in this formulation of sets, so-called Russel's Paradox: https://en.wikipedia.org/wiki/Russell's_paradox https://en.wikipedia.org/wiki/Russell's_paradox. There are then many ways of dealing with this paradox. The most widely accepted way is to just reformulate the axioms, which was done with Zermelo-Frankel set theory: https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t.... When people use the word "mathematics" today, they generally implicitly mean that ZFC is being used. It's the most widely accepted mathematical foundation we have. Another path was proposed by Russell himself, and that is the notion of "type." By restricting the way in which certain operations and their arguments can be considered "valid," his own paradox can be avoided. So from the beginning, sets are about _collecting_, and types are about _restricting_.

ProfHewitt 5y ago
Types are about rigorously constructing mathematical abstractions from primitive types defined up to a unique isomorphism. In fact, types have become the primary foundation of Computer Science. Russell introduced the crucial concept of the order of a proposition to block his famous paradox as follows: Without orders on propositions, the paradoxical predicate I’mNotSelfApplicable (such that I’mNotSelfApplicable[I’mNotSelfApplicable]⇔¬I’mNotSelfApplicable[I’mNotSelfApplicable]) could be constructed using the following recursive definition: I’mNotSelfApplicable:Predicate<i>≡¬I’mNotSelfApplicable[I’mNotSelfApplicable] Since I’mNotSelfApplicable is a predicate variable in the definition, ¬I’mNotSelfApplicable[I’mNotSelfApplicable]:Predicate<i+1>. Consequently, I’mNotSelfApplicable:Predicate<i>⇒I’mNotSelfApplicable:Predicate<i+1> which is a contradiction meaning that I'mNotSelfApplicable does not exist. See video: https://www.youtube.com/watch?v=AJP1VL7shiI https://www.youtube.com/watch?v=AJP1VL7shiI
ProfHewitt 5y ago

specialist 5y ago

> Sets are characterized by the \in relation: we can ask which items are elements of a set and which are not. > Types, on the other hand, are characterized by how elements of the type are built: we can construct elements of a type (and deconstruct them) in certain ways specific to the type. Huh. So sets vs types are like folksonomies vs taxonomies? Neat. -- Tangent: > Disco> {1,2} ⊆ {1,2,3} Dumb question: How are you entering mathematically symbols? My hobby language recognizes both "!=" and "≠" as "not equal", and I use a font with ligatures to render them the same.

Ericson2314 5y ago

I feel like the author should just write call Set FiniteSet, and then a lot of confusion would go away! https://golem.ph.utexas.edu/category/2021/06/large_sets_1.html https://golem.ph.utexas.edu/category/2021/06/large_sets_1.ht... also, I highly recommend this series for anyone interested in sets outside of set theory.

raphlinus 5y ago

From the title, I thought it was going to be an extension of this discussion: https://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista https://mathoverflow.net/questions/376839/what-makes-depende... It's not, exactly, but some of the concepts do overlap. In particular, the idea of being able to write things in a "natural" mathematical style, then have them translate to an obsessively precise internal representation, is essentially the problem of "elaboration" as described in the top answer.

nolta 5y ago

Here's a nice video with a little more detail on the difference between intensional/extensional: https://www.youtube.com/watch?v=bNG53SA4n48 https://www.youtube.com/watch?v=bNG53SA4n48

piinbinary 5y ago

> So types are prior to sets: types provide a universe of values, constructed in orderly ways, that we can work with; only then can we start picking out certain values to place them in a set. What about uninhabited types? Or types where the constructor is not enough to determine the entire type? e.g. data MyType a b = MyConstructor { myField :: a }

tel 5y ago
What's the question? For uninhabited types there's a universe (empty), ways to construct (no ways), ways to work with (any way), and you can (tautologically) pick out values and put them in sets. Constructors aren't first order meaningful (except in higher-kinded calculi) but for any concrete types `A` and `B`, `MyType A B` is a type with a universe of values (isomorphic to `A`'s universe), ways to construct and use (again, isomorphic to `A`s), and we can place them in sets.
- piinbinary 5y ago
  I think I see now. So the author wasn't saying that construction of values is what defines the type. Rather it is a necessary step before you can start talking about sets of values. (And you can talk about a type without knowing how to construct it, so that makes types different from sets?)
  - tel 5y ago
    I think I see what the question is now. A type is defined by picking how its values are introduced and/or used. It doesn’t mean that those rules have to be actually productive. In fact there are many kinds of uninhabited types (the empty type being the simplest, but in languages with rich type systems there are many others).

didibus 5y ago

Isn't the confusion just that the Disco language uses the same symbol for its type that math uses for a very commonly known set? The symbol ℕ commonly refers to a set, but on Disco it suddenly refers to a type, it's not surprising that the confusion arises, especially since Disco also includes the concept of sets. > The set of natural numbers, denoted ℕ This is mostly how math refers to it, you can see both set and type here, the set of type natural numbers is denoted ℕ, thus "natural number" is the type and "ℕ" is the set. The type describes the rules for what is included in the set (in this case: all natural numbers), and the set is the list of all things that are included (each of the natural numbers themselves). The set of <type> is denoted <notation>

alisonkisk 5y ago
It gets even weirder when Brent (an expert in Haskell and math, both of which feature infinite sets!) expresses concern that he'll have to add infinite sets to his language, as though that wasn't totally obvious from the start.

chobytes 5y ago

Honestly philosophers getting ahold of set theory is probably one of the worst things to happen to it. I feel like it can be hard for people to take set theory seriously when the conversation about it is dominated by this kind of drivel. Basically this kind of dichotomy, and this image of set theory as the source of all truth in math or whatever... is essentially a myth made up by people peddling their own (new and improved!) foundations project as the source of all truth.

kazinator 5y ago

> keyword "ℕ" cannot be used as an identifier It looks to me like the guy has an outbreak of reservedkeyworditis the language that he's trying to handwave around with some talking point about sets versus type. But a syntax error of a reserved keyword being used in some phrase structure that calls for a a non-reserved identifier doesn't have anything to do with type semantics. The phrase structure of the A ⊆ B syntax could allow B to be certain keywords, such as ℕ, which is treated as a set in that context in the appropriate way (via an implicit conversion or whatever). We know what A ⊆ N means; what the programmer is asking. The requirement is not unclear. Moreover, it is doable. The question is do you do that, or not.

jdmichal 5y ago
That struck me too. My initial impression was to simply implement "Set s ⊆ Type t" as something like "∀i: sᵢ instanceof t"