137 lines
35 KiB
HTML
137 lines
35 KiB
HTML
|
<div><div>
|
|||
|
|
184
|
|||
|
|
</div><p>
|
|||
|
|
I apologize for writing a lengthy answer, but I get the feeling the discussions about foundations for formalized mathematics are often hindered by lack of information.
|
|||
|
|
</p><p>
|
|||
|
|
I have used proof assistants for a while now, and also worked on their design and implementation. While I will be quick to tell jokes about set theory, I am bitterly aware of the shortcomings of type theory, very likely more so than the typical set theorist. (Ha, ha, "typical set theorist"!) If anyone can show me how to improve proof assistants with set theory, I will be absolutely deligthed! But it is not enough to just have good ideas – you need to test them in practice on large projects, as many phenomena related to formalized mathematics only appear once we reach a certain level of complexity.
|
|||
|
|
</p><h3>
|
|||
|
|
The components of a proof assistant
|
|||
|
|
</h3><p>
|
|||
|
|
The architecture of modern proof assistants is the result of several decades of experimentation, development and practical experience. A proof assistant incorporates not one, but several formal systems.
|
|||
|
|
</p><p>
|
|||
|
|
The central component of a proof assistant is the <strong>kernel</strong>, which validates every inference step and makes sure that proofs are correct. It does so by implementing a formal system <span>$F$</span> (the <strong>foundation</strong>) which is expressive enough to allow formalization of a large amount of mathematics, but also simple enough to allow an efficient and correct implementation.
|
|||
|
|
</p><p>
|
|||
|
|
The foundational system implemented in the kernel is too rudimentary to be directly usable for sophisticated mathematics. Instead, the user writes their input in a more expressive formal language <span>$V$</span> (the <strong>vernacular</strong>) that is designed to be practical and useful. Typically <span>$V$</span> is quite complex so that it can accommodate various notational conventions and other accepted forms of mathematical expression. A second component of the proof assistant, the <strong>elaborator</strong>, translates <span>$V$</span> to <span>$F$</span> and passes the translations to the kernel for verification.
|
|||
|
|
</p><p>
|
|||
|
|
A proof assistant may incorporate a third formal language <span>$M$</span> (the <strong>meta-language</strong>), which is used to implement proof search, decision procedures, and other automation techniques. Because the purpose of <span>$M$</span> is to implement algorithms, it typically resembles a programming language. The distinction between <span>$M$</span> and <span>$V$</span> may not be very sharp, and sometimes they are combined into a single formalism. From mathematical point of view, <span>$M$</span> is less interesting than <span>$F$</span> and <span>$V$</span>, so we shall ignore it.
|
|||
|
|
</p><h3>
|
|||
|
|
Suitability of foundation <span>$F$</span>
|
|||
|
|
</h3><p>
|
|||
|
|
The correctness of the entire system depends on the correctness of the kernel. A bug in the kernel allows invalid proofs to be accepted, whereas a bug in any other component is just an annoyance. Therefore, the foundation <span>$F$</span> should be simple so that we can implement it reliably. It should not be so exotic that logicians cannot tell how it relates to the accepted foundations of mathematics. Computers are fast, so it does not matter (too much) if the translation from <span>$V$</span> to <span>$F$</span> creates verbose statements. Also, <span>$F$</span> need not be directly usable by humans.
|
|||
|
|
</p><p>
|
|||
|
|
A suitable variant of set theory or type theory fits these criteria. Indeed Mizar is based on set theory, while HOL, Lean, Coq, and Agda use type theory in the kernel. Since both set theory and type theory are mathematically very well understood, and more or less equally expressive, the choice will hinge on technical criteria, such as availability and efficiency of proof-checking algorithms.
|
|||
|
|
</p><h3>
|
|||
|
|
Suitability of vernacular <span>$V$</span>
|
|||
|
|
</h3><p>
|
|||
|
|
A much more interesting question is what makes the vernacular <span>$V$</span> suitable.
|
|||
|
|
</p><p>
|
|||
|
|
For the vernacular to be useful, it has to reflect mathematical practice as much as possible. It should allow expression of mathematical ideas and concepts directly in familiar terms, and without unnecessary formalistic hassle. On the other hand, <span>$V$</span> should be a formal language so that the elaborator can translate it to the foundation <span>$F$</span>.
|
|||
|
|
</p><p>
|
|||
|
|
To learn more about what makes <span>$V$</span> good, we need to carefully observe how mathematicians <em>actually</em> write mathematics. They produce <a href="http://hott.github.io/HoTT/dependencies/HoTTCore.svg" rel="noreferrer">complex webs</a> of definitions, theorems, and constructions, therefore <span>$V$</span> should support <em>management</em> of large collections of formalized mathematics. In this regards we can learn a great deal by looking at how programmers organize software. For instance, saying that a body of mathematics is "just a series of definitions, theorems and proofs" is a naive idealization that works in certain contexts, but certainly not in practical formalization of mathematics.
|
|||
|
|
</p><p>
|
|||
|
|
Mathematicians omit a great deal of information in their writings, and are quite willing to sacrifice formal correctness for succinctness. The reader is expected to fill in the missing details, and to rectify the imprecisions. The proof assistant is expected to do the same. To illustrate this point, consider the following snippet of mathematical text:
|
|||
|
|
</p><blockquote><p>
|
|||
|
|
Let <span>$U$</span> and <span>$V$</span> be vector spaces and <span>$f : U \to V$</span> a linear map. Then <span>$f(2 \cdot x + y) = 2 \cdot f(x) + f(y)$</span> for all <span>$x$</span> and <span>$y$</span>.
|
|||
|
|
</p></blockquote><p>
|
|||
|
|
Did you understand it? Of course. But you might be quite surprised to learn how much guesswork and correction your brain carried out:
|
|||
|
|
</p><ul><li><p>
|
|||
|
|
The field of scalars is not specified, but this does not prevent you from understanding the text. You simply assumed that there is some underlying field of scalars <span>$K$</span>. You might find out more about <span>$K$</span> in subsequent text. (<span>$K$</span> is an <a href="https://coq.inria.fr/refman/language/extensions/evars.html" rel="noreferrer">existential variable</a>.)
|
|||
|
|
</p></li><li><p>
|
|||
|
|
Strictly speaking "<span>$f : U \to V$</span>" does not make sense because <span>$U$</span> and <span>$V$</span> are not sets, but structures <span>$U = (|U|, 0_U, {+}_U, {-}_U, {\cdot}_U)$</span> and <span>$V = (|V|, 0_V, {+}_V, {-}_V, {\cdot}_V)$</span>. Of course, you correctly surmised that <span>$f$</span> is a map between the <em>carriers</em>, i.e., <span>$f : |U| \to |V|$</span>. (You inserted an <a href="https://coq.inria.fr/distrib/current/refman/addendum/implicit-coercions.html" rel="noreferrer">implicit coercion</a> from a vector space to its carrier.)
|
|||
|
|
</p></li><li><p>
|
|||
|
|
What do <span>$x$</span> and <span>$y$</span> range over? For <span>$f(x)$</span> and <span>$f(y)$</span> to make sense, it must be the case that <span>$x \in |U|$</span> and <span>$y \in |U|$</span>. (You <a href="https://en.wikipedia.org/wiki/Type_inference" rel="noreferrer">inferred</a> the domain of <span>$x$</span> and <span>$y$</span>.)
|
|||
|
|
</p></li><li><p>
|
|||
|
|
In the equation, <span>$+$</span> on the left-hand side means <span>$+_{U}$</span>, and <span>$+$</span> on the right-hand side <span>${+}_V$</span>, and similarly for scalar multiplication. (You reconstructed the <a href="https://coq.inria.fr/refman/language/extensions/implicit-arguments.html" rel="noreferrer">implicit arguments</a> of <span>$+$</span>.)
|
|||
|
|
</p></li><li><p>
|
|||
|
|
The symbol <span>$2$</span> normally denotes a natural number, as every child knows, but clearly it is meant to denote the scalar <span>$1_K +_K 1_K$</span>. (You interpreed "<span>$2$</span>" in the <a href="https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#notation-scopes" rel="noreferrer">notation scope</a> appropriate for the situation at hand.)
|
|||
|
|
</p></li></ul><p>
|
|||
|
|
The vernacular <span>$V$</span> must support these techniques, and many more, so that they can be implemented in the elaborator. It cannot be anything as simple as ZFC with first-order logic and definitional extensions, or bare Martin-Löf type theory. You may consider the development of <span>$V$</span> to be outside of scope of mathematics and logic, but then do not complain when computer scientist fashion it after their technology.
|
|||
|
|
</p><p>
|
|||
|
|
I have never seen any serious proposals for a vernacular based on set theory. Or to put it another way, as soon as we start expanding and transforming set theory to fit the requirements for <span>$V$</span>, we end up with a theoretical framework that looks a lot like type theory. (You may entertain yourself by thinking how set theory could be used to detect that <span>$f : U \to V$</span> above does not make sense unless we insert coercions – for if everthying is a set then so are <span>$U$</span> and <span>$V$</span>, in which case <span>$f : U \to V$</span> <em>does</em> make sense.)
|
|||
|
|
</p><h3>
|
|||
|
|
Detecting mistakes
|
|||
|
|
</h3><p>
|
|||
|
|
An important aspect of suitability of foundation is its ability to detect mistakes. Of course, its purpose is to prevent logical errors, but there is more to mistakes than just violation of logic. There are formally meaningful statements which, with very high probability, are mistakes. Consider the following snippet, and read it carefully:
|
|||
|
|
</p><blockquote><p>
|
|||
|
|
<strong>Definition:</strong> A set <span>$X$</span> is <em>jaberwocky</em> when for every <span>$x \in X$</span> there exists a bryllyg <span>$U \subseteq X$</span> and an uffish <span>$K \subseteq X$</span> such that <span>$x \in U$</span> and <span>$U \in K$</span>.
|
|||
|
|
</p></blockquote><p>
|
|||
|
|
Even if you have never read Lewis Carroll's works, you should wonder about "<span>$U \in K$</span>". It looks like "<span>$U \subseteq K$</span>" would make more sense, since <span>$U$</span> and <span>$K$</span> are both subsets of <span>$X$</span>. Nevertheless, a proof assistant whose foundation <span>$F$</span> is based on ZFC will accept the above definition as valid, even though it is very unlikely that the human intended it.
|
|||
|
|
</p><p>
|
|||
|
|
A proof assistant based on type theory would reject the definition by stating that "<span>$U \in K$</span>" is a type error.
|
|||
|
|
</p><p>
|
|||
|
|
So suppose we use a set-theoretic foundation <span>$F$</span> that accepts any syntactically valid formula as meaningful. In such a system writing "<span>$U \in K$</span>" is meaningful and therefore the above definition will be accepted by the kernel. If we want the proof assistant to actually <em>assist</em> the human, it has to contain an additional mechanism that will flag "<span>$U \in K$</span>" as suspect, despite the kernel being happy with it. But what is this additional mechanism, if not just a second kernel based on type theory?
|
|||
|
|
</p><p>
|
|||
|
|
I am not saying that it is impossible to design a proof assistant based on set theory. After all, <a href="http://mizar.org" rel="noreferrer">Mizar</a>, the most venerable of them all, is designed precisely in this way – set theory with a layer of type-theoretic mechanisms on top. But I cannot help to wonder: why bother with the set-theoretic kernel that requires a type-theoretic fence to insulate the user from the unintended permissiveness of set theory?
|
|||
|
|
</p><img src="https://www.gravatar.com/avatar/59d57d95bc7c45ced5f1969279cec06b?s=32&d=identicon&r=PG" alt=""/><div>
|
|||
|
|
30
|
|||
|
|
</div><p>
|
|||
|
|
<b>EDIT:</b> Since this question has gotten so much interest, I have decided to substantially rewrite my answer, stating explicitly here on MO some of the more important points rather than forcing the reader to follow links and chase down references.
|
|||
|
|
</p><ol><li>To begin with, it is important to distinguish between <b>what currently existing proof assistants can do</b> versus <b>what they could do if we put in the necessary development work</b>. There is no doubt that existing type-theoretic proof assistants outperform existing set-theoretic proof assistants according to various important metrics, such as convenience, pre-existing libraries, etc. Someone who favors type-theoretic proof assistants therefore always has a trump card to play in these discussions—“What you say is nice in theory, but show me the money. How does your set-theoretic proof assistant perform in practice on real problems?” In an earlier version of this answer, I mentioned a talk by John Harrison entitled, “Let’s make set theory great again!” (<a href="https://www.youtube.com/watch?v=n0YNsJAoWQA" rel="noreferrer">part 1</a> <a href="https://www.youtube.com/watch?v=3jL8p9z86eg" rel="noreferrer">part 2</a> <a href="http://aitp-conference.org/2018/slides/JH.pdf" rel="noreferrer">slides</a>), and Andrej Bauer asked the reasonable question (in the comments below) whether Harrison had implemented his ideas. As <a href="https://cs.nyu.edu/pipermail/fom/2018-May/021026.html" rel="noreferrer">Jeremy Avigad</a> has said, even though he thinks that the “ideal proof assistant would be based on ZFC, with enough practical infrastructure to support all the things we need to do mathematics,” “it is easy to underestimate the difficulties involved in designing a useful and workable system.” At the same time, if we take the long view, we should be careful not to mistake what might be an artifact of our current implementations for a fundamental truth. <a href="https://cs.nyu.edu/pipermail/fom/2018-June/021032.html" rel="noreferrer">Larry Paulson</a> has in effect said “show me the money” in a more literal sense:</li></ol><blockquote><p>
|
|||
|
|
I would guess that the amount of effort and funding going into type theory exceeds the amount that went into set theory by an order of magnitude if not two. It's not unusual to encounter open hostility to set theory and classical logic combined with an air of moral superiority: “Oh, you aren’t constructive? And you don't store proof objects? Really?” And I have seen "proof assistant" actually DEFINED as "a software system for doing mathematics in a constructive type theory".<br/>
|
|||
|
|
<br/>
|
|||
|
|
The academic interest simply isn't there. Consider the huge achievements of the Mizar group and the minimal attention they have received. Also, I think that my 2002 paper on proving the reflection theorem (and presented at CADE, a high-profile conference) was really interesting, but it had been cited only six times, and two of those are by myself.<br/>
|
|||
|
|
<br/>
|
|||
|
|
I am certain that we would now have highly usable and flexible proof assistants based on some form of axiomatic set theory if this objective had enjoyed half the effort that has gone into type theory-based systems in the past 25 years.
|
|||
|
|
</p></blockquote><ol><li><p>
|
|||
|
|
A second point is that everyone acknowledges that having a system where the computer can help you catch silly mistakes is a huge benefit, if not an absolute necessity. For this, some kind of type-theory-like mechanism is very useful. However, this is not as decisive an argument in favor of type theory and against set theory as it might seem at first glance. The “working mathematician” is often tempted to regard the absurdity of a statement such as <span>$2\in 3$</span> as a strong argument against set theory, but the working mathematician also tends to balk at giving <span>$0/0$</span> a concrete value (instead of declaring it to be “undefined”), which is the sort of thing that many proof assistants do. In both cases, there are known ways to block “fake theorems.” It is standard engineering practice to develop systems that contain multiple layers (the distinction between <i>vernacular</i> and <i>foundation</i> in Andrej Bauer’s excellent answer is an example), and the fact that <span>$2\in 3$</span> might be a theorem at some low layer does not automatically mean that this is something a user will be able to enter from the keyboard and not get caught by the system. In principle, therefore—to return to the actual question being asked—set theory does not seem to pose any intrinsic barriers to automation. Indeed, other <a href="https://mathoverflow.net/a/377031">answers</a> and <a href="https://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista#comment956156_376988">comments</a> have made this point, and explained how powerful automation tactics can and have been written in set-theoretic systems such as Metamath. Another example is the work of <a href="https://arxiv.org/abs/1707.04757" rel="noreferrer">Bohua Zhan</a> on auto2, which has shown that many of the alleged difficulties with untyped set theory can be overcome.
|
|||
|
|
</p></li><li><p>
|
|||
|
|
There remains the question, even if a set-theoretic proof assistant with the power and usability of Coq/Lean/Isabelle <i>could</i> be developed, what would be the point? Aren't the already existing type-theoretic assistants good enough? This is a much more “subjective and argumentative” point, but I would propose a couple of arguments in favor of set theory. The first is that set theory has a great deal of flexibility, and it is not an accident that historically, the first convincing demonstration that all of mathematics could be put on a single, common foundation was accomplished using set theory rather than type theory. With a relatively small amount of training, mathematicians can see how to formulate any concepts and proofs in their field of expertise in set-theoretic terms. In the language of Penelope Maddy’s paper, <a href="http://www.socsci.uci.edu/%7Epjmaddy/bio/What%20do%20we%20want%20-%20final" rel="noreferrer">What do we want a foundation to do?</a> set theory provides a <i>Generous Arena</i> and a <i>Shared Standard</i> for all of mathematics with minimal fuss. Of course, there is a price to be paid if we give someone enough rope—they might decide to hang themselves. But if we want to see widespread adoption of proof assistants by the mathematical community, then we should take seriously any opportunities we have to leverage mathematicians’ existing habits of thought. I do not think that it is an accident that set-theoretic proof assistants tend to produce more human-readable proofs than type-theoretic proof assistants do (though I will admit that this could be an artifact of existing systems, rather than a fundamental truth).<br/>
|
|||
|
|
<br/>
|
|||
|
|
Another argument is that if we are interested in reverse mathematics—which axioms are needed to prove which theorems—then there has been a lot more work done to calibrate mathematics against set-theoretic and arithmetical systems than against type-theoretic systems. In Maddy’s language, we might hope for a proof assistant to help us with <i>Risk Assessment</i> and <i>Metamathematical Corral</i>. This does not seem to be a priority with too many people at the present time, but again I am trying to take the long view here. The mathematical community already has a good grasp of how the mathematical universe can be built from the ground up using set theory, and exactly what ingredients are needed to achieve which results. It would be desirable for our proof assistants to be able to capture this global picture.<br/>
|
|||
|
|
<br/>
|
|||
|
|
One could point out that someone who is really interested in set theory can use something like Isabelle/ZF, which builds set theory on top of type theory. That is true. I am not trying to argue here that a set-theoretic foundation with some kind of type theory layered on top is necessarily better than a type-theoretic foundation with some kind of set theory layered on top. I am only trying to argue that set theory does enjoy some advantages over type theory, depending on what you are trying to achieve, and that the claim that “automation is very difficult with set theory,” or that there is nothing to be gained by using set theory as the basis for a proof assistant, should be taken with a grain of salt.
|
|||
|
|
</p></li></ol><p>
|
|||
|
|
Let me conclude with a remark about Lean specifically. A couple of years ago, Tom Hales provided a <a href="https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/" rel="noreferrer">review of the Lean theorem prover</a> that spells out the pros and cons as he saw them at the time. Some of what he said may no longer be true today, but one thing that is true is that even Lean enthusiasts agree that there are flaws that they promise will be fixed in Lean Version 4 (which unfortunately is going to be incompatible with Lean 3, or so I hear).
|
|||
|
|
</p><div>
|
|||
|
|
27
|
|||
|
|
</div><p>
|
|||
|
|
I still find it very surprising that this random talk I gave attracts so much attention, especially as not everything I said was very well thought out. I am more than happy to engage with people in discussions about what I said and whether or not some things I said were ill-informed.
|
|||
|
|
</p><p>
|
|||
|
|
But onto my answer to your question: whilst I am not an expert in proof assistants in general (I have become knowledgeable at precisely <em>one</em> proof assistant and have limited experience with others), it is my empirical observation that high-level tactics like Lean's <code>ring</code> tactic, which will <a href="https://leanprover-community.github.io/lean-web-editor/#code=import%20tactic%0A%0Aexample%20%28R%20%3A%20Type%29%20%5Bcomm_ring%20R%5D%20%28x%20y%20%3A%20R%29%20%3A%0A%20%20%28x%2B2*y%29%5E3%3Dx%5E3%2B6*x%5E2*y%2B12*x*y%5E2%2B8*y%5E3%20%3A%3D%0Abegin%0A%20%20ring%0Aend" rel="noreferrer">prove results</a> like <span>$(x+2y)^3=x^3+6x^2y+12xy^2+8y^3$</span> immediately -- and there are similar tactics in Coq and Isabelle/HOL, two more type theory systems -- do not seem to exist in the two main set theory formal proof systems, namely Metamath and Mizar. I don't really know why, but those are the facts. Note that the proof of this from the axioms of a ring is extremely long and uncomfortable, because you need to apply associativity and commutativity of addition and multiplication many times -- things mathematicians do almost without thinking.
|
|||
|
|
</p><div>
|
|||
|
|
6
|
|||
|
|
</div><p>
|
|||
|
|
I'll answer just the automation question since the other answers gave nice broad overview, but didn't seem focus on that narrow question. My own direct automation experience is wrt to ACL2, Lean and SMT-based solvers.
|
|||
|
|
</p><p>
|
|||
|
|
Strictly speaking, I don't know if there's any foundational argument for why set theory would be better or worse than the type theory-based approach in Lean.
|
|||
|
|
</p><p>
|
|||
|
|
The strengths that Lean have from my perspective are: an expressive explicit type system, a relatively simple core language for representing terms, and a attention to how terms are represented for efficient manipulation.
|
|||
|
|
</p><p>
|
|||
|
|
With regards to typed core logics, most automation in theorem provers is tailored to specific common theories that are widely used in mathematics. When writing such automation, it is important to know the types and operations involved. For example, in writing a decision procedure for linear arithmetic in an untyped language, one needs to carefully check that any transformations still make sense even if the expressions do not denote numbers. By having a typed and typechecked expression language, one gets from the theorem prover itself and does not have to pay the additional runtime and complexity costs.
|
|||
|
|
</p><p>
|
|||
|
|
A second strength of Lean is ensuring that the core language is simple, but expressive so that one can represent proofs compactly. When using automation such as SMT solvers, the "proof terms" generated as evidence can be very large and the core proof language needs to be designed to compactly represent proofs while still be amenably to efficient checking. I'm not sure if Lean has an advantage to Coq or other solvers here per se but it is a factor in Lean's design.
|
|||
|
|
</p><p>
|
|||
|
|
A third strength of Lean is that the language for writing tactics and creating definitions and theorems are one and the same. There is a bit of syntactic sugar for the tactic sequences and a tactic-specific library, but by having the same language one does not have to learn multiple languages just to get started writing tactics. Lean is also not unique here -- ACL2 is similar, but it is a strength of Lean still. It will also become even more relevant with Lean 4 thanks to the efficient compiler being developed.
|
|||
|
|
</p><div>
|
|||
|
|
answered <span title="2020-11-20 20:31:36Z">Nov 20 '20 at 20:31</span>
|
|||
|
|
</div><img src="https://www.gravatar.com/avatar/59a42d941c5ab2d4cd4ce8172c61ec97?s=32&d=identicon&r=PG" alt=""/><div>
|
|||
|
|
-2
|
|||
|
|
</div><p>
|
|||
|
|
Modern programming languages unlike older programming languages, or unlike assembly and machine code are typed. For example c++ with or without templates compared to c, or Java compared to Basic.
|
|||
|
|
</p><p>
|
|||
|
|
With typing, a compiler needs to check that all expressions have the correct type. Generally, this is done by telling the compiler what types are being used. However, we can attempt to automate this process and allow the compiler to work out what the types are by itself, given the base types under consideration. This is known as type inference.
|
|||
|
|
</p><p>
|
|||
|
|
Depending upon the language, type checking and inference can range from trivial to undecidable.
|
|||
|
|
</p><p>
|
|||
|
|
We also say it is sound iff it accepts correctly typed programs.
|
|||
|
|
</p><p>
|
|||
|
|
Now, type checking and inference in the simply typed Lambda Calculus with parametric polymorphism is decidable and one implementation of this is the Hindley-Milner Type Sysyem where complexity is linear in the size of the program; however, the problem is PSPACE hard and EXPTIME complete, meaning that in the worst case scenario it requires a polynomial worth of extra space and an exponential amount of extra time. Luckily, it happens to be linear when the nesting depth of polymorphic variables is bounded.
|
|||
|
|
</p><p>
|
|||
|
|
For example,
|
|||
|
|
</p><blockquote><ol><li>C++ with templates is Turing complete by an informal proof by Veldhuizen '03. This means type checking and inference is undecidable.</li></ol></blockquote><blockquote><ol><li>In C#, both type checking and inference is undecidable. And it is unsound.</li></ol></blockquote><blockquote><ol><li>Similarly Java because Java Generics are Turing Complete. Amin and Tate '15 showed that Java 5 or later is unsound.</li></ol></blockquote><blockquote><ol><li>Haskell has decidable type checking and inference. But with enough extensions, that is to at least System F, then it becomes undecidable as System F is.</li></ol></blockquote><p>
|
|||
|
|
Dependent types allow types to depend upon their values and so give a finer control over types. For example, with ordinary types you cannot have a type for even numbers; with dependent types you can. Unfortunately, adding this capability generally renders type inference undecidable.
|
|||
|
|
</p><p>
|
|||
|
|
Lean is a programming language which is based upon Calculus of Constructions with Inductive Tupes. This calculus is a higher order typed Lambda Calculus and lies at the top node of Barendregt's Lambda Cube. This means it has polymorphism and dependent types.
|
|||
|
|
</p><p>
|
|||
|
|
It's main rival, is Martin Lof's Type Theory which is also dependent and inductive types. It comes in two main varieties, intensional and extensional. The intensional variety can be alternatively thought of as Homotopy Type Theory. In this variety, type inference is decidable whilst in the extensional variety it is not.
|
|||
|
|
</p><p>
|
|||
|
|
Set Theory like machine code, like assembly and like early programming languages are not typed. So type checking does not apply. As types allow us to program more safely, these languages are not as safe as typeful languages and hence, automation is more difficult here as we cannot prove they will act as we expect them to do so.
|
|||
|
|
</p><p>
|
|||
|
|
Typed languages does not mean that untyped languages will go away. After all, the languages at all in fact nested. Haskell, at bottom, is still executed by machine code and this is untyped. Hence, development of both is required for automation in all it's varieties.
|
|||
|
|
</p><p>
|
|||
|
|
After all, if I had to program the fastest loop to add as many consecutive integers in a second as I could on a particular machine I would choose to write it in machine code, I typed as it is - every time. More importantly, in my opinion it's makes one realise how the whole stack of languages from the editor through the compiler and then through the interface and interrupts down to the metal works. In this way, you learn more about how every works 'under the hood' - so to speak.
|
|||
|
|
</p><p>
|
|||
|
|
<strong>edit</strong>
|
|||
|
|
</p><p>
|
|||
|
|
@LSpice: It's written this way because the question itself is kind of vague. Why not ask the OP to tighten up the question? The proposed question is answered in the last paragraph. And the preceding paragraphs simply explains my terms and my thinking in a step-by-step pedagogical manner rather than a deus ex-machina manner ... or do you think explanatory text is a little too old-fashioned for the hyped up and glib virtual world?
|
|||
|
|
</p></div>
|