Where do type systems come from? (2017)
blog.felipe.rs
blog.felipe.rs
This remains the first such system most people learn in elementary school. Historically such ideas arose along with measurements themselves and computations upon their results like comparison/subtraction/even taxation.
Yes, this is all (typically) manually checked and explicit metadata symbols are carried through calculations. I still think it's the primordial example that few mention in discussions like these.
Invention: I created that.
Discovery: I found that lying around.
Identification: I conceptualized a definition for that.
Also, in the everyday speech the word "literally" no longer means what it was meant to mean.
To be clear, I think Russell was an amazing mathematician and inventor. I also think that the history of types is way more rich and interesting than just saying that he invented the idea. To not mention at least Frege is to miss a lot.
Eg "4x + 4y = 40.4z"
x, y, and z here are units: x is meters, y is centimeters, and z is decimeters. You could do the same with types. The computer only knows the binary value, but the type assigns meaning to the value just like physical units do.
This must've been really obvious to a lot of people, but it only clicked just now for me. Thank you.
The constraints of their usage can be used to determine the type required of that data.
Proof: "constrained operations" and "notional objects" are very limited/somewhat concrete - "additive/comparative/conversion-y" and "measured things". Modern notions abstract both ideas.
This is, however, not unimportant (not to suggest I think @10000truths said so, exactly). In educational settings one usually wants to begin with the most familiar examples and then generalize. { Why, this probably even applies to greats like Russell. :-) } Further, in attributional settings, giving general names/notions to things is often less seminal than the things one is naming. (Both are often worthy of attention, but I tend to push back when "namers get all the credit".)
There is probably no single, famous big name like Russell to attach to the idea of units of measure/standard conversion/comparison. There may be a King of Olden Times who beheaded those who didn't follow his particular "system" when taxing crop growing areas or converting area to expected weights or volumes of grain/etc. ;-)
In some ways the very idea of "money" itself incorporates standardized exchange/comparison within it. Money itself is taken to be pre-historic [1], though there may have been a few original "coins"/tokens of money. Little tick marks in clay ledgers may have been the first and we can be fairly sure even before all the spice trade/wars that not all crops/goods were deemed equal/additive unconverted. On the contrary, money was useful specifically to help convert.
Following up on that ">1" requires a bit of explanation. Particle physics gets by with "natural" units where basically everything is rational powers of one base unit (MeV|energy|whatnot). SI units want like 7 or 8 or 9 base dimensions to avoid fractional powers (kind of a losing game since as soon as you have an equation with varying integer powers on either side fractional powers resurface).
Rayleigh may have used different English words than "abstract base class" or "type" (maybe "kind", "sort", etc.), but physicists definitely had "type ideas" more abstract and formally symbolic than the units of measure your grandma knew for recipes - before Russell said anything about them.
I am not sure Planck was the first to realize the "pick how many base dimensions you want" tricks - seems like Rayleigh or even earlier may have been, but in 1899 Planck published (before Russell's 1903 Doctrine of Types) a very abstract system of units such that major constants are 1.0 and dimensionless [1]. That level of conceptual abstraction (dimensionality - at least 1 more than just concrete vs abstract) also clearly predated Russell - but maybe only by a decade or two.
It seems to me uncontentious that physics/physicists were in a very abstract type theory headspace with regard to units of measure before Russell published that appendix. The only point of debate would be "Does it count or did Russell abstract it so much further as to count as a fundamentally different thing?" While I am no Russell biographer, it would be unsurprising to me if he was inspired either implicitly or even very explicitly by such "just earlier than him" happenings in physics like Planck units. These units famously "make physics look more like pure math" which does not seem like something Russell would have failed to notice.
As an "error catching mechanism" like types in programming languages, units function exactly the same way as programming types - just with the person as a compiler "doing their own checksum" to make sure they don't add apples & oranges. Calculation by hand was the predominant kind of computation at the time. So this is all coherent. At least "along the history of ideas arc" leading to programming language types, there may be great abstracters, but I doubt credit can be given to one person like TFA article tries to except maybe as an ambassador/evangelist/namer/maaaaybe first abstractor. (Not trying to suggest realizing the importance of something doesn't matter, but more make people realize how much this particular line of thought is almost as prehistoric as numbers themselves/quantification itself.)
Anyway, I find units for mass, speed, time, etc. useful in explaining types (and checksums) to non-programmers. Maybe you will, too.
A nitpick but those are also related by a simple scalar factor (the speed of light)
[1] https://frinklang.org/ [2] https://metacpan.org/pod/Language::Farnsworth
Towards the end he spoke about something in passing that's stayed with me.
Through out early/mid 20th century different mathematicians created their own theories of mechanised computation. Turing machine, Lambda calculus, SK combinators etc., However over they all turned out to be equivalent; for example Church-Turing thesis. So this leads one to believe strongly that mechanised computation is "discovered" rather than invented. Also it is a good indication that the computing theory is on a solid foundation.
However, when it comes to distributed and parallel computing theories have been proposed but no equivalence has been found (or at least proved). It's an active field which he hopes will result in a similarly solid foundation for the distributed computing. At the moment it seems to be on a shaky ground.
Is this really the case? It seems that game semantics ought to be able to model these concerns. The logical side of it would then be some sort of multi-modal logic.
"Finite of Sense and Infinite of Thought: A History of Computation, Logic and Algebra"
Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs!
Some programs in the Simply Typed Lambda Calculus [^1] have no type—i.e. diverging programs. Even some programs that may converge have no type. The Y Combinator, for instance, has no type because it would require an infinite type.
From the Wikipedia article under "General Observations":
Given the standard semantics, the simply typed lambda calculus is strongly normalizing: that is, well-typed terms always reduce to a value, i.e., a λ abstraction. This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term Ω = (λx.x x) (λx.x x) . Recursion can be added to the language by either having a special operator fixₐ of type (α → α) → α or adding general recursive types, though both eliminate strong normalization.
Since it is strongly normalising, it is decidable whether or not a simply typed lambda calculus program halts: in fact, it always halts. We can therefore conclude that the language is not Turing complete.
Writing a non-terminating program is like writing one of these self-contradictory logic statements: it has no proof of truth or falsehood. Thus, the fact that we can write programs to which we can assign some kind of type but that never terminate is a way of demonstrating the fact that there are theorems that are well-formed but have no truth assignment to them. (Gödel's Incompleteness Theorem)
[^1]: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus; see also https://softwarefoundations.cis.upenn.edu/current/plf-curren...
[^2]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
Thanks.
One can give a small step relation for a Turing machine and one could possibly come up for a type system for it, but generally one starts with the semantics for untyped lambda calculus.
Some of the more advanced type theory stuff unifies the notions of terms and types, meaning arbitrary computations can happen in type checking and so properties about types can involve properties about computation in general.
Nitpick, because those programs have no type they are not members of the Simply Typed Lambda Calculus but only of the underlying untyped calculus
I think the article has this a little wrong.
The theorem in programming terms I think simply means that there are some programs for which another program can't prove certain properties.
But in theory you can restrict yourself to writing programs that can be proven completely.
Even then though, you won't eliminate all bugs, and I think that's the part the article gets wrong.
Type system don't prevent bugs, they help you prove properties, but the programmer still needs to come up with all properties and edge cases themselves and set things up for the type system to prove those, and there's a lot of opportunity for the programmer to forget about a lot of properties or to have a bug in how they're trying to prove it.
Finally, there are only so much you can prove in a general way, in that there are only so many properties you can try to prove.
Just think about it, you can't go listing all possible inputs and asserting all possible outputs because as a programmer that would take way too long. So you try to come up with shortcuts, which will be properties, maybe you say alright so for even inputs I'd expect even outputs. Now maybe you use a type system to prove that. But you can still see how you've not proven that it returns the right output for every single input, just the property that even should return even. And that still leaves gaps for bugs.
But none of those have anything to do with Godel's incompleteness theorem, those exist even if you restrict yourself to programming only in a language for which type systems can fully operate in.
Disclaimer: I'm no expert in this though.
The type system will try to prove that a program will behave in some specific ways without needing to run the program. The "specific ways it behaves" is what I call "properties".
Property based testing will run the program and check as it is running that it behaves in some specific ways.
In the end, they both can be used to demonstrate that some properties of a program execution hold, but they go about it differently.
The type system will use logic over the code semantics and structure to assert that in all possible cases (combination of inputs) the property will hold.
The property based testing will use sampling to assert that in a lot of cases (combination of inputs), the property will hold.
Unless you can sample the entire input range in a property based test, you don't prove that it holds for all inputs, just for a large number of them. While type systems tend to prove for all inputs.
Also generally the type system will take less time to execute its reasoning over the code, than the property based test will take to run its sample set.
From a certain perspective, I disagree.
If I write a function, let's call it sort. It takes an array of integers and returns an array of integers. I call the function with an array and it so happens that the array returned isn't sorted.
Is there a bug?
I would argue there isn't because the function makes no such statement that the array returned should be sorted, or that it should be a permutation of the input array.
How could any programming language/type system "catch all the bugs" if no statements are made as to what constitutes a bug?
If I create a function in Idris and specify in the type signature that the returned array will be a permutation of the original and that it will be in increasing order, then yes Idris will catch all the bugs.
Types like "returns an array" or Java's checked exceptions are attempts at narrowing the possible behaviors from a function.
Basically, the proof is the spec, and a bug is defined as "not behaving as defined by the spec".
And assuming Idris is itself bug free in its language implementation and type checker implementation and is powerful enough to prove your given spec, then OP says your function is guaranteed bug free.
The difference is that he defines bug as:
> When the function behaves outside what Idris has proven.
While I think most people define a bug as:
> Doesn't do what it should have to provide the correct intended user behavior.
Using your definition of bug, take for example a function in an untyped language. Assuming a bug free implementation of the language, I can say that no matter what code I write, it will always be bug free, because the code will always do exactly what the code specifies, and the function made no statement to any particular behavior.
So if you define your "sort" to be a function that does what your Idris type specification defined it to do, yes your sort will be correct to it, assuming a bug free implementation of Idris and its type system, and that the type checker asserted it to be correct.
And yet, for the intended behavior to the users of the program and the objective it was meant to achieve it's very possible that your sort function doesn't work.
Or in other words take this Python code:
def sort(array):
return array
print(sort([2,1,3]))
[2,1,3]
I feel like that's the gist of your argument. You're saying: it behaved correctly to the extent that I have formally specified it, which in the case of Python I have not formally specified anything so all behavior are valid and correct.
But what good is that?
I think perhaps the challenge 'write a doubly linked list in Rust' is an example of this, but I am not sure.
I know this is true:
> given any type system / proof system for correctness, there will be well behaved programs that cannot be proven correct in the proof system
But I'm not sure if this is as well:
> nor can they be refactored to equivalent programs that can be proven correct
If so, then there will be some programs whose behavior simply cannot be proven by a type system. Though I wonder if for those programs there could be another type system that could prove it? So maybe with a combination of type systems it can still be achieved?
Either way, what I meant to say was that even for programs that can, the problem of "bugs in a program" has not been completely solved. Since there can be bugs in your proof, and there are often missing assertions in it as well, in that you'll generally prove a property of it, but not directly assert precisely what you expect of each and every inputs, and you might also simply forget to prove certain key properties.
You'll never understand because it's false. Godel theroem proves that theorems aren't enumerable. But they're still computably enumerable.
enumerable (in fact they are not even countable). See the following article:
https://papers.ssrn.com/abstract=3603021
In a foundational system, there are true propositions that
cannot be proved. For example, is true but unprovable that
an algorithm can enumerate the theorems of an order
abstracted from strings.
In that case, they're not theorems. Theorem are things that can be proved starting from axioms. And proofs are enumerable, except if the axioms are not enumerable.
It turns out that if you have that system in code written as s and then try to assert certain properties of it G, then it’s possible to design G such that s: G is so twisty and self-referential that it can’t be verified. Something to that effect: strong logics have a tough time speaking completely about themselves.
So that’s at least one property for one program that’s unprovable no matter how powerful our type system is.
But that’s so long range. Practically we can make type systems that let us prove massive amounts of things using judgements like e: B. The real issue is that it’s just very hard and expensive to make those systems practically eliminate even a small subset of bugs.
It is a well-known phenomenon that it can take surprisingly little to turn a computation system Turing complete; witness, for instance, C++'s accidentally-Turing-complete templates. So it can wiggle in without you even realizing it at design time. Or, if you're using a type system with sufficient power like dependent types, it is surprisingly easy to put together four or five recursive types that, on their own, are all perfectly computable, but together turn out to create something that is Turing complete. Write a program with a few hundred of these and Turing completeness is almost bound to sneak in somewhere.
See https://www.gwern.net/Turing-complete , and ponder applications to just-slightly-too-powerful type theories. Or https://github.com/Microsoft/TypeScript/issues/14833 .
that I’mUnprovable ⇔⊬I’mUnprovable) for proving inferential
undecidability of Russel’s foundational theory, which had the
type-restriction on orders of propositions to prevent
inconsistencies. I’mUnprovable cannot be constructed in
foundational theories because strong types prevent
construction of I’mUnprovable using the following recursive
definition (see Diagonal Lemma [Gödel 1931]):
I’mUnprovable:Proposition<i>≡⊬I’mUnprovable.
Note that (⊬I’mUnprovable):Proposition<i+1> in the right-hand side of the definition because
I’mUnprovable:Proposition<i> is a propositional variable in
the definition ⊬I’mUnprovable. Consequently,
I’mUnprovable:Proposition<i>⇒I’mUnprovable:Proposition<i+1>,
which is a contradiction.
I imagine it is a harder read but probably worth adding to my growing stack of books waiting to get read.
1. Bertrand Russell studied the "I am lying" paradox, which I always thought was nothing more than a clever meme. 2. Bertrand Russell is responsible for type theory 3. That type theory came out of his study of the paradox.
Think along the lines that you have some sentence Px which asserts that sentence Py is false. Now imagine a table where both the rows and columns are P0, P1, P2, .. populated with these sentences. The diagonal is where you have the self-reference: Pi asserting that Pi is false.
construction of paradoxes such as “The Liar” [Russell 1908].
Without orders on propositions, the “self-referential”
proposition I’mFalse (such that
I’mFalse⇔¬I’mFalse) could be constructed using the
following recursive definition:
I’mFalse:Proposition<i>≡¬I’mFalse. Since Ψ is a
propositional variable in the definition, ¬Ψ:Proposition <i+1>. Consequently,
I’mFalse:Proposition <i>⇒I’mFalse:Proposition<i+1>, which
is a contradiction.
For more information see the following:
Types have existed for a long time as mechanisms to provide classification and structure to formal (and even informal) languages. Even just before Russell, Frege (and many of his contemporaries) made a huge deal of the fine distinctions in type between propositions, expressions of truth, proofs, and their ilk.
What really made type theories blow up was the recognition that they corresponded with these very things: propositions, judgements, proofs. Mathematicians developed type theories as follow-on to Russell's (and others) work because they wanted to better describe what kinds of things counted as valid propositions and what kinds of corresponding proofs were formally admissible. They also were critically tied to conversations of syntax and semantics where mathematicians asked hard questions about why funny symbols on pages ought to have any sort of force of knowledge whatsoever.
So what made types rich was a recognition of the richness in the structure of first- and higher-order logics. The recognition that the power of the semi-formal language of proofs employed by working mathematicians required sophisticated study in order to describe and formalize. And that doing so required a distinction between the object of mathematical work, the proof, and the intent or semantics, the judgement.
Early PL type systems seem to have been convergent evolution. Here we were as computer scientists making and operating new formal languages and needing to describe certain properties of the syntax (but really: its ultimate semantic weight as it is operated by a machine) so that we could, e.g., make sure we used properly sized registers. Only as more sophisticated programming languages were developed that desired to simply the supposed programmer's task of working with abstraction did PL designers begin to converge toward, steal, and ultimately influence these languages of logic. The convergence, in my opinion, occurred because there truly are significant similarities in the kinds of mental processes accomplished by logicians and by programmers.
So where do type systems come from, really?
I think the good ones represent natural, parsimonious structuring of logic. We land on compositional systems because they're easy to reason about inductively. We land on sums and products because of archetypes from boolean logic, our belief about the "cheapness" of copying knowledge, and because of the natural urge to package together and make choices. We land on modules/quantifiers due to the value of abstraction in compartmentalizing and reusing ideas.
We can relax and challenge some of these assumptions to come up with new sorts of logic (and many PL designers and logicians make their bread in this way). We can also imagine totally different approaches to logic (like: state machine transition matrices) which are more challenging for us to work with using human minds or communicate to others using human speech. In this way, our type theories and logics are tailored to how humans most comfortably perceive the world.
Is there any field of study where the whole point is NOT to make concepts understandable by humans?
It could be interesting to let AI, for example, use theories that are easy to "understand" by computers instead, whatever that means.
Literary and art critique seems to be that field.
This is an often repeated claim, but I can’t shake the feeling that it’s an incorrectly drawn conclusion (of Gödel’s incompleteness theorems).
My understanding: It’s true that there are such “mathematical truths without proofs within axiomatic system X”, but they are unreachable by mathematicians and symbolic logic / machines alike. If a mathematical statement has no proof within ZFC we (usually) don’t call it a “truth”, regardless of if it is true or not.
Please correct me if I’m wrong.
I'm not sure I understand what this changes to the overall situation. Remember that a formal system also can't prove its own consistency, so you can't just ignore bits that you don't like and expect that it doesn't matter, it's possible that one of these "true but unprovable" propositions would actually render your system inconsistent, in which case it ought to be addressed.
I mean in the end Godel's own proof effectively relies on this: he builds a proposition using the rule of the system saying "this proposition has no proof" and at this point you either have to accept that the proposition is incorrect, but then your system is inconsistent (it can be used to derive falsehoods) or that it is correct but then the system is incomplete. So you may decide not to call it a truth but you also can't really call it a falsehood.
I would also wager that mathematicians generally prefer incomplete to inconsistent systems, if which case you have to accept that these unprovable propositions are indeed truths.
It's like the "does the set of all sets not containing themselves contain itself" paradox, you can't just ignore it as irrelevant because it puts into question your entire formal system.
Is that true? It seems to me that if a statement is unprovable, then even if it would in theory render your system inconsistent, there's no way that can actually happen.
Since, if you found any example of a chain of logic which leads to an inconsistency, that would count as a proof of the original statement. Which is unprovable, and as such can't have proofs.
See https://youtu.be/HeQX2HjkcNo?t=926 for instance which is (IMO) a fairly good explanation of the proof and why you end up with something both true and not provable.
Penrose's "Emperor's New Mind" also discusses this topic at length (within the context of whether human brains can be emulated). I wasn't convinced with his argument regarding AI but his overview of the problem of what's computable and what's not is rather good if a bit dense.
As far as I'm aware physics is computable, so I don't buy that one. :)
At most one might argue that there are high-level optimizations to be had, which can't be used because they're uncomputable. In which case is it really an optimization?
I don't really buy this theory, but the book is basically 80% "here's what we know" and 20% "here's what I conjecture" so it's still a worthwhile read IMO. It's worth noting that it's a book from the late 80's however, so it's a bit outdated in some parts (he didn't know that the universe's expansion was accelerating in particular, which renders his discussion of the curvature of the universe a bit obsolete).
See the following:
https://papers.ssrn.com/abstract=3603021
However, the proof is not convincing because the proof is
valid even if the system is inconsistent!
So in those limited systems we know there are things that are "true" or "false", but which can only be proven when we have a superset of the original tools available.
And by extension, maybe in our more complete type system there are things which can't be proven yet, but could perhaps be if there were better tools available?
Maybe another angle to look at it: one of the things which is difficult to prove is the halting problem. Maybe you can't prove that a given program will terminate. But you could run that program and watch it terminate, and then you'd know it does. In that sense there is a "true" answer, but one which couldn't have been proved in advance from type theory.
But I admit I only have a high-level understanding of these things. Type theory and axiomatic mathematics is something I'd like to know more about.
This depends on your formalism for logic. Intuitionist logic merges the meaning of "true" and "has a proof" but classical logic does not have any problem with having a thing be called "true" while also not being provable.
I am not sure about that - there are some "pathological" phenomena in classical math that are rejected (for the lack of proof) in constructive math.
Let me be more specific: Given a sentence that is true in every model of ZFC, you can prove that sentence. This is true because ZFC is a first-order theory, and this is a property of ANY first-order theory.
People that are pointing out incompleteness are talking about something else: They are talking about the fact that there are sentences S where neither S nor not S is provable. Additionally, there is a meta reason why S is believed to be true. For example, take S = encoding of "ZFC is consistent". BUT: This sentence S is true in some models of ZFC, and false in others, because otherwise the completeness of ZFC would make it provable / disprovable. So this boils down to the meta-truth being different from truth in a model.
Disclaimer: I just recently looked seriously into this stuff, because I was wondering about completeness of a logic I invented. So if the above is wrong, please somebody correct me!
Π₁-sentences (see arithmetical hierarchy) are closed formulas of the form, ∀x:ℕ. P(x), where P is some decidable predicate. i.e. all quantifiers in P are bounded. Thus for any given fixed value for x, say n, P(n) can be expanded out into conjunctions and disjunctions of atomic equalities and inequalities between closed arithmetic formula and those (in)equalities can in turn be decided (in principle) by calculation. Notice that 'x' is a formal variable in the language of first order logic, while we are using 'n' as a meta-variable denoting a term representing a numeral, e.g. 42.
Σ₁-sentences are closed formulas of the form, ∃x:ℕ. P(x), where P is again a decidable predicate.
Some basic first order logic yields that the negation of a Σ₁-sentence is logically equivalent to a Π₁-sentences and similarly the negation of a Π₁-sentence is logically equivalent to a Σ₁-sentence.
Important Fact: All true Σ₁-sentences are provable (in any sufficiently powerful system). Why? Suppose ∃x. P(x) is true. Then, there is some numeral 'n' where P(n) is true. Since P(n) is decidable we can prove P(n) when P(n) is true. And, by the rule of existential introduction, ∃x.P(x) is provable from P(n).
Now, let us consider some consistent system T (which is "sufficiently powerful"). For example, we can take T to be ZFC if you think ZFC is consistent. We can construct a Goedel-Rosser sentence for T, let's call this sentence G. G is a Π₁-sentence by construction, so we can put G in the form of ∀x:ℕ. P(x) for some decidable predicate P.
Now either G is true, (i.e. ∀x:ℕ. P(x) is true) or ¬G is true, (i.e. ∃x:ℕ. ¬P(x) is true). Suppose ¬G is true. Since ¬G is (equivalent to) a Σ₁-sentence then T proves ¬G. But by the Goedel-Rosser incompleteness theorem, this would imply that T is inconsistent, contradicting our assumption.
Thus it must be the case that G is true. However G is unprovable in T because, again by the Goedel-Rosser incompleteness theorem, if G were provable in T, then T would be inconsistent, contradicting our assumption.
Thus G is an example of a true sentence that isn't provable in T.
propositions because there are some expressions that do not
halt but it is unprovable that they do not halt.
While it is true that ZFC is model-complete in your sense (which holds for all first-order theories as you note), ZFC has many non-standard models that come with with non-standard sets of natural numbers within them. There are Σ₁-sentences that are false in models with standard sets of natural numbers but are true in models with non-standard sets of numbers.
Tarski's definition of truth, which I'm using for the definition of (in)completeness in my comment, excludes non-standard models because it requires, for example, for a Σ₁-sentence ∃x. P(x) to be considered true, that there actually exist a numeral (e.g. a closed term such as 42), 'n' where P(n) is true (recalling P is a decidable predicate the truth or falsity of P(n) can be determined (in principle) by calculation). When a Σ₁-sentence is only true in models with non-standard natural numbers, such numerals that witness P do not exist.
Some people argue that non-standard natural numbers are just as good as standard natural numbers, and you can try that argument I suppose. However, if I'm hiring someone do formal analysis of some algorithm and they "prove" that it is terminating by showing it terminates in some non-standard number of iterations, then I'm just going to fire them because such a result isn't helpful for reasoning about programs.
There is a material difference between standard and non-standard natural numbers. The standard natural numbers are formed in a natural way from the terms that make up the formal language of the first-order logic under consideration (i.e. the terms that are numerals), but the non-standard natural numbers cannot since they include "numbers" that have no associated numeral. Also note this way of characterizing the standard natural numbers won't work for characterizing "standard sets", because we do not expect all sets to come with canonical concrete terms denoting them, like we do expect for natural numbers.
I wouldn't fire the analyst in your example, by the way, because the fault would be mine: I should have just specified what complexity bound would be acceptable in a termination proof of the algorithm for it to be practical for my purposes.
I thought someone might say something like this. My counter is that if the analyst just used a normal proof system (i.e. one that doesn't assume false (in the standard model) axioms) then we could use Goedel's Dialectica [1] to mine the proof for some (probably crappy) complexity bound. That said, this is getting close to the edge of my knowledge on this subject.
[1] http://math.stanford.edu/~feferman/papers/dialectica.pdf
Related HN discussion: https://news.ycombinator.com/item?id=21898309
How is this (programming/practical) side of the word "type systems" related to formal/mathematical "type systems"?
I missed that part
The early history of type theory for programming languages comes from research into lambda calculus:
A type is a (possibly infinite) subset of all the possible values that can be provided as input to a program, or all the possible results a program can produce.
Type theory is about trying to figure out at compile time, if the inputs to a function are of a certain type (i.e. belong to a certain subset) what type the output will be (i.e. what subset of possible values the output will belong to).
It is not possible to figure this out in general because that would require solving the halting problem, so the art of designing type systems is choosing subsets of the data that allow you to prove useful things about programs at compile time so that you can find errors before the program runs, and eliminate run-time checks and hence make the programs run faster.
The reason people who like dynamically typed languages get frustrated with statically typed languages is that they value development speed more than they value run-time speed or avoiding of run-time errors, so they don't want to put in the extra effort needed to provide the compiler with the information it needs to do these compile-time derivations, or put up with the compiler complaining when it is unable to do them. They just want the program to run, and they're willing to pay for that with some inefficiency and run-time errors.
That's pretty much it.
On a more serious note: JS is in the background also keeping track of types, obviously.
I never understood that. For anything non-trivial, development speed is increased with types: you get auto-complete, safe refactorings, code navigation etc.
I mean, who would ever care about fringe cases when you can have continuous delivery instead?
But treating dates and surnames alike doesn't help robustness either.
Or separate types for metric distance and imperial distance might have prevented mars(?) lander losses. Or for sea levels referenced to Rotterdam or Le Havre might have prevented some bridges to have differing levels.
How hard is to write var v= SomeMethod() or var v = 5?
However, you still have to sometimes do some work to make your ideas fit the type system. Number of keystrokes isn't the only thing here.
People also seem to associate strong typing with compilers that bog down the write->run->debug loop, some of which used to have notoriously bad error messages, and things have changed because of JIT compilation (dart can even be both AOT compiled & JIT compiled), and also because modern compilers are so much better optimized and user friendly compared to just a decade ago (I mean, compare rustc error messages to GCC, lol). Compilers are doing a much better job today of helping decrease total debugging time.
FWIW this doesn't mean more advanced programmers necessarily move to strongly typed languages to increase their productivity. Instead, we are moving toward a progressively typed world (e.g typed python, typescript) to bring the benefits to users of dynamic languages as they begin to need them (without forcing them to use anything). And strongly typed languages are doing the opposite, e.g getting lots of dynamically typed features (e.g type inference in C++ with `auto`, initializer list syntax) which again, don't have to be used unless it helps with code readability and/or development velocity.
There are patterns or language features in dynamically typed languages which are very hard to translate to static types. I think Peter Norvig has some slides somewhere comparing OOP patterns to lisp, a more dynamic language, and that is the sort of thing I’m thinking of here. For language features, consider implementing an n-ary list map in Haskell vs Common Lisp. Or the typed equivalent of delimited continuations.
That said, research on the differences between languages is difficult and inconclusive. I would like to see more of it.
isn't that just flatMap?
> typed equivalent of delimited continuations
It's very clunky to do in Haskell, but conceptually they can be built on top of a monadic pipeline.
In practice, the only case where statically typed languages force you to write different code is if:
(a) the type system is too restrictive and dumb (no generics, awkward function types, etc).
(b) you're trying to write a function that effectively returns monster types like Union[None, int, str, List[str]], which is common in dynamic languages but it's something you're not really supposed to do.
I agree with your broader point, that static types can in fact slow down development, but I have a different model.
Types are kind of two things at the same time: tags to tell the compiler how many bytes need to be allocated, and partial proofs of correctness of the program. The key observation of dynamic languages is that in most cases we can do without the first part: the runtime can handle that in the same way it handles memory management. I believe one of the mistakes of the original wave of dynamic typing proponents is that they kind of threw away the baby with the bathwater: the correctness part is important, and at least a form of optional typing should be provided.
The real trouble is that it's not easy to conjure type systems that are both expressive and ergonomic to use for the average developer. Sufficiently advanced type systems are indistinguishable from math riddles, and in a working environment that can be frustrating.
There’s no way to bootstrap that process for them: you’re asking for the output as an input.
I think TypeScript has one of the best compromises.
Also, I think people are understating how easy dynamic typing makes substitutions — everyone else is writing their class twice (interface + class) just to get the same flexibility.
Is there any kind of programming task where it's too much to ask the programmer to know the type of the function he's writing?
The only place I can imagine types being a burden is in a REPL (it's just boring to write them every time), but even then optional types like Python and TS are an unequivocal win (you're presumably going to move your code out of the notebook/repl and into proper source files at some point).
> understating how easy dynamic typing makes substitutions
Yeah so easy they're easily wrong. One of the worst problems of dynamic languages is that they don't have the concept of an interface, which makes it harder and not easier to write generic code.
> everyone else is writing their class twice (interface + class)
That's caveman Java right there. Interfaces with defaults (Java, Kotlin, even C# has something similar IIRC) can easily emulate dynamic patterns like mixins while preserving type safety and without the diamond problem.
I think the problem is that lots of type systems are inherently limited, so there may be patterns that you want to express that your type system simply can't, or that you have to write tons of boilerplate code to express. In languages like Java or C# that don't have Sum types, this can be as basic as "this value is a String or Integer". You have to write a class hierarchy to express this in Java. In JavaScript you simply accept a parameter and branch on `typeof value`. More powerful type systems allow you to express more patterns, but you still have to type them out. This can be done, but if you're doing exploratory work an unknown dataset then this can make the work much slower. And there be may little benefit.
People keep forgetting Basic is dynamic and .NET was designed to support it as well, additionally it got improved with DLR classes to support IronPython and IronRuby projects.
So you can co type crazy in C#, F# and C++/CLI, or just get hold of those dynamic features.
It can be a useful pattern when designing interface boundaries across modules (e.g. ABI's, data interchange formats etc.) to allow for the required flexibility in a limited context where the overhead isn't going to matter all that much.
Is it one of those in-between systems, just more on the dynamic side?
The point I'm getting at is that using interfaces lets you make guarantees about what methods the objects must have. I'm not really picky about what specific technical means are being used to enforce those, but passing an object of the wrong type to a method is an entirely avoidable category of errors, and I prefer them to be flagged by the compiler/interpreter/runtime/tsc/mypy/whatever as soon as possible.
IME well designed interfaces are even more important than well designed classes, and dynamic languages unfortunately make it harder to enforce interfaces. It's not by chance that the first thing Typescript did was to introduce interfaces.
In Common Lisp the lambda-list looks something like:
(MAPCAR func list &rest lists)
(defun mapcar1 (f list &aux r)
(tagbody
g
(when list
(push (funcall f (pop list)) r)
(go g))
(nreverse r)))
(defun every (pred list)
(dolist (x list)
(unless (funcall pred x)
(return nil)))
t)
(defun mapcar (f list &rest lists)
(prog ((lists (cons list lists))
r)
loop
(when (every #'consp lists)
(push (apply f (mapcar1 #'car lists) r)
(setf lists (mapcar1 #'cdr lists))
(go loop))
(nreverse r)))
type ('ftype,'output) t =
| [] : ('a,'a) t
| (::) : 'a list * ('b,'c) t -> ('a -> 'b,'c) t
val mapn : f:'f -> ('f,'x) t -> 'x
One nice quality of dynamic languages is that you get very useful objects like lists or python/JavaScript style ‘dicts’ and lots of standard library functions to operate on them. You can implement them in a statically typed language to some extent but they are much less versatile and less first class. It means you often need to write different functions that do basically the same thing because they use different record or tulle types as input. I don’t think any mainstream languages are very close to static typing with structural subtyping.
There's the key phrase. There's plenty of people that can whip up a POC or MVP in an afternoon of hacking or a week of fiddling, but going from that to something that can safely handle millions of users and hundreds of developer contributions needs types and other assurances. If it fits in a developer or a team's heads, then it's just fine - that's how I did my first major JS application, just Knowing what fields my objects have and what types they are expected to have. But that doesn't scale, people move on, gaps exist in tests, etc etc etc.
Also, development speed can go down if you have to show your compiler that data conforms to a given type. Certainly for one-offs where the user writes and maintains their own program, that can sometimes/often get you something doing something useful for the inputs you have _now_ fairly rapidly.
There might be a hidden assumption of stead-state in there. In the initial ramp-up when people are learning a language, or learning to code to start with, types will slow down development because there is one more system to learn and use correctly.
It is notable that if your code is going to be a bug ridden mess regardless of language features, language features that reduce the number of bugs (like type systems) are a hindrance.
- Type systems of varying complexity, where you sometimes have to abuse the language in complicated ways to express constraints you want;
- Pushing complex checks to runtime, even though they should be - in principle - computable ahead of time. Or, the compiler should be able to tell you ahead of time what you need to do to ensure an assertion never fails.
- External tools like proof checkers.
I guess having types as names of constraints is useful. Then, what I'm looking for is a better "satisfies" from Common Lisp - one that would be guaranteed to run mostly arbitrary code at compile time.
Well, programming language people tend to call any kind of property you can statically check a 'type'.
Basically a lot of properties that you probably can think of that could be checked for but aren't expressible in Java types system can still be expressed using types in another system. Therefore if you want something more powerful than the types your using, use more powerful types! It turns out that we do not really need more to reach the limits of what we can check for automatically.
It turns out that sets are a very general concept. Anything you can say about a program can be expressed in terms of sets of states that program goes through as it runs. So there is nothing you can say about a program that cannot be expressed, at least in principle, in terms of sets.
The problem is that sets are themselves Turing-complete. If you can add a member to a set, and remove a member from a set, and test if a set is empty, that is a Turing-complete set of primitives. So if you allow yourself to have a type system that is so powerful as to be Turing-complete you haven't gained anything because now the problem of debugging problems in your type system is equivalent to that of debugging problems in your programming language.
So in order to be useful, a type system has to be constrained in some way that prevents it from being Turing-complete. Choosing those constraints is the art of designing type systems. No matter what you do, it will necessarily be the case that if your type system is going to be useful at all there will be certain things it cannot express. The trick is to insure that those things are things you don't actually care about very much or, alternatively, that your language allows you to "break out" of the constraints of the type system when they become too burdensome and tell the compiler to just do what you tell it despite the fact that it can't prove there won't be errors.
I wonder if this is true of a program written in a purely functional language.
What foundation would you rather have?
And what would it do better / how would it be less "detrimental" to formal mathematics?
But what is "this"? I think the only criticism of existing theorem provers at https://practal.com is that Coq uses coercions rather than subtyping. Is there a practical example where Coq just doesn't have a good equivalent for what subtypes can do?
or they don't make the kinds of errors that static typing helps defend against so for them it is an impediment.
- The art of designing type systems you describe is also heavily constrained by the practical limits of language. We could easily add more and more 'types' to a programming environment to cover more use cases, but at some point it makes the 'language' difficult when there's too many. Which is why turn to different languages for different uses.
- There's a bunch of different categories of types. This thread is full of discussion of functions and lambda calculus which is important as function types are some of the most complex, especially for 'trying to figure out at compile time' as you describe. But there's also common types like a 1 byte char, 4 byte unsigned int, or memory pointer that are more based on hardware and established standards, as well as user defined types and 'classes' which bring their own practical complexity and approaches.
2. Modeling the domain with types, making erroneous states unrepresentable is helpful
3. Carefully chosen types help with communicating intent
For example TypeScript has the "any" and the "unknown" types. Both encompass the same set of values (any possible value which can be represented in the language), but the allowed operations are different.
C# has something similar with "object" and "dynamic".
For a static type system it makes more sense to think of a type as a set of supported operations rather than a set of values.
You could probably define terms such that of these, only `Void` is a "type" - for example, it's the only one that you can use directly as function inputs or outputs. (i.e. you can write a function `Void -> Int` but not a function `Maybe -> Int`.) I think that would be nonstandard, but maybe reasonable to do. But then when you explain what a "type" is you've only explained a subset of what "type theorists" talk about, which includes the others.
But to support my "nonstandard" claim:
* https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compil... mentions "Types (possibly of higher kind); e.g. [Int], Maybe"
* https://limperg.de/ghc-extensions/#polykinds talks about "types of different kinds", using Int and Monad as examples.
* https://en.wikipedia.org/wiki/Kind_%28type_theory%29 says "the type [] (list) is a type constructor". It uses the terms "data type" and "proper type" for what I think you simply want to call "type".
It's also possible usage is just inconsistent on the subject. (Evidence for this: that second link calls constraints "type-like things", when they're just types according to me.) But my sense is that usually, people engaging seriously with type theory or advanced Haskell would call Maybe and Monad types.
(You're of course right that Maybe is a type constructor and Monad is a typeclass, but that doesn't mean they aren't also types.)
For a start it's a discriminated union (a sum type), its set of values is:
a + 1
`Maybe a` is a type-lambda abstraction (still a type)
`Maybe Int` is a type-application, passing Int to the `Maybe a` type-lambda as an argument, to get a `Maybe Int` in return (still a type).
I don't know what you mean by this - lambdas are values not types. You could argue the type of the Maybe type constructor is Type -> Type but there is no Type type in Haskell so Maybe is not a 'type' in the Haskell type system in the way e.g. String is. The separation of types and values is AFAIK the defining characteristic of non-dependent type systems, which Haskell is (for now).
I think they meant "`Maybe` is a type-lambda abstraction", meaning roughly "a type-level function", which seems true to me. I don't think they meant to say that `Maybe` is a type in the same way String is. (I'd agree it's not, though I'd still call it a type.)
> there is no Type type in Haskell
Incidentally there is[1], and it even has kind `Type` just like `String` does. So you can ask "what is the kind of `Maybe Type`" (it's `Type`) where you can't ask "what is the kind of `Maybe Maybe`" (`Maybe` has kind `Type -> Type` so this is a kind error).
[1]: https://hackage.haskell.org/package/base-4.15.0.0/docs/Data-...
It really doesn't. 'any', 'unknown', 'object', and 'dynamic' are all 'top' in type systems (the type that is the super-type of all other types), they hold the set of all values. The fact a language assigns additional semantics based on their name is just sugar over the underlying type system, the type-system can live quite happily without names.
But even then, you could consider the name of a type a 'discriminating tag', like in discriminated unions. So, something like:
type Top = Any a
| Unknown a
| Object a
| Dynamic a
> The same type, but with different states depending on the semantics of the language.
This is just playing games with definitions. What you call "state" is a type in the type system of the programming language.
Yeah, it's pretty much like those people taking a reasonable, standard car, and removing the motor to add horses instead. Who in their right mind would do that? Turns out, plenty of people in the past just did that for no reason at all.
"Linear type systems are the internal language of closed symmetric monoidal categories, much in the same way that simply typed lambda calculus is the language of Cartesian closed categories. More precisely, one may construct functors between the category of linear type systems and the category of closed symmetric monoidal categories."
That is what I was referring to when I used the word "impenetrable". I was talking about pedagogy, not substance.
The impression that these concepts were inherently simple in the first place is the consequence of the observer standing on the shoulders of popularizers, themselves standing on the shoulders of theorists. To think that we had simple things that were made complicated essentially reverts the timeline.
Now, I don't discount the possibility that I might be missing something, maybe even something very cool and powerful. But I have been coding for over 40 years and I have a Ph.D. in computer science, so I'm not a complete idiot. But so far no one has been able to explain to me what that thing is that I'm missing in terms that I can understand. That is what I am complaining about.
I'm not sure which programming language you're referring to, but as you may see in the video I posted elsewhere in this thread, the notion of computer algorithms predate transistors by a few centuries, and the notion of computability, the groundwork for types, predates transistors by a few decades.
The first people that had a stab at it were logicians, and they were used to some abstractions that probably felt as natural as code to you, while the concept of compilation wouldn't exist for another half-century.
> I have been coding for over 40 years and I have a Ph.D. in computer science, so I'm not a complete idiot. But so far no one has been able to explain to me what that thing is that I'm missing in terms that I can understand. That is what I am complaining about.
If you're looking for scientists to popularize breaking research work, you're probably barking up the wrong tree. You'll find plenty of accessible work explaining modern type systems (e.g. f# for fun and profit), it's just that this work didn't exist when scientists set about to solve this problem.
> The first people that had a stab at it were logicians
Yes, I know. The original article pointed that out.
> it's just that this work didn't exist when scientists set about to solve this problem.
Yes, I know that too. But it exists today and so today there isn't any reason not to avail onesself of that knowledge when engaging in pedagogy.
I have no idea what we are actually arguing about here. All my original comment was intended as was to echo the sentiment expressed in the first sentence of the original article, that's all.
That's pretty much it.
And once you have that kind of functionality, you need more than just what you described.
(And, no, Go's approach doesn't cut it. Their 'generic' sorting interface only works for in-place algorithms.)
Those templates can be used to do something like generics, but they are also basically duck typing at compile time.
In Haskell terms, C++'s generics are like typeclass-instances without typeclasses themselves. (I think in Java terms they would be similar to not providing interfaces. But I don't know enough about Java to see whether that's actually true.)
> A type is a (possibly infinite) subset of all the possible values that can be provided as input to a program, or all the possible results a program can produce.
What you are describing are 'extrinsic types. There are also 'intrinsic types'.
Btw, types don't have to be sets at all. (Nor are they all isomorphic to sets. Some types describe things bigger than sets.)
Intrinsic definition:
"Birds are a group of warm-blooded vertebrates constituting the class Aves, characterised by feathers, toothless beaked jaws, the laying of hard-shelled eggs, a high metabolic rate, a four-chambered heart, and a strong yet lightweight skeleton."
Extrinsic definition:
"Birds are the set made up of: Sparrows, Pigeons, Robins, Hummingbirds, Hawks, Eagles, Parrots, Penguins, Ducks, etc..."
Though not sure whether Wikipedia does a better job:
> An intrinsic/Church-style semantics only assigns meaning to well-typed terms, or more precisely, assigns meaning directly to typing derivations. This has the effect that terms differing only by type annotations can nonetheless be assigned different meanings. [...] In contrast, an extrinsic/Curry-style semantics assigns meaning to terms regardless of typing, as they would be interpreted in an untyped language.
> The distinction between intrinsic and extrinsic semantics is sometimes associated with the presence or absence of annotations on lambda abstractions, but strictly speaking this usage is imprecise. It is possible to define a Curry-style semantics on annotated terms simply by ignoring the types (i.e., through type erasure), as it is possible to give a Church-style semantics on unannotated terms when the types can be deduced from context (i.e., through type inference). The essential difference between intrinsic and extrinsic approaches is just whether the typing rules are viewed as defining the language, or as a formalism for verifying properties of a more primitive underlying language. Most of the different semantic interpretations discussed below can be seen through either a Church or Curry perspective.
I've often seen this reductionist simplification of "type" but I don't think it's accurate because of the emphasis on values without mentioning the rules for those values.
The extra power of "types" comes from behaviors of values.
E.g. in mathematics example, a Complex Number when only seen as "values" looks like a 2-dimensional vector. Therefore, r^2 and complex plane can appear as the same type but they are not. Complex Numbers have extra behavior rules e.g. multiplication that plain r^2 does not. (https://math.stackexchange.com/questions/444475/whats-the-di...)
For a less mathy example, would be a typical DateTime type. Yes, some underlying implementation may use a 64bit integer as an offset from an epoch but a rich datetime type would also have "behavior rules" such as adding 1 day to Saturday makes it wrap around back to Sunday because of modular arithmetic. It's the built-in behavior rules that make using a DateTime type less error-prone than manipulating raw 64bit integers.
Personal anecdote: I initially learned an incomplete and misleading idea about "types" from K&R's "The C Programming Language". From that book, I only thought of "types" as different data widths (or magnitudes). An "int" held 16bits and a "long" held 32 bits, etc. And C keywords like "typedef" futher adds to the misunderstanding of "types" because typedef is just an name alias instead of defining behavior rules.
> rich datetime type would also have "behavior rules" such as adding 1 day to Saturday makes it wrap around back to Sunday because of modular arithmetic.
Conceptually, it's a overloaded method, that's a function, again, with syntactic sugar. Functions are defined from one set to other. The fact that we use same names or symbols doesn't change that types, for all simple purposes, correspond to sets in math.
But regardless of ITT vs. ETT, the point of type theory is that proofs are mathematical objects. That's where the real power comes from and this is the power unityped languages lack.
I suspect that this false belief that dynamically-checked language afficionados have, of types being sets, is responsible for their disdain for statically-typed languages. If you think that types are sets, it's easy to miss what they can do.
As a gentle introduction to modern type theory I would recommend https://arxiv.org/abs/1601.05035.
Maybe this is a dated perspective now, since more modern languages like Julia are aiming for dynamic types with good run-time speed, or like nim which aim to make statically typed languages as easy to use as dynamic ones.
Sure, sure. Nothing is perfect. It could use stronger REPLs, one has to workaround compiler limitations occasionally, and I seem to be the only one telling people to use the TinyC/tcc backend as a default in their $HOME/.config/nim/nim.cfg or $HOME/.config/nim/config.nims for sub-second compile-times (part of "fluid"). It is very good as-is and deserves more attention than it gets.
That's an argument for dynamic types, not against static types, and I think languages with both (TypeScript, ObjC) are a sweet spot.
Mathematicians chose to sacrifice readability in favor of terseness; they invented a large number of abstractions, often with only tiny differences between them. Also, descriptions of concepts tend to focus on the wrong characteristics... Maths would be far more accessible if mathematicians described everything in plain English and reused abstractions to describe similar concepts instead of inventing entirely new words. It's possible, they just don't want to do this because it wouldn't make them sound as clever.
As a developer, I can explain a blockchain as:
1. A decentralized ledger which relies on an asymmetric signature scheme such as EdDSA, zero-knowledge proofs or other mechanism to authenticate on-chain messages. A blockchain network forms either a structured (deterministic) or unstructured (stochastic) P2P mesh, ideally with each node having a partial view and propagating messages through the network via a gossip protocol. Blockchain nodes adhere to a consensus mechanism such as PoW or PoS (or variants) to provide byzantine fault tolerance and resilience to forks given certain finality conditions.
Or:
2. A ledger which is replicated across multiple nodes/computers which are connected together. The blockchain is usually a ledger of accounts involving financial transactions. The authenticity of each transaction can be independently verified by anyone by checking that a digital signature on any transaction corresponds to the account which claims to have sent the transaction - This is possible because each account is associated with a 'public key' which anyone can see and which can be used to verify that a signature was generated by the sender since only the sender could have known the 'private key' (secret) which was used to generate this specific signature given this specific transaction and this specific public key.
Mathematicians absolutely do write accessibly from time to time, but when they do so you have to be fortunate enough to be in the audience. Often these are aimed at only the most general of audiences and thus are pretty sparse in detail.
Are you sure about that?
Take Kepler's Laws of Planetary Motion as an explanation of orbital mechanics and try and do anything with just these plaintext definitions (courtesy of Wikipedia):
The three laws state that:
1. The orbit of a planet is an ellipse with the Sun at one of the two foci.
2. A line segment joining a planet and the Sun sweeps out equal areas during equal intervals of time.
3. The square of a planet's orbital period is proportional to the cube of the length of the semi-major axis of its orbit.
Or take this formula, converted into plain English:
The distance of a planet from the sun is proportional to the semi-latus rectum and one more than the product of the eccentricity of the orbit and the cosine of the angle between the planet's current position and its nearest approach.
The latus rectum is the chord parallel to the directrix and passing through a focus; its half-length is the semi-latus rectum (ℓ).
That idea of "solve for θ" is "just" a basic application of algebra. An act that would become impossible to do with any kind of reasonable efficiency and confidence about correctness without something like our current mathematical notation, and plain English (very anglocentric, guess we don't want anyone outside the anglosphere to participate) would be a poor alternate.