Questions tagged [type-theory]
Type structure is a syntactic discipline for enforcing levels of abstraction.
405
questions
7
votes
3
answers
627
views
Example of a term in system F which is not typable in the simply typed lambda calculus
What is the simplest possible example of a (correctly typed) term in system F that does not correspond to any correctly typed term in the simply typed λ-calculus?
More precisely, I am looking for a ...
- 841
7
votes
1
answer
642
views
Which universities in the U.S. are doing research in type theory?
The question is meant to be broad in that recommendations with mentions of the particular areas within type theory research are greatly appreciated. Also, the research need not be conducted in ...
- 173
7
votes
2
answers
641
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
7
votes
2
answers
436
views
Is case analysis on normal forms of lambda terms sufficient to prove parametricity results?
There are many closed terms of a given type. For instance, both of these terms:
$$ \lambda x . x $$
$$ \lambda x . (\lambda y . y) x $$
have a type of a polymorphic identity function:
$$ \forall X ....
- 1,187
7
votes
3
answers
487
views
When a type is a value?
In functional programming and in the theoretical setting of the $\lambda$-calculus it is standard to consider a lambda abstraction $\lambda x.M$ as a value. In my understanding, the intuitive reason ...
7
votes
1
answer
240
views
Stronger "induction" principles than induction-recursion
Are there type theories in the literature with "induction" principles stronger than induction-recursion? This answer gives System F as an example of a theory stronger than MLTT + induction-...
7
votes
2
answers
428
views
Explicit set of types and terms in MLTT
Whenever I read a presentation of MLTT, especially in the context of the correspondence of MLTT with LCCCs (eg. Seely's paper), they say "the type constructors/formation rules are..." and then list a ...
- 173
7
votes
1
answer
818
views
Constraint types (IBM/X10) compared to dependent types
Constraint types have been proposed by IBM in their X10 programming language (it's a commercial programming language, not open source software).
Nystrom, Nathaniel, et al. "Constrained types for ...
- 443
7
votes
1
answer
358
views
Semantic definition of strict positivity for a functor
If we consider a definition of recursive type as:
F : Type -> Type;
T = fix F;
It is customary to talk about the functor F ...
- 390
7
votes
1
answer
393
views
Decidability of parametric higher-order type unification
I'm making a language that has higher-kinded types (like Haskell) and allows type synonyms to appear partially applied in type expressions (unlike Haskell). As an example, consider the following ...
- 501
7
votes
1
answer
396
views
The precise definition of Normalization By Evaluation?
The Wikipedia article suggests that NbE is a technique for obtaining "the normal form of terms" by translating the object language into abstractions of the meta (host) language:
The ...
- 105
7
votes
1
answer
1k
views
Strongly normalizing type theory beyond induction-recursion
Are there known type theories in the literature, which have strong normalization proofs and their proof-theoretical strength goes beyond strength of type theories with induction-recursion?
- 920
7
votes
1
answer
246
views
If the untyped language is terminating, can we still derive a contradiction from `Type : Type`?
Question
If a pure type system has a terminating proof language, can we have Type : Type at the logic level without causing paradoxes (i.e., without causing ...
- 3,137
7
votes
1
answer
364
views
Implications of the rule of cumulativity in the Calculus of Constructions
Please help me understand some type theory research.
As suggested in "Type Checking with Universes" by Robert Harper and Robert Pollack, we can add the following rule to our otherwise standard COC or ...
- 720
7
votes
1
answer
772
views
Determinism and pi-calculus
Milner embedded $\lambda$-calculus into $\pi$-calculus, showing that the $\pi$-calculus is capable of Turing-complete, deterministic calculation. Since parallel compositions of processes in the $\pi$-...
- 616
7
votes
1
answer
327
views
How Univalence can be used for proofs about algorithm correctness
I read a book on homotopy type theory. HoTT has the univalence axiom. This axiom seems to simplify working in category theory, but which other fields of mathematics it simplifies? I.e. how can I use ...
- 1,762
7
votes
1
answer
233
views
Where do people publish/submit their work on type theory?
Besides the most common venues (perhaps POPL, ICFP, LICS and FSCD), where else are papers on type theory commonly published?
Especially, I'm looking for more "pure mathematical" venues/journals which ...
- 1,175
7
votes
1
answer
321
views
Type checking, Hypothetical judgments, meaning explanations and computational type theory
We say that a system is a computational type theory if it is a type theory defined by not a bunch of inference rules, but some sort of Martin-Löfian meaning explanations (e.g. in the sense of NuPRL). ...
- 777
7
votes
1
answer
386
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
1
answer
473
views
Avoiding Cycles with Unification and Subtyping
Context
I realize that subtyping often doesn't admit principle types, and that inference in the presence of subtypes is undecidable. I'm working in a context where typechecking should simply fail ...
- 2,832
7
votes
1
answer
328
views
How to define eta-equivalence for F-omega types?
There are (at least) two styles for defining a (declarative) equivalence judgement for a typed lambda calculus:
via a plain relation $t_1 = t_2$,
via an indexed relation $\Gamma \vdash t_1 = t_2 : T$...
- 1,310
7
votes
1
answer
191
views
"Interesting" categories whose internal logic is a dependent-linear type theory
Dependent-linear type theories may be a functional programmer's dream, but is it categorically interesting, i.e. is it the internal language of an "interesting" category? By "...
- 1,175
7
votes
1
answer
194
views
Can you regain the Church-Rosser property in languages with continuations?
I'm aware that if you naively add continuations to a language, the Church-Rosser property no longer holds. For example, suppose we have some variant of the STLC with basic arithmetic and integer types....
- 81
7
votes
1
answer
342
views
Finding a common factor in $\lambda$-terms that agree under certain substitutions
Suppose that $\mathcal{L}$ is the language of a simply typed lambda calculus of two base types, $e$ and $t$, with infinitely many constants at each type.
A substitution $j$ is a mapping from ...
- 453
7
votes
0
answers
227
views
Relationship between Pataraia's theorem and inductive-recursive definitions?
Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem ...
- 32.6k
7
votes
0
answers
629
views
How to do Type Inference using an SMT solver?
I understand that Hindley-Milner Type Inference can be implemented using an off-the-shelf SMT (Satisfiability Modulo Theories) solver?
How would this work, for example for a very simple type system (...
- 369
7
votes
0
answers
294
views
MLTT vs. [weak] MSOL
I've noted that both Martin-Lof type theory and [Weak] Monadic Second-Order logic (eg over trees) enjoy the ability to express basically any finite computer program, in a decidable manner. I was ...
- 181
6
votes
3
answers
782
views
Boolean as subtype of integer
In languages oriented towards systems programming, digital logic and hardware design, it's common to treat boolean as a subtype of integer. In languages oriented towards mathematics and type theory, ...
- 307
6
votes
1
answer
766
views
Types which correspond to sets of cardinality of continuum
Are types which correspond to sets with cardinality of continuum possible in MLTT (or in any other constructive theory)?
On the first sight, they aren't, since elements of types are terms and we ...
- 1,762
6
votes
2
answers
440
views
Preservation under Substitution with Telescopes
In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution":
If $\Gamma \vdash v : \tau_1$ and $(x : \tau_1) \vdash t : \tau_2$,
then $\Gamma \...
- 2,832
6
votes
3
answers
587
views
Proving running time upper bounds for algorithms in dependent type theory
Proof assistants are a valuable tool for verifying
the correctness of proofs of mathematical theorems.
When dealing with proofs of correctness of algorithms,
one is not only interested on showing ...
- 1,072
6
votes
2
answers
710
views
With equirecursive types are there downsides to making all types potentially recursive?
By this I mean to ask, is it a bad idea to have all type constructor term expressions abstracted with $\mu$ just in case they need to be recursive? For example,
$Bool : Type;$
$Bool = (\mu Bool' ...
- 720
6
votes
1
answer
526
views
Defining inductive types in intensional type theory purely in terms of type-theoretic data
To define a (non-indexed) W-type all we need is a type $A:U$ and a function $B:A\to U$ and we get a type $W_{a:A}B(a)$. To check that this definition is valid we only need to check that the ...
user61651
6
votes
2
answers
300
views
Typing of substitution in a bidirectional type system
In most typed lambda calculi, we have the following lemma:
If $\Gamma \vdash t_1 : \tau_1$ and $\Gamma, x : \tau_1, \Delta \vdash t_2 : \tau_2$ then $\Gamma,\Delta[t_1/x] \vdash t_2[t_1/x] : \tau_2[...
- 2,832
6
votes
1
answer
605
views
Applications of Barendregt–Geuvers–Klop conjecture
I was learning about type systems from Benjamin C. Pierce's Types and Programming Languages and came across the Lambda cube in the chapter on Higher-Order Polymorphism. After reading up more about it ...
- 161
6
votes
3
answers
2k
views
How does type theory change how one thinks about programming?
I have been dabbling in HoTT and I am convinced that dependent type theory is much more suitable than set theory for proof assistants.
Now, this made me wonder - how fundamental is Type Theory ...
- 169
6
votes
1
answer
154
views
Is CoC inconsistent with cnat_ind axiom?
It is not possible to derive induction for Church-encoded datatypes on the Calculus of Constructions (source). Moreover, according to the accepted answer to another question, it is also not possible ...
- 3,137
6
votes
1
answer
799
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
299
views
Can a totality checker be used to guarantee a proof on the calculus of constructions + inductive types is correct?
If we extend the Calculus of Constructions with Fix, we gain a lot of expressivity for barely no added complexity. That includes being able to derive induction, perform large eliminations, prove ...
- 3,137
6
votes
1
answer
656
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
6
votes
1
answer
357
views
What type system fits the subclass of λ-terms that can be reduced optimally?
There is a subset of λ-calculus terms that can be reduced by Lamping's Abstract Algorithm without using the Oracle. That is an interesting subset, because only for those terms it is proven that ...
- 3,137
6
votes
1
answer
232
views
Structural equality of Pi Types with heterogeneous equality?
I'm trying to implement a proof of the following type:
...
- 2,832
6
votes
1
answer
169
views
Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?
To perform type inference in the presence of polymorphic recursion, one can use a Kleene-Mycroft iteration to compute the principal type of an expression. To type $\mathsf{fix}\ f\ldotp e$, we define $...
- 2,832
6
votes
1
answer
133
views
A function is lambda-2-definable iff it is HG computable and provably type correct in lambda-PRED2
I'm having a problem regarding Theorem 5.4.40.3 of Barendregt's Lambda calculi with types (1992), a chapter in Handbook in logic in computer science. (I'm referring to the PostScript version available ...
- 895
6
votes
1
answer
231
views
Typing relations terminology – how do I read typing relations?
I am currently trying to read up on type theory and have some quick questions on terminology.
In the following rule,
$$
\frac{x:T_1 \vdash t_2 : T_2}{\vdash \lambda x:T_1.t_2:T_1\to T_2}
$$
How ...
- 293
6
votes
1
answer
204
views
What is the general definition of 'extensionality' in type theory and how is extensionality defined for positive types?
It is well-known in the literature that (internal) extensionality of a function type means $(\prod_a f~a=g~a)\implies f=g$ (where $=$ is the intensional equality type) and extensionality of a product ...
- 965
6
votes
1
answer
267
views
What are the pros and cons for type cases in dependent type theories?
Pattern matching on $\cal U$ is allowed in XTT and Idris2 (for unerased types), and that implies the injectivity of type constructors (that's just my intuition, though -- I also wonder how do I prove ...
- 965
6
votes
1
answer
159
views
What arithmetical theorems can plain $\lambda \Pi$ reason about?
I've read that System F cannot state or prove theorems of the First Order Theory of Arithmetic. I assume this is because we lack dependent types, so we cannot explicitly express $\forall n:\mathbb{N}....
- 219
6
votes
1
answer
247
views
Decidability of rank-k polymorphism vs. System F
There's a paper by Kfoury from 1992, "Type Reconstruction in Finite Rank Fragments of
the Second-Order $\lambda$-Calculus", that proves that type inference for Curry-style rank-$k$ polymorphic lambda ...
- 325
6
votes
1
answer
353
views
Strong Normalization of Extended Calculus of Constructions (CC with cumulative universes)
There are some proofs around to prove the strong normalization of the calculus of constructions (i.e. that all type systems in the lambda cube are strongly normalizing). I have analyzed the proof ...
- 375