Source: https://cs.stackexchange.com/questions/48754/daily-applications-of-type-theory/48843
Timestamp: 2019-04-22 14:37:34+00:00

Document:
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?
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.
There has been interesting uses of type theory in linguistics. See for example the linguistic works of Chung-chieh Shan or Christian Rétoré.
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.
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.
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.
Foundational Proof Checkers with Small Witnesses. Dinghao Wu, Andrew W. Appel, Aaron Stump. PPDP 2003.
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.
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.
Not the answer you're looking for? Browse other questions tagged type-theory applied-theory or ask your own question.
Does modern type theory include specifications and implementations?
Cubical type theory for dummies?
Introduction to type theory for a beginner?

References: §1
 §2
 §3
 §4
 §5
 §6