Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [type-theory]

Type structure is a syntactic discipline for enforcing levels of abstraction.

9
votes
1answer
359 views

Can Elementary Affine Logic be used as the core type system of a practical programming language?

Elementary Affine Logic is a type system which captures the class of λ-terms that can be reduced in elementary time. Moreover, EAL-typeable terms can be reduced using the abstract fragment of Lamping'...
18
votes
3answers
2k views

Classification of Typed/Untyped Lambda Calculi

Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi? I'm particularly ...
15
votes
1answer
886 views

Can boolean algebra be expressed in simply typed lambda caclulus?

Boolean algebra can be expressed in untyped lambda calculus in (for example) this way. ...
46
votes
5answers
5k views

What is the most intuitive dependent type theory I could learn?

I am interested in getting a really solid grasp on dependent typing. I've read most of TaPL and read (if not fully absorbed) 'Dependent Types' in ATTaPL. I've also read and skimmed a bunch of articles ...
39
votes
4answers
3k views

How would I go about learning the underlying theory of the Coq proof assistant?

I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use ...
44
votes
3answers
3k views

How do 'tactics' work in proof assistants?

Question: How do 'tactics' work in proof assistants? They seem to be ways of specifying how to rewrite a term into an equivalent term (for some definition of 'equivalent'). Presumably there are formal ...
38
votes
2answers
5k views

Explaining Applicative functor in categorical terms - monoidal functors

I'd like to understand Applicative in terms of category theory. The documentation for Applicative says that it's a strong lax ...
32
votes
3answers
2k views

Type classes vs object interfaces

I don't think I understand type classes. I'd read somewhere that thinking of type classes as "interfaces" (from OO) that a type implements is wrong and misleading. The problem is, I'm having a problem ...
19
votes
2answers
1k views

Is there a typed lambda calculus which is consistent and Turing complete?

Is there a typed lambda calculus where the corresponding logic under the Curry-Howard correspondence is consistent, and where there are typeable lambda expressions for every computable function? This ...
28
votes
6answers
2k views

Why naturals instead of integers?

I'm interested in why natural numbers are so beloved by the authors of books on programming languages theory and type theory (e.g. J. Mitchell, Foundations for programming languages and B. Pierce, ...
25
votes
1answer
1k views

Are types propositions? (What are types exactly?)

I've been reading a lot on type systems and such and I understand roughly why they were introduced (in order to resolve Russel's paradox). I also understand roughly their practical relevance in ...
17
votes
1answer
822 views

Why it's impossible to declare an induction principle for Church numerals

Imagine, we defined natural numbers in dependently typed lambda calculus as Church numerals. They might be defined in the following way: ...
25
votes
2answers
1k views

Context Sensitive Grammars and Types

1) What, if any, is the relationship between static typing and formal grammars? 2) In particular, would it be possible for a linear bounded automaton to check whether, say, a C++ or SML program was ...
14
votes
1answer
247 views

Logical Reations for an Impredicative System in a Predicative MetaTheory

Logical Relations for Impredicative languages like System F seem to rely critically on impredicativity of the ambient logic. Specifically, the interpretation for the forall-type will be defined in ...
17
votes
2answers
2k views

Implicit vs explicit subtyping

This page asserts that many languages do not use implicit subtyping (structural equivalence), prefering explicit/declared subtyping (declaration equivalence) I've mostly used programming ...
15
votes
0answers
260 views

Are there simple core languages which are consistent and expressive?

The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...
15
votes
3answers
846 views

Can we prove weak normalization for System F by induction on a transfinite ordinal

Weak normalization for the simple typed lambda calculus can be proved (Turing) by induction on $\omega^2$. An extended lambda calculus with recursors on natural numbers (Gentzen) has a weak ...
10
votes
3answers
584 views

For what languages is there already a theory of observational equivalence?

For a correctness proof, I'm looking for a usable notion of program equivalence $\cong$ for Barendregt's pure type systems (PTSs); missing that, for enough specific type systems. My goal is simply to ...
7
votes
1answer
227 views

Fixed points in dependent type theories

Most dependent type theories aim for some notion of correctness in two respects: The type system must be decidable. The type system must be consistent. e.g. $\forall \tau. \tau$ should not be ...
13
votes
1answer
321 views

Minimal specification of Martin-Löf type theory

I'm reading the formal presentation of Martin-Löfs type theory (appendix of the HoTT book). The authors introduce a hierarchy of universes, then $\Pi, \Sigma,+, {\bf 0}, {\bf 1}$ and also $W$-types as ...
10
votes
2answers
632 views

Formalizing the theory of finite sets in type theory

Most proof assistants have a formalization of the concept of "finite set". These formalizations, however, differ wildly (although one hopes that they are all essentially equivalent!). What I don't ...
10
votes
1answer
595 views

Algorithm to determine function equality on the simply typed lambda calculus?

We know that beta-equality of simply typed lambda-terms is decidable. Given M,N:σ→τ, is it decidable whether for all X:σ, MX $≃_β$ NX?
9
votes
2answers
152 views

Decidability of type inference and type checking in MLTT

In Martin-Löf's An Intuitionistic Theory of Types: Predicative Part it is proved that type checking $a \colon A$ is decidable subject to $a$ being typeable in the first place, by proving a ...
9
votes
1answer
425 views

In System F à la Church, can we automatize type inference for the for-all elimination?

The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$. Now, suppose ...
7
votes
1answer
474 views

Is Church-pentation implementable in Agda?

Inspired by suggestion in this question, I've implemented predicative Church encoding of Peano arithmetic. Exponentiation works fine, unfortunately tetration requires the level of one of the arguments ...
6
votes
2answers
390 views

“Correctness” of type theory

How to "proof" that type theory is correct? Or at least explain that it's meaningful in some sense. In what extent is this a mathematical question and in what is a philosophical one? When type ...
4
votes
0answers
120 views

Hereditary Substitution with Inductives and Eliminators?

I'm wondering, is there any existing work on hereditary substitution with inductive type families and dependent eliminators? In particular, normalizing the application of an eliminator to an ...
4
votes
1answer
272 views

Strong normalization property of CoC inside CoC

Wikipedia says that The CoC is strongly normalizing, although, by Gödel's incompleteness theorem, it is impossible to prove this property within the CoC since it implies inconsistency. Why is ...
4
votes
0answers
451 views

Is it possible to derive induction by extending CoC with recursion?

Suppose we extended the CoC with primitive recursion; that is, we added a term µ x . t such that equality allowed unrolling recursive terms: ...
10
votes
1answer
501 views

Can affine lambda calculus solve every problem in P?

In Advanced Topics in Types and Programming Languages it is mentioned, in the chapter on sub-structural type systems, that a "carefully crafted" affine lambda calculus with a recursion combinator for ...
9
votes
1answer
225 views

Example of where violation of strict positivity condition in inductive types leads to inconsistency

Most dependent typed systems have a strict positivity conditions for inductive types. Does anybody know an example where violation of the condition leads to inconsistency in the system?
9
votes
1answer
773 views

Will Martin-Löf Type Theory lead to a greater ability to write provably correct code?

This post refers to the Curry-Howard isomorphism and the Martin-Löf Type Theory. The post makes the claim of a future 'unification' between the the describing language of math, and the operation ...
9
votes
0answers
189 views

reference request: deciding validity of higher-order quantified boolean formulas is not Kalmar-elementary

$\newcommand\iddots{⋰}$In "A simple proof of a theorem of Statman" (TCS 1992), Harry Mairson gives a simple proof of Statman's result that deciding $\beta\eta$-equality of terms in simply typed lambda ...
7
votes
2answers
725 views

An example of a totally computable function that is not definable in system T?

Could you give me an example of a totally computable function of type N × N → N that is not definable in System T? Thanks.
3
votes
1answer
320 views

What exactly is “large elimination”?

I'm studying type theory (mostly Coq) and often encounter the term "large elimination", usually when talking about type universes hierarchy consistency, for example: impredicative polymorphism + ...
1
vote
0answers
152 views

Is it possible to type Ackermann function with (stratified variant of) System F?

I was surprised to find no open-source implementation of Ackermann function in pure System F as an illustrative example. I finally managed to implement it myself in Haskell using Church encoding: <...