Questions tagged [type-theory]

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

Filter by
Sorted by
Tagged with
-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
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 ...

1
2 3 4 5
7