Questions tagged [type-theory]
Type structure is a syntactic discipline for enforcing levels of abstraction.
57
questions
11
votes
1
answer
1k
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'...
- 3,177
2
votes
1
answer
245
views
How to encode a function from an existential type
I am having trouble using parametricity to show that existential types work in System F (or System Fω) in the way one would expect them to work.
It is known that an existential type $\exists t.~P~t$ (...
- 552
19
votes
3
answers
4k
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 ...
- 293
16
votes
1
answer
1k
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.
...
- 261
9
votes
2
answers
2k
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 + ...
- 201
49
votes
3
answers
4k
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 ...
- 1,325
48
votes
2
answers
6k
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 ...
- 2,611
48
votes
5
answers
7k
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 ...
- 1,325
44
votes
4
answers
5k
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 ...
user788
35
votes
3
answers
3k
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 ...
- 463
29
votes
6
answers
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, ...
- 1,103
26
votes
1
answer
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 ...
- 677
26
votes
2
answers
2k
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 ...
25
votes
2
answers
3k
views
Why do Agda and Coq disagree on strict positivity?
I've stumbled across a confusing disagreement between Agda and Coq that is not obviously related to the most well known distinctions between their type theories (e.g., (im)predicativity, induction-...
- 471
21
votes
1
answer
2k
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:
...
- 1,762
20
votes
2
answers
3k
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 ...
- 461
18
votes
2
answers
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 ...
- 291
16
votes
1
answer
586
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 ...
- 505
16
votes
3
answers
1k
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 ...
user6892
16
votes
1
answer
805
views
Relative consistency of PA and some type theories
For a type theory, by consistency, I mean that it has a type which is not inhabited. From the strong normalization of the lambda cube, it follows that system $F$ and system $F_\omega$ are consistent. ...
- 343
15
votes
1
answer
615
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 ...
- 1,695
15
votes
1
answer
1k
views
Is MLTT effectively pCiC without Prop?
Is Martin-Löf type theory basically the predicative Calculus of inductive Constructions without impredicative $\mathtt{Prop}$?
If they're closely related but with more differences than just $\mathtt{...
- 615
14
votes
0
answers
442
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, ...
- 3,177
13
votes
1
answer
1k
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 ...
- 1,213
13
votes
3
answers
910
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 ...
- 2,069
12
votes
3
answers
2k
views
Type inference for imperative statements other than assignment
In my search for research papers about type systems for imperative languages, I only find solutions for a language with mutable references but without genuine imperative control structures such as ...
- 301
11
votes
2
answers
896
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 ...
- 1,540
11
votes
1
answer
327
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 ...
- 4,561
11
votes
2
answers
450
views
Hereditary substitution with a universe hierarchy
I've read about hereditary substitution for the Simple Lambda Calculus and for The Logical Framework with distinct terms and types.
I'm wondering, are there any examples of hereditary substitution in ...
- 2,952
11
votes
4
answers
1k
views
Explaining monad transformers in categorical terms
Most resource regarding categorical notions in programming describe monads, but I've never seen a categorical description of monad transformers.
How could monad transformers be described in the terms ...
- 2,611
10
votes
1
answer
368
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?
- 1,762
10
votes
3
answers
1k
views
Universal and existential types
I'm trying to wrap my head around the concepts of universal and existential types but everywhere I look, I see either logical or operational intuitions (or implementations) (e.g. TAPL book by B. ...
- 121
10
votes
1
answer
900
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 ...
- 2,581
10
votes
2
answers
513
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 ...
- 203
10
votes
1
answer
1k
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?
- 3,177
9
votes
1
answer
472
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 ...
- 701
8
votes
1
answer
854
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 ...
- 1,213
8
votes
3
answers
770
views
What's the logical counterpart to jumps with arguments on CPS terms?
It's well known that the CPS (continuation-passing style) translation often employed in compilers corresponds to double negation translation under the Curry-Howard isomorphism. Though often the target ...
- 387
8
votes
2
answers
878
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.
- 2,835
7
votes
1
answer
393
views
Can type inference be classified in two groups: unification-based and control-flow-based?
I recently came across the 1995 paper Safety analysis versus type inference (pdf link) by Palsberg and Schartzbach that contrasts unification-based type inference and static analysis methods based on ...
- 173
7
votes
2
answers
678
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 ...
- 1,762
6
votes
1
answer
807
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 ...
- 1,187
6
votes
1
answer
682
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 ...
- 163
5
votes
1
answer
492
views
Complexity of type-checking in relation to complexity of normalization
In order to verify that a terminating program terminates, one thing that can be done is to actually run the program. That may take a lot of time. If the program is typed in a total type-system, we can ...
- 1,187
4
votes
0
answers
524
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:
...
- 3,177
4
votes
0
answers
170
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 ...
- 2,952
4
votes
0
answers
98
views
Is the encoding of existential types in System F adequate?
This is somewhat related to How to encode a function from an existential type
Existential types can be encoded in System F. If $P$ is any type constructor, not necessarily covariant, then the ...
- 552
4
votes
1
answer
783
views
Dependent Sums and Products
I'm trying to understand the connections between a few different concepts fundamental to dependent type theory.
Dependent functions ($\Pi$-types)
Including non-dependent functions ($A \rightarrow B$)...
- 145
3
votes
1
answer
220
views
Type of induction principle for fixpoint types
To the Calculus of Constructions we could add a general fixpoint type constructor (accepting inconsistencies or assuming F is a ...
- 701
3
votes
0
answers
423
views
Is it possible to check equality of equi-recursive types, or recursive λ-terms?
Can we determine if two λ-terms are equal?
Given two lambda terms, let's say they are equal if their (possibly infinite) Bohm trees are. Under this definition, for example, ...
- 3,177