4 ms·
Not much related to the paper, but I'm inspired to emphasise the phrase "quantified over" which I personally find very useful in day-to-day thinking and somethi
by mjburgess 4y ago
Not much related to the paper, but I'm inspired to emphasise the phrase "quantified over" which I personally find very useful in day-to-day thinking and something strangely absent from the programming community at large.
To "quantify over" something is, in effect, to treat it as a variable whose value will range over some set. As a phrase, it makes clear what is a variable in your description.
Generics are just quantifiers (forall T in Types, c: Box<T> = new Box()).
- auggierose 4y agoThey are absent because quantifying over something is a model-theoretic notion (that is where the set is coming from), while programming language researchers often prefer type theory and follow a proof-theoretic approach. Personally, I like proofs, but I think they go better with a model-theoretic approach :-)
- eynsham 4y ago> To "quantify over" something is, in effect, to treat it as a variable whose value will range over some set. As a phrase, it makes clear what is a variable in your description. That’s a rather non-trivial claim: see e.g. Williamson, ‘Everything’, Philosophical Perspectives, 2003, §§ IV and IX.
- thrown_22 4y agoEverything in the real world is finite which is equivalent to an arbitrary large but strictly finite number of conjunction for "for all" and a the same with distinctions for "there exists".
- eynsham 4y agoYes, in a finite system Russelian paradoxes don’t arise as easily (although see Ian Rumfitt and Timothy Williamson, once again, ‘Logic and Existence’, Proceedings of the Aristotelian Society, 1999 for one interesting view that infinitude is logically necessary.)