Questions tagged [type-theory]
Type structure is a syntactic discipline for enforcing levels of abstraction.
372
questions
16
votes
4
answers
2k
views
How can relational parametricity be motivated?
Is there some natural way to understand the essence of relational semantics for parametric polymorphism?
I have just started reading about the notion of relational parametricity, a la John Reynolds' ...
- 131
2
votes
0
answers
96
views
How to implement the next type inference algorithm?
Here I mean only simple typed Lambda calculus / Combinatory logic.
Notation: Combinatory logic terms: $F, X_i, Y_i$. Term application: $(F*X_1)$. Type variables $x_i,y_i$. Type assignment: $X:x_i$.
...
- 10.4k
3
votes
1
answer
107
views
Exposition of categorical models of type theory from type-theoretic perspective
Are there any formalizations or expositions of categorical models from type theoretic point-of-view? What I have in mind to get a better grasp of categorical models of dependent types, treating ...
- 31.8k
3
votes
0
answers
90
views
How far is the distance between Mahlo Universe and Mahlo Cardinal?
There seems to be some literature stating that Mahlo Universe[1][2] is the counterpart of Mahlo Cardinal in type theory, but I don't fully understand this point of knowledge.
More explicitly, I would ...
- 31
1
vote
1
answer
157
views
Defining normalization with respect to judgmental equality instead of reduction
In type theory with a type $\mathbb{N}$ of natural numbers (or some other base type such as booleans) and judgmental equality instead of reductions, canonicity is a meta-theoretical statement claiming ...
- 26.8k
2
votes
0
answers
82
views
Why Multiple Clocks in Guarded Dependent Type Theories?
The main purpose of clocks in guarded type theories (originating in Atkey & McBride ICFP 2013) is so that we can define coinductive constructions from guarded recursive definitions.
Semantically ...
- 1,494
10
votes
0
answers
130
views
Stratification of System Fω
I'm wondering if there's any update on this conjecture listed by Urzyczyn from years and years ago (I don't think that's its first appearance), which I'll restate below.
System Fω can be stratified ...
- 325
0
votes
1
answer
91
views
Is there a type theory system which includes an Any type
It's been a while since I read any type theory, so this might sound kind of dumb.
Anyway, if I look at examples of type systems, they all seem to be based around having an empty type, and then ...
- 356
7
votes
2
answers
384
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 ....
- 112
5
votes
2
answers
149
views
Commutativity of Clock Quantification and Disjunction/Existential Quantification in Guarded Type Theories
In Atkey & McBride ICFP 2013, they extend a simple type theory with guarded recursion indexed by clock variables $\triangleright^k$ and a clock quantification $\forall k. A$ that conveniently ...
2
votes
2
answers
202
views
What is the computational power of the Calculus of Constructions?
The calculus of constructions (CoC) without fix is clearly not Turing complete, as the program that loops infinitely cannot be expressed in it. What I'm wondering: ...
- 1,349
2
votes
1
answer
73
views
Question about "Free-ness" of Free SCWF
In Category with Family by Castellan et al., they introduce the concept of Free SCWF as correspondence of STLC with base type. Seemingly, they define Free B-SCWF as the synonym of initial B-SCWF.
My ...
- 1,494
1
vote
1
answer
51
views
Question in relating STLC and Free CCC
In Lambek's Intro to Higher Order Cat Logic, Chapter 1 Section 4 introduces the free construction (upon graph)
My question is, if I want to have STLC + (fake/incomplete) boolean type, how do I have ...
- 133
0
votes
0
answers
119
views
Boolean logic: What is the name of this trick to replace explicit negations by implications?
Consider a Boolean circuit $C$ composed of some finite set of input variables $A_1,\ldots, A_n$ and the connectives $\lor\land\neg\rightarrow$ (with $X\rightarrow Y=\neg X\lor Y$) (update: assume that ...
- 25
0
votes
0
answers
82
views
Type theory: Eliminating callback functions?
Consider a type theory such as the one developed in Chapter 1 of the HoTT book, or similar. In fact, I am currently only interested in the types that can be constructed from a collection of elementary ...
- 25
0
votes
0
answers
45
views
What does impredicativity mean in substructural and co-intuitionistic logics?
Predicative foundations puts restrictions on power sets and function sets.
Entirely apart from the philosophy predicative theories are a lot easier to prove things about and this sounds interesting to ...
- 123
5
votes
1
answer
179
views
How do we use directed univalence in directed type theory?
In directed type theory of Riehl and Shulman, we have a new type, $hom_A\:x\:y$ representing arrows between elements $x$, $y$ of type $A$, note that these are not a priori functions.
I will call the ...
- 667
6
votes
1
answer
142
views
Is there a way to define dependent types without explicit substitutions internally within agda?
I am playing around the Programming Language Foundations in Agda exercises and wondering if we can achieve the same level of theories with dependent types. With simple types, the definition usually ...
- 251
9
votes
2
answers
476
views
Induction-recursion in models other than $\mathbf{Set}$
It is well-known that various flavors of induction-recursion are consistent*. Typically, this is proven by showing that the standard model of type theory in sets can be extended to include induction-...
- 26.8k
8
votes
3
answers
664
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 ...
- 123
7
votes
0
answers
119
views
For which type systems have normalizaton proofs been formalized?
I am trying to understand what the open problems are in the area of formalizing proofs of normalization for type systems.
Obviously STLC has been done many times.
For predicative System F, I found one ...
- 171
11
votes
1
answer
592
views
Swapping arguments of variables in higher-order pattern unification
Pattern unification is a simplified form of higher-order unification in which existential variables only appear applied to distinct universal variables. Thus, for instance, an equation such as $M \,x\...
- 1,349
10
votes
2
answers
406
views
What are the issues with a set-like interpretation of quantifiers in type theory?
In his answer to a question that tries to treat universal and existential quantifiers as intersections and unions of sets, Andrej Bauer says:
Forget the intersections and unions. People get this idea ...
- 26.8k
8
votes
4
answers
304
views
Type theory and fixed points of datatypes
For the purposes of this question, say that a datatype is a type constructor with one type parameter (this is sometimes called a type operator).
In Haskell, we can define a fixed point ...
7
votes
1
answer
326
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 ...
- 5,444
0
votes
0
answers
145
views
What is wrong with the "obvious" approach to function extensionality by providing context-aware rewrites?
There is an obvious, dirty and probably wrong approach that allows one to prove function extensionality in a straight-forward manner: provide an equality primitive with a context-aware rewrite. For ...
- 3,045
9
votes
2
answers
406
views
Why is the Curry-Howard isomorphism?
The Curry-Howard isomorphism is the correspondence between type systems (like for the simply typed lambda calculus) and proof systems (like natural deduction). More precisely, types resemble ...
- 7,485
4
votes
1
answer
171
views
Effect of HoTT/Univalence Axiom on equality between terms of inductive types?
It is well known that Univalence contradicts Axiom K,
for example there are two ways $\mathbf{2} = \mathbf{2}$ may be proved using Univalence, via $\mathtt{id}_{\mathbf{2}}$ or $\mathtt{not}$.
But ...
- 26.8k
6
votes
1
answer
177
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 ...
- 4,511
4
votes
1
answer
680
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
22
votes
1
answer
4k
views
Prove proof irrelevance in Coq?
Is there a way to prove the following theorem in Coq?
Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.
EDIT: An attempt to give a brief ...
- 923
3
votes
2
answers
291
views
How does axiom K contradict univalence?
I have seen it claimed several times that axiom K is inconsistent with univalence (e.g. here and here), but I have never seen a proof sketch. Specifically, I'm curious about how this manifests in the ...
10
votes
3
answers
407
views
Does the order of declarations in an inductive type matter?
I was wondering if the order of declarations of an inductive type can matter.
For example in Coq you can define Nat either by:
...
- 923
3
votes
2
answers
515
views
Constructing terms of function types out of the empty type
If a function $f$ is understood as its graph, i.e. a set of pairs $\langle x,y\rangle$ where $x$ is input and $y$ is output, then the empty set $\emptyset$ is a valid function, and for any set $A$, we ...
- 111
1
vote
1
answer
102
views
Are coproduct types redundant in presence of natural numbers and $\Sigma$-types?
In the homotopy type theory book section A.2.5 defines $\Sigma$-types, A.2.6 coproduct types and A.2.9 the natural numbers type.
If we already have $\Sigma$-types and the natural numbers type can we ...
- 26.8k
44
votes
4
answers
4k
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 ...
7
votes
0
answers
176
views
$\lambda$-definability and structure preserved by homomorphisms
I imagine there are some standard results that bear on this, but I'm having trouble finding a proof or refutation of it.
Some prelimary definitions.
A Henkin structure $A = (A^\cdot, ⟦\cdot⟧_A)$ for ...
- 433
8
votes
2
answers
379
views
What's the categorical semantics of definitional equality?
The categorical semantics of a dependent type theory is normally described as a CwA/CwF/CompCat/etc. and in these models, we can talk about propositional equality by interpreting an 'identity type'. ...
- 1,349
6
votes
3
answers
1k
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 ...
- 243
2
votes
2
answers
187
views
What is the point of the eliminator for the unit type?
In the HoTT book p. 436 A.2.8 the eliminator $\mathrm{ind}_{\mathbf{1}}$ for the unit type is described.
What is the point of it? What if you did not introduce it and instead just replaced all the ...
- 923
5
votes
1
answer
121
views
$\eta$-reduction not locally confluent on well-typed terms
This paper says: "In the presence of a unit type, $\eta$-reduction is not even locally confluent on well-typed terms [20]."
[20] is a reference to a 300-page book with no further details and ...
- 31.8k
2
votes
0
answers
70
views
Reference request: characterisation of simultaneous substitution
For simply typed λ-calculus, a simultaneous substitution from $\Gamma$ to $\Delta$ is concretely a type-preserving map from variables in $\Delta$ to terms in $\Gamma$. See, for example, Programming ...
- 121
9
votes
0
answers
180
views
Constructive Strong Normalization of the Extended Calculus of Constructions
The extended calculus of constructions (ECC) is basically the calculus of constructions with cumulative universes. I use the definition which Zhaohui Luo used in his PhD theses which contained a proof ...
- 365
3
votes
1
answer
164
views
2
votes
1
answer
105
views
External failure of law of excluded middle in Martin-Löf type theory
Is there an explicit type $T$ in Martin-Löf type theory such that $(T\to \mathbf{0})\to\mathbf{0}$ has an explicit closed term and $T$ can be shown externally to not have closed terms?
- 1,349
11
votes
1
answer
477
views
Is there a good notion of non-termination and halting proofs in type theory?
Constructive type theory with its basic interpretation under the curry howard correspondence consists only of total, computable functions. In the literature, some has been said on using "computational ...
1
vote
0
answers
93
views
CubicalTT: successor of add proof?
Lecture 2 of the cubical type theory lectures provide a proof of
(suc a) + b = suc (a + b):
...
- 565
2
votes
1
answer
198
views
Alternatives to Normalization by Evaluation
Reading about lambda calculus I got the impression that normalization is evaluation.
So I don't understand what is meant by Normalization by Evaluation (used e.g. in several publications of A. Abel).
...
- 13.3k
6
votes
1
answer
215
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 ...
- 31.8k
2
votes
0
answers
79
views
MLTT/MiniTT: why do normal forms of sum types carry environments?
I am learning how to implement MiniTT: a simple type theoretic language, which is a dependently typed language with sum types, mutual recursive/inductive definitions and a universe of small types.
A ...
- 565