I want to understand type theory but I have to know first how I can apply it. Could there be more non-obvious applications of type theory aside from in type systems in programming? Could there be other applications, let's say in personality profiling and the likes?
$\begingroup$
$\endgroup$
7
-
2$\begingroup$ Why does something have to have applications outside what it was invented for? $\endgroup$– Raphael ♦Oct 27, 2015 at 9:05
-
3$\begingroup$ Foundations of mathematics? People also have used type theory for formalizing things like synthetic domain theory, topology, etc. There's also Chris Martens' work on using type theoretic tools to model narrative story telling. Dissertation link $\endgroup$– daniel gratzerOct 27, 2015 at 12:19
-
1$\begingroup$ Could yoy clarify counts as an application? $\endgroup$– JakeOct 28, 2015 at 8:27
-
4$\begingroup$ I'm not convinced by your premise. Suppose that somebody said, "I want to understand automotive engineering but I have to know first what I can use a car for. Could there be more non-obvious applications of cars aside from transportation?" They get answers saying that some people sleep in their cars, and Ansel Adams used his as a platform to take photographs from. Well that's great but it doesn't help anyone understand engineering and is likely to lead our hypothetical student to design cars with super-reclining seats and very stiff suspension. $\endgroup$– David RicherbyOct 28, 2015 at 18:56
-
3$\begingroup$ The fact is that much of theoretical computer science (including the stuff I work on) is practically useless, though mathematically beautiful. Unfortunately you have to pick sides. $\endgroup$– Yuval FilmusOct 28, 2015 at 21:57
|
Show 2 more comments
5 Answers
$\begingroup$
$\endgroup$
9
Because of the Curry-Howard correspondence, types can be interpreted as propositions, and propositions as types.
As a result of this, type theory is applicable to literally any field that uses formal logic for its proofs. This can be circuit verification, real analysis, symbolic logic, geometry, etc.
For instance, some automated proof checking tools work using this principle: they check the validity of the proof by type-checking a particular term in some type system. The LF proof checker is based on this approach, as is HOL Light. As an example application, proof-carrying-code used LF to check proofs of memory-safety of untrusted code. The benefit of using this kind of proof-checker is that the implementation can be very simple, and thus we can gain high assurance that the implementation is correct. See, e.g., the following paper:
Foundational Proof Checkers with Small Witnesses. Dinghao Wu, Andrew W. Appel, Aaron Stump. PPDP 2003.
-
$\begingroup$ This might help: math.ucr.edu/home/baez/rosetta.pdf $\endgroup$– Pseudonym ♦Oct 28, 2015 at 5:15
-
1$\begingroup$ I don't think this answers the question. What about actual applications? $\endgroup$ Oct 28, 2015 at 7:57
-
-
1$\begingroup$ Do you know if anyone's used type theory to prove something new about circuit verification, real analysis, symbolic logic or geometry? Or are we just talking about cases where somebody uses 20 pages of type theory to prove something that takes three lines in an elementary textbook? $\endgroup$ Oct 28, 2015 at 19:11
-
$\begingroup$ @David What this answer is that in principle you can use type theory to prove stuff. Also, in principle we can use cellular automata to prove stuff, since Rule 110 is Turing-complete. I think the former statement is as meaningless as the latter. $\endgroup$ Oct 28, 2015 at 21:56
$\begingroup$
$\endgroup$
2
You may be interested in the work on Ceptre, a result of the PhD research of Chris Martens, which uses type theory for interactive storytelling. Quoted below is the thesis abstract:
Interactive storytelling weaves together deep computational ideas with humanity's rich history of story and play, providing an important context for tools and languages to be built. At the same time, formal specification languages offer a palette of representation and inference techniques typically reserved for the analysis of programming languages and complex deductive systems. This thesis connects problems in the interactive storytelling domain to solutions in formal specification.
Specifically, we examine narrative from a structural point of view and observe that alternative narrative paths play a complementary role to simultaneous interacting timelines. Linear logic provides the representational tools necessary to investigate this structure, and by extending the correspondence to proofs and proof construction, we find a suite of computational possibilities. We present three efforts toward realizing those possibilities: (1) the use of linear logic programming to generate narratives; (2) a new programming language for authoring interactive narratives, games, and simulations; and (3) techniques for stating and proving design-level program properties.
We find that linear logic programming, enriched with a minimal extension to its logical semantics, enables a wide range of programming idioms and domain encodings. As evidence, we give five case studies, including social simulation, combat-based adventure games, and board games. To support reasoning about design correctness, we present techniques for stating and proving program invariants, as well as a decidability proof for automatically checking those invariants for a large fragment of the language.
These findings show that linear logic is a fruitful representation language to serve as the basis for modeling and executing interactive worlds, and they invite future investigations on using proof-theoretic methodologies for creative systems.
-
1$\begingroup$ That sounds like a use of linear logic, rather than type theory per se. $\endgroup$ Oct 29, 2015 at 9:03
-
6$\begingroup$ Linear logic is a cornerstone topic of type theory. This work is very much part of type theory as a discipline (some people describe their work as "proof theory" when it's equally relevant to type theory, although the names are not equivalent as some other works in "proof theory" would be considered as more specific to proof theory rather than also central to type theory). $\endgroup$– gascheOct 29, 2015 at 9:23
$\begingroup$
$\endgroup$
There has been interesting uses of type theory in linguistics. See for example the linguistic works of Chung-chieh Shan or Christian Rétoré.
Quoted below is the description of Rétoré's book on categorial grammars:
This book is a contemporary and comprehensive introduction to categorial grammars in the logical tradition initiated by the work of Lambek. It guides students and researchers through the fundamental results in the field, providing modern proofs of many classic theorems, as well as original recent advances. Numerous examples and exercises illustrate the motivations and applications of these results from a linguistic, computational and logical point of view. The Lambek calculus and its variants, and the corresponding grammars, are at the heart of these lecture notes. A chapter is devoted to a key feature of these categorial grammars: their very elegant syntax-semantic interface. In addition, we adapt linear logic proof nets to these calculi since they provide efficient parsing algorithms as exemplified in the Grail parser. This book shows how categorial grammars weave together converging ideas from formal linguistics, typed lambda calculus, Montague semantics, proof theory and linear logic, thus yielding a coherent and formally elegant framework for natural language syntax and semantics.
The following quote is in the introduction of Shan's Linguistic Side Effects book chapter:
This paper relates cases of apparent noncompositionality in natural languages to those in programming languages. It is shaped like an hourglass: I begin in §1 with an approach to the syntax-semantics interface that helps us build compositional semantic theories. That approach is to draw an analogy between computational side effects in programming languages and what I term by analogy linguistic side effects in natural languages.
This connection can benefit computer scientists as well as linguists, but I focus here on the latter direction of technology transfer. Continuations have been useful for treating computational side effects. In §2, I introduce a new metalanguage for continuations in semantics.
The metalanguage I introduce is useful for analyzing both pro- gramming languages and natural languages. For intuition, I survey the first use in §3, then point out the virtues of this treatment in §4.
Turning to natural language in §5, I describe in detail how this perspec- tive helped Chris Barker and I study binding and crossover, as well as wh-questions and superiority. I have also used continuations to study quantifier and wh-indefinite scope, particularly in Mandarin Chinese, but there is only room here to sketch these further developments, in §6.
$\begingroup$
$\endgroup$
1
An interesting article that explain applications of dependent types, is the The Power of Pi, that shows how Agda can be used to solve interesting problems.
Another good example is the use of dependent types to resource control. A good example is the file management API of Effects of Idris. For instance, the function for reading a line from a file has the following type
readLine : { [FILE_IO (OpenFile Read)] } Eff String
which specifies that this function is only applicable if there's a file opened. The list in braces indicates which effects are available. In this case, we have that this function requires the effect of having a file opened for reading.
More information on Effect library can be found here.
One more application is the use of dependent types for concurrency as reported in the following article by the creator of Idris.
-
1
$\begingroup$
$\endgroup$
2
as mentioned in jmite's answer, higher order logic/ type theory in circuit/ hardware/ electronics verification has been around for decades and is now so routine that its not even noticed/ regarded so much as an "application" after an apparently major transfer effort in the ~1990s although its still an active area of research. there is also a lot of application of Coq and its type logic in particular to circuit/ hardware/ electronics verification all the way from low level gate logic to much higher level/ order structures/ subsystems. here are a few key refs
Higher order logic and hardware verification / Melham (1993!)
Higher Order Logic Theorem Proving and its Applications/ Claeson, Gordon
Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types / Brady, Mckinna, Hammond
Certifying circuits in Type Theory / Grimal
Coquet: a Coq library for verifying hardware / Braibant
-
1$\begingroup$ To be fair, though, most actual hardware verification at an industrial scale has been done using model checking, a verification technology that is generally unrelated to type theory (although bridges have been drawn recently). Type theory has been used to build hardware description languages (not far-fetched from programming languages), and most of the languages you give are in this category, and some of the proof-assistants designed for hardware verification (notably the original HOL, but not the most-used PVS) are Curry-Howard transposes of type theory. $\endgroup$– gascheNov 1, 2015 at 9:25
-
$\begingroup$ if you have deeper background in hardware verification it would be interesting to hear more details in Computer Science Chat but think/ suspect narrow/ distinct lines/ generalizations are not easy to draw in this area eg between model checking and type theory. it can take very subtle historical analysis to comprehensively uncover/ piece together connections between two different fields with different aims and sometimes is even outside of the capabilities of experts in either field individually... the refs overall show strong connections that could be analyzed further... $\endgroup$– vznNov 1, 2015 at 18:03