5
$\begingroup$

I'm looking for a high-level explanation although if that isn't possible or difficult, I'd prefer references to books/papers.

I understand that modern type theory is inspired by Curry-Howard correspondence. From the Wikipedia article on Curry-Howard correspondence:

The correspondence has been the starting point of a large spectrum of new research after its discovery, leading in particular to a new class of formal systems designed to act both as a proof system and as a typed functional programming language. ... This field of research is usually referred to as modern type theory.

Looking at the various type theories proposed and under development, I have a few basic questions:

1. Most modern type theories marry a type system with lambda calculus. Are there examples where a type theory uses a computational calculus other than lambda calculus?

2. At a very high level, if every modern type theory is a bundle of a type system and a computational calculus and the computational calculus is turing-complete (like lambda calculus), does the computational calculus in any way affect the decidability of decision problems like type checking, type inference, etc.? (AFAIK modern type theories tweak the type system while keeping the associated turing-complete computational calculus intact and just tweaking the type system affects decidability of type checking, type inference, etc.)

EDIT

Type Theory in Formal Verification of Programs

NB: The distinction between Type Theory 1 and Type Theory 2 is based on their application in formal verification of programs and not based on the philosophy of type theory research. Also, the Program/Computation/Dynamic blocks are bigger as I guess existing programming languages have higher computational complexity than the type theories used for formal verification of their programs.

W.R.T. to the illustration above:

1) In type theory 1 methods, are type theories used both consistent and complete (w.r.t. Godel’s incompleteness theorem)? If there are type theories in proof assistants that are incomplete; leading to undecidable decision problems, how does the undecidability manifest in practical applications (like proving the correctness of a complex distributed systems protocol)?

2) In type theory 2 methods, what are the limitations of type theories in static analysis (w.r.t. Rice’s theorem)? Here, is decidability in type theories also affected by the computational model of programming language (eg. imperative vs functional languages)?

$\endgroup$
  • 1
    $\begingroup$ Note that cross-posting on Stack Exchange sites is discouraged. $\endgroup$ – varkor Mar 23 at 12:38
  • $\begingroup$ I'm not sure what exactly you mean by "computational calculus", but the lambda calculus and its variants are computational: this is why the $\beta$-laws are often called "computational rules". You can make this even more explicit by treating $\beta$-reduction as explicit rewriting rules. The type system and its computational behaviour are not differentiated. Dependent type theories integrate terms into the type system and so undecidability at the term level leads to undecidability at the type level, for instance with type inference or even type checking. $\endgroup$ – varkor Mar 23 at 12:43
  • 1
  • $\begingroup$ @D.W. Thanks. I can see the question is already closed on cstheory. I want to close (not delete) it on math too, but am not sure how to do it. $\endgroup$ – Bharat Khatri Mar 25 at 19:24
  • 1
    $\begingroup$ @BharatKhatri, you can't. All you can do is delete it. (You could flag it and ask the mods to close it, but really, rather than adding to their workload, it would be better to simply delete it yourself.) $\endgroup$ – D.W. Mar 25 at 20:31
4
$\begingroup$

I don't think that the term "modern" helps distinguish anything. One way to explain is to draw a distinction between "behavioral", or "semantic", type theories and "formal", or "syntactic", type theories.

Behavioral type theories start with a notion of computation (say, an operational semantics of some kind), and define types as descriptions of program behavior, ie specifications. For example, one might specify that a function takes primes to primes as a description of how it behaves. Membership in a type is a matter of truth, not formal proof, and is never remotely axiomatizable, by Gödel's Theorem.

Formal, or syntactic, type theories are given by a collection of rules, including axioms as no-premise rules. They are inherently recursively enumerable, and never come close to any notion of truth. In particular such type theories, which often enjoy a (n empty) correspondence with a logical system (the poorly named C-H Correspondence), have no inherent meaning, computational or not. They are mere formalisms.

The two concepts may be linked by stipulating a priori that programs must be "well-typed" in the formal sense, with specifications of behavior refining types (for example, isolating the primes among the naturals). There are good reasons to take this viewpoint, namely that the rules prevent you from writing the code that you didn't want to write (eg, enforcing abstraction boundaries). But they also prevent you from writing the code that you do want to write (they define up-front what are the programs). The benefit of such restrictions is something called "the fundamental theorem", which states that syntactically well-formed programs enjoy behavioral properties associated to their types, a generalization of "type safety". In particular, the parametricity theorem is an example; it expresses that abstraction is properly enforced.

| cite | improve this answer | |
$\endgroup$
3
$\begingroup$

You are probably looking for computational type theory and you should probably look into realizability theory as well, which explains how to interpret type theory (and higher-order logic) on top of almost any kind of computational model.

Type theories based on a computational models that are Turing complete typically does not have decidable equality. An example of such a type theory is NuPRL.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ thanks for the pointers! I'm down a deep rabbit hole here, have rephrased the questions to make them more precise. Would you mind having a look? $\endgroup$ – Bharat Khatri Mar 25 at 19:21
  • 1
    $\begingroup$ What you call "type theories 2" looks a bit like a realizaiblity model, or a Curry-style type theory, or a computational type theory (it's difficult to tell from a picture). Regarding "type theories 1": if you have a type theory with decidable type checking, then proof extraction will give you only a strict subset of all Turing-computable functions. But you can have a "type theory 1" which has non-decidable type checking and that can express all Turing-computable functions. There's lots of freedom here. $\endgroup$ – Andrej Bauer Mar 25 at 19:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.