Questions tagged [type-theory]

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

Filter by
Sorted by
Tagged with
5
votes
1answer
315 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 ...
5
votes
1answer
422 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 ...
5
votes
1answer
504 views

Can all linear lambda calculi be linearity checked syntactically?

Given a lambda calculus with explicit linearity and usual application and abstraction, can the linearity check be done on an untyped syntax tree if we keep track of the structural types? Are the ...
5
votes
1answer
178 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 ...
5
votes
2answers
211 views

What's the point of stack judgement in CBPV?

Call-by-push-value (CBPV) introduces two main families of types, values and computations, and their corresponding judgements. However, in some extensions/variants/adaptation of CBPV, there is a third ...
5
votes
1answer
171 views

What's the difference between proving weak normalization and implementing evaluator?

Implementing an normalization (cut elimination) procedure for a type system A in a language with a total type system B, automatically proves cut elimination for type system A since the implementation ...
5
votes
1answer
249 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 ...
5
votes
2answers
349 views

Is there a "lambda cube" for interaction nets?

The lambda calculus is an untyped language that is often extended with logical frameworks such as the vertices of the λ-cube. Is there something similar to it, but for interaction nets? What about ...
5
votes
1answer
171 views

Nested automatization of type inference of forall elimination

Following a previous question about how to automatize the type inference in a forall elimination of an application, now suppose we want to do the same but for a nested forall, say $(\Lambda X_1.\...
5
votes
1answer
116 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 ...
5
votes
1answer
295 views

Can a term on normal form prove an illogical assertion?

Suppose we take a language such as Agda and disable the features that make it consistent; for example, universe polymorphism, structural recursion checks and similar. Suppose then that we take a term ...
5
votes
1answer
120 views

Logics for timed resource control

I'm studying proof theory and I've seen that linear logic can be used as a way to control resource usage, since by the propositions-as-types it is equivalent to the linear lambda calculus. Is there a ...
5
votes
1answer
121 views

Definitional function extensionality for functions out of $\mathbf{2}$

Denote by $a$ and $b$ the canonical terms of $\mathbf{2}$. For any map $f:\mathbf{2}\to \mathcal{U}$ we have the eliminator$$\mathrm{ind}_{\mathbf{2}}(f) : \big(f(a) \times f(b)\big) \to \prod_{x:\...
5
votes
0answers
151 views

On the interpretation of coinduction in type theory

The notion of (co)datatype can be modeled satisfactorily in category theory as fixed-points of polynomial functors. Then, (co)induction principles are derived from initial algebras/terminal ...
5
votes
0answers
440 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 (...
5
votes
0answers
257 views

Commonalities and differences between canonical structures and the implicit calculus

There is a paper on The Implicit Calculus as a generalization of type classes. Coq's canonical structures are also a generalization of type classes. The paper does not mention canonical structures ...
4
votes
2answers
189 views

What is the first name of Bainbridge?

Bainbridge coauthored the paper `Functorial Polymorphism' with Freyd, Scedrov and Scott (DOI). What is his/her first name?
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. ...
4
votes
1answer
486 views

Rules about Prop and Set in UTT

In Luo's UTT (type theory which is used in Agda, Idris, and other dependently typed programming languages), there're are two rules for $\Pi$ types. One for $\mathsf{Prop}$ and one for $\mathsf{Set}$. ...
4
votes
1answer
488 views

Church-style CoC with axiom for induction over Church-encoded unit, is it consistent?

If we start with the Calculus of Constructions, and then use the following definitions for the Church-encoded Unit: ...
4
votes
1answer
134 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
1answer
219 views

Why isn't it "enough" to prove induction with one extra "INat" argument?

It is well known that it is impossible to prove the induction principle for Natural numbers on the Calculus of Constructions. That is, ...
4
votes
1answer
166 views

What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?

In the context of constructive type theory, a term inhabiting some type is said to be in canonical form if it is explicitly built up using the constructors of that type. Particularly, the only ...
4
votes
1answer
139 views

Is there a simple algorithm for proof search on CoC?

Given the usual Calculus of Constructions with an extra primitive, _, that stands for "attempt to fill this location in a way that type-checks", is there any simple/...
4
votes
2answers
110 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 ...
4
votes
1answer
260 views

Is it possible to verify a typechecker for a total dependently-typed language in that language's logic?

I understand the diagonalization argument against implementing an eval function in a total language, and that typechecking in a dependently typed language requires ...
4
votes
1answer
97 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 ...
4
votes
1answer
428 views

Featherweight Generic Java formalization in Coq

I've been searching for some nice formalization of FGJ (Featherweight Generic Java) in Coq. I am going to develop an extension of FGJ in Coq, so I hope there is an appropriate Coq implementation which ...
4
votes
1answer
133 views

Rendering of type-level computation

Programming languages with dependent types and/or higher-kinded types feature what might be called compile-time computation at the type-level. This is usually defined as follows (I'm omitting some ...
4
votes
1answer
580 views

Generalization and instantiation of types in Hindley-Milner type inference

I’m currently reading Heeren, B., Hage, J., & Swiestra, D. (2002). Generalizing Hindley-Milner Type Inference Algorithms in an attempt to understand Hindley-Milner-style type inference. I'm ...
4
votes
1answer
125 views

Is the church-style affine calculus of constructions with unrestricted recursion consistent?

Suppose we take the church-style calculus of constructions, except with affine functions (variables must occur at most once) and mutual recursive definitions. For example: ...
4
votes
0answers
149 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 ...
4
votes
0answers
80 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
152 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 ...
4
votes
0answers
161 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 ...
4
votes
0answers
153 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 ...
4
votes
0answers
183 views

Implementations of Dependent Type Theory

I am trying to find a minimal implementation of dependent type theory that supports Pi Types (obviously) Modules containing records Inductive data types Universe Hierarchy A notion of equality ...
4
votes
0answers
195 views

Is my understanding regarding how to implement Quotient Types correct?

I was trying to understand Quotient Types, and determine if Self-Types can be used to implement them. From a Reddit post, Here is an example and explanation that may be more familiar to non-...
4
votes
0answers
102 views

Proof that CIC or Dybjer-style eliminators are strongly-normalizing?

Related to this question I'm wondering, what is the standard technique for showing that dependent types with eliminators are strongly normalizing? I'm thinking something like the Calculus of ...
4
votes
0answers
143 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 ...
4
votes
0answers
412 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
498 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: ...
4
votes
0answers
132 views

Completeness of realizability semantics for higher-order type theory

In this answer I mention a paper by Geuvers in which he describes a class of models for a type theory $\lambda P_2$ which is a sub-system of the CoC and roughly corresponds to 2nd order predicate ...
4
votes
0answers
83 views

Coherence spaces and full completeness for the implicative fragment of linear logic

Linear logic isn't complete for coherence space semantics since $1$ and $\top$ get identified. But it is, I believe, complete for the fragment of linear logic whose only connective is $\multimap$. I ...
4
votes
0answers
259 views

Modeling union types using sum types

It is trivial to model sum types using only union types and product types: simply add a discriminant. $A + B \cong (0 \times A) \cup (1 \times B)$. What I am wondering is whether or not there is a ...
4
votes
0answers
308 views

Subtyping rules for extension of System $F_\omega$ with subtyping and kind-level variance tracking

I need an extension of System $F_\omega$ with subtyping, and where the variance of type constructors is reflected in their kind. Unfortunately, System $F^\omega_{<:}$, as defined in chapter 31 of ...
4
votes
0answers
322 views

Category theory in plain MLTT

I want to define a category in simple MLTT (not in HoTT). I defined it with the help of setoids. I.e. category consists of: a type of objects with equivalence relation (Obj : Set) a type of arrows ...
4
votes
0answers
196 views

Type-and-effect systems, stochasticism and effect squelching: how about quicksort?

There's a feature of Haskell's type system which bugs me: you can't implement a randomized sorting algorithm without the use of randomness spilling out into all of its callers. That seems undesirable....
3
votes
4answers
340 views

Philosophy behind monotonicity requirement for inductive types

Is there a good philosophical reason for why inductive types with negative occurrences or non-monotonicity should not be considered valid constructions? According to my understanding of the Bishop/...
3
votes
2answers
350 views

Type a variable-argument function?

Is it possible to type a variable-argument function? EDIT: like those defined in Scheme.

1
3 4
5
6 7