Questions tagged [type-theory]
Type structure is a syntactic discipline for enforcing levels of abstraction.
323
questions
-1
votes
0answers
19 views
Reasoning about subtyping in type theory
I recently heard a lecture by Thorsten Altenkirch where he pointed out that set union and intersection are "evil" operations since they depend on elements. I think he also linked ...
1
vote
0answers
80 views
Is just one W-type enough for formalizing mathematics?
We work in intensional Martin-Löf type theory with $0$, $1$, $2$, $\Pi$, $\Sigma$, $W$ and a cumulative hierarchy of universes. Suppose our goal is to formalize constructive mathematics.
Now if we ...
2
votes
0answers
121 views
Set-theoretic encoding of functions in type theory
Functions usually get encoded in set theory as follows. A function $A\to B$ is a subset $f\subset A\times B$ such that $\pi_1:f\to A$ is a bijection.
In type theory to give a function $A\to B$ is to ...
2
votes
1answer
84 views
Dependent eliminator for empty type in intensional Martin-Löf type theory
In calculus of inductive constructions you can just say that the empty type is the type with no constructors and it automatically builds the dependent eliminator.
But let's say I'm setting up ...
0
votes
0answers
52 views
How much type information do Hindley-Milner proof assistants need to remain sound?
A known benefit of the HM type system is that you can usually infer a term's most general type with no user-provided type annotations. For example, if my theory contains the standard axiom: $$\forall ...
1
vote
2answers
81 views
Explicit type system with infinite non-cumulative universe hierarchy
Is there an open-source proof assistant or at least an explicit set of rules written down somewhere for a type system with an infinite non-cumulative universe hierarchy and unique typing?
I want to ...
0
votes
0answers
46 views
Complexity of finding typing derivation trees
In type theories where type checking is decidable do we have estimates for how much time/space it takes to find a typing derivation tree of a valid typing judgment? Do any published references do this ...
2
votes
0answers
54 views
What is the relation of parametricity and function extensionality?
In Agda function extensionality can be defined like this:
funExt = {A : Set} {B : Set} {f1 f2 : A → B} → (∀ x1 x2 → x1 ≡ x2 -> f1 x1 ≡ f2 x2) → f1 ≡ f2
One may ...
2
votes
2answers
120 views
$\mathbb{N}$ in intensional MLTT with judgmentally commutative $+$ and $\times$
Is there a way to implement natural numbers in intensional Martin-Löf type theory so that addition and multiplication is judgmentally commutative?
13
votes
3answers
899 views
“Guarded” negative occurrences in definition of inductive types, always bad?
I know how some negative occurrences can definitively be bad:
...
3
votes
1answer
109 views
Model of MLTT with $\eta$ rule where function extensionality fails
Consider intensional Martin-Löf type theory with judgmental $\eta$ rule for dependent product types. Is there a model of it where function extensionality fails?
4
votes
0answers
138 views
Model of homotopy type theory where propositional & judgmental equality coincide for closed terms
In intensional Martin-Löf type theory we can prove the metatheorem that two closed terms are propositionally equal iff they are judgmentally equal.
Is there a non-empty model of homotopy type theory ...
2
votes
1answer
70 views
Normal term of double negation of W-type
Consider the intensional Martin-Löf type theory without axiom of choice or the law of excluded middle.
Let $A:U_0$ be a type and $B:A\to U_0$ be a function such that $\Sigma_{a:A}(B(a)\to 0)$is ...
5
votes
1answer
261 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 ...
3
votes
1answer
137 views
Defining binary natural numbers without quotient types
Let's say we work in a dependent type theory with W-types and we want to have a type for binary natural numbers. We don't want to add quotient types or higher inductive types to the system.
How to ...
2
votes
1answer
86 views
Typing inference as a map on abstract syntax trees
Is there a reference that explains typing inference for Martin-Löf type theory as a computable map from abstract syntax trees of terms to abstract syntax trees of types? I don't want to identify non-...
3
votes
1answer
78 views
Relating functors to relational functors with the parametricity translation
$\newcommand{\Type}{\text{Type}}\newcommand{\id}{\text{id}}\newcommand{\map}{\text{map}}$
In attempting to answer the question: Rigorous proof that parametric polymorphism implies naturality using ...
2
votes
1answer
63 views
Surjection from a type to a universe
We work in homotopy type theory. Can there be a type $A:U_m$ and a map $f:A\to U_n$ for some $n\geq m$ such that the type $\prod_{T:U_n} \|\mathrm{fib}_f(T)\|$ is inhabited?
5
votes
1answer
162 views
Choose term of coproduct type
We work in homotopy type theory. Denote the propositional truncation of a type $A$ by $\|A\|$ and the function type between types $A$ and $B$ by $A \to B$.
Can you construct a term of the following ...
7
votes
1answer
357 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?
4
votes
0answers
71 views
Relative consistency of various Martin-Löf style type theories
I am wondering about relative consistency of various Martin-Löf type theories, when compared to one another, I will use MLTT for the intensional Martin-Löf type theory with $\Pi$, $\Sigma$, $\mathbb{N}...
4
votes
0answers
339 views
What is the proof for the inconsistency of impredicativity + excluded middle + large elimination in type theory
Why is the combination of
impredicativity + excluded middle + large elimination
inconsistent in dependent type theory?
My understanding of large elimination is I am doing large elimination if I am ...
4
votes
0answers
138 views
What logic do refinement types correspond to?
I'm interested in applicability of refinement types to theorem-proving hence the questions about their logical expressiveness. Let's say, we have a type system which corresponds to some logic ...
3
votes
1answer
124 views
Structural normalization algorithm for the simply typed lambda calculus
I would like to know if there is a (piecewise) structural normalization algorithm for the simply typed lambda calculus. By structural I mean a recursive function that only calls itself on subterms of ...
7
votes
1answer
106 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 "...
0
votes
0answers
70 views
What do we call a type system where any term of any type ultimately parses down to $*:\mathbf{1}$?
If a type system allows inductive types (as in e.g. Coq) then we can coin new primitive constants that inhabit types. For example $0:\mathbb{N}$ is constructed when defining $\mathbb{N}$ and does not ...
4
votes
1answer
86 views
Context weakening as an explicit rule for languages of the the lambda cube?
I'm trying to formalize the syntax and typing judgments of the Calculus of Constructions in Coq. I'm choosing to use the Pure Type Systems presentation of CoC; however, I've seen mild variations in ...
6
votes
2answers
232 views
Intuition behind nested positivity and counterexamples
I'm looking at the nested positivity conditions for inductive types stated in the Coq manual. First off, are there any other references (not necessarily for Coq, but in dependent type theories ...
33
votes
5answers
10k views
What are some good introductory books on type theory?
I'm recently studying Haskell and programming languages. Could someone recommend some books on type theory?
8
votes
2answers
443 views
Can factorial be encoded in the Kappa-calculus with fixed point operator?
Suppose we have a $\kappa$-calculus with operator $fix$, that could be used to transform function with type $(1 \rightarrow a) \rightarrow a$ to a value of type $1 \rightarrow a$. We use a normal ...
0
votes
2answers
192 views
Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?
I've been curious about the 'geometric situation' that one has when considering the type
$\prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$.
Here, addition is defined in the ...
3
votes
0answers
83 views
Request for an update on a discussion about coinductive types in HoTT (or anywhere else)
Googling something else I stumbled on a conversation titled "coinductives" initiated by Vladimir Voevodsky on Google groups in 2014. It lasted for three days, invloved a dozen people, and ...
5
votes
3answers
201 views
Is it possible to create a “quote” function that, given a native λ-term, returns its λ-encoded representation?
Suppose we implement the λ-calculus inside the λ-calculus itself with λ-encodings and Bruijn indices:
...
12
votes
1answer
652 views
Can we derive Cubical Type Theory from Self-Types?
Self Types are known for being a simple extension to the Calculus of Constructions that allow it to derive all inductive datatypes of a proof assistant like Coq and Agda, without a "hardcoded&...
6
votes
0answers
99 views
Is there a known notion of “stochastic dependent pair”?
I came upon this when thinking about the semantics of probabilistic programs. Say you have a generative model
N ~ Poisson()
for n = 1:N
X[i] ~ Normal()
Then the ...
1
vote
0answers
91 views
λProlog vs HiLog
λProlog is a well-known higher-order logic programming language.
On the other hand, HiLog is described as a logic programming language with higher-order syntax, but first-order model theory.
Do I ...
2
votes
2answers
271 views
Uncountability in intuitionistic logic
I've read snippets here and there that inside intuitionistic logic, uncountable can be a subset of the naturals ?
What is the correct intuition to think about this? Andrej Bauer replied above, saying ...
-2
votes
1answer
75 views
Forming ordered pairs using monads and doing without the Kuratowski encoding of ordered pairs
Suppose we have a set $S$ of constants of the Simply-Typed Lambda Calculus (STLC) various types, and the operation of union $\cup$ which takes two constants and forms their union.
For example, $S$ ...
4
votes
0answers
156 views
Is full ownership inference possible?
Rust is famous for its ownership type-system, but requires the programmer to annotate ownership in function signatures. Is it possible to do full program inference of ownership, without any ...
3
votes
1answer
190 views
Why would the term “dynamically typed” be considered a misnomer?
In the book "Types and Programming Languages", the author writes:
The word "static" is sometimes added explicitly - we speak of a "statically typed programming language",...
4
votes
2answers
97 views
What is the relation of HOL Light type theory and some of the intuitionistic type theories?
I'm trying to understand how HOL Light deductive rules relate to mainstream intuitionistic type theories.
Here is a sample of questions that come to my mind.
Does ...
3
votes
1answer
76 views
Why REFL rule is primitive in HOL Light?
HOL Light
assumed REFL as a primitive.
Why does it need to do so?
Can't REFL rule be deduced in this way using ...
3
votes
0answers
116 views
Would it be possible to derive `transp` natively from Path, Interval and typecase?
Assume for a moment that we extended Agda with an Interval and a Path type, but not transp (which is a primitive currently). I'm ...
6
votes
1answer
133 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}....
2
votes
1answer
167 views
Defining finite sets inductively in a proof assistant?
To represent finite sets within coq, we either use something like ListSet, which are just definitions on top of list, or we ...
6
votes
0answers
140 views
Postulating self types in a proof assistant
Self types introduce two typing new rules (simplified):
$
\frac{\Gamma \; \vdash \; t : [t/x]T}{\Gamma \; \vdash \; t : \iota x. T}$ I-self and
$
\frac{\Gamma \; \vdash \; t : \iota x. T}{\Gamma \; \...
4
votes
2answers
185 views
Well-formedness condition for inductive types
I work on implementing a simple dependently typed language. I want to implement inductive types there. However, I want them to be well formed. From what I've seen in Coq not all types are acceptable. ...
3
votes
0answers
131 views
Weakest model of computation that can typecheck?
What's the weakest (known) model of computation (or smallest language class) that can decide whether a simply-typed lambda calculus program type checks? What about an (explicitly typed) CoC program?
5
votes
1answer
95 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 ...
4
votes
0answers
130 views
Rules between UIP with function extensionality and univalence
I am wondering if there are any interesting rules/judgemental equalities, denoted $A$, which satisfy the following properties:
$iMLTTfe+UA \implies \neg A$
$iMLTTfe+UIP \implies \neg A$, or more ...
