# Questions tagged [type-theory]

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

287 questions
Filter by
Sorted by
Tagged with
85 views

123 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?
71 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 ...
111 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 ...
472 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: ...
55 views

### Sample Terms in System Omega

I've been implementing mini languages that fall into each corner of the Lambda Cube. My main reference for this has been Types and Programming Languages. The latest one I finished is System Omega. I ...
155 views

### Non-termination, strict positivity and free monads

Using the standard encoding of a free monad in Haskell and its fmap instance: ...
128 views

### From Church-encoding to induction principle

I am looking for an algorithm to go from a Church-encoded datatype to their induction principle in the Calculus of Constructions. For example: ...
113 views

### Extensional type theory and function extensionality

Is the principle of function extensionality $(\forall x. f(x) = g(x)) \implies f = g$, derivable from ETT? Most notably is this derivable in Agda with axiom K?
185 views

### Which types are nihilistic?

[Note 2020-02-08: I updated the definition of nihilistic types so that it relies less on the type Empty.] A discussion on Twitter prompted the following question, ...
115 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 ...
101 views

### Type of induction principle for fixpoint types

To the Calculus of Constructions we could add a general fixpoint type constructor (accepting inconsistencies or assuming F is a ...
125 views

### Set:Set or Negative Inductives in a Total Language?

In total dependently typed languages, general recursion is forbidden, since this can allow for non-terimination. However, dependently typed language can still describe Turing-complete computations (...
104 views

288 views

### How do continuations represent negations (under the Curry–Howard correspondence)?

Under the Curry–Howard correspondence, types can be thought of as propositions, and values inhabiting a type can be thought of as proofs that the corresponding proposition is true. (E.g., the ...
119 views

### Verified type checkers

Most of the work on programming language metatheory mechanization focus on the declarative properties of the languages (e.g., type soundness), but fail to address the algorithmic side, i.e. the type ...
3k views

### Why colon to denote that a value belongs to a type?

Pierce (2002) introduces the typing relation on page 92 by writing: The typing relation for arithmetic expressions, written "t : T", is defined by a set of inference rules assigning types to ...
407 views

### Applications of algebraic geometry in type theory/programming language theory

Lately, I have become interested in algebraic geometry and have started reading on it. I still know very little about this field, but I do want to know if it has any connection with my main field, ...
222 views

### Can Isorecursive types capture mutually recursive data types?

I've been reading TAPL, and reached the section on recursive types. I understand the type operator $\mu$. For example, the two type expressions are equivalent ...
277 views

### Intuition Behind Strict Positivity?

I'm wondering if someone can give me the intuition behind why strict positivity of inductive data types guarantees strong normalization. To be clear, I see how having negative occurrences leads to ...
165 views

### What will go wrong if a recursive record type has a negative eta rule?

In the context of Agda like dependent type theory: This short paper https://jesper.sikanda.be/files/vectors-are-records-too.pdf says some inductive type can be seen as records, for example ...
260 views

### Extending Hindley-Milner to type mutable references

I have been trying to implement a programming language from scratch, and have gotten reasonably far. It reads just like Python, other than the fact that let is used ...
133 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/...
127 views

### Definitional equality of recursive function definition by “infinite unfolding”

The context is checking definitional equality in dependent type theory implementations. Consider in Coq ...
96 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 ...
149 views

### Is it possible to check equality of equi-recursive types, or recursive λ-terms?

Can we determine if two λ-terms are equal? Given two lambda terms, let's say they are equal if their (possibly infinite) Bohm trees are. Under this definition, for example, ...
140 views

### Universe polymorphism: the inference of universes and their constraints

When making a universe polymorphic definition in Coq, universes and their constraints are automatically inferred. Are they somewhat the most general ones (in a sense similar to the principal type ...
138 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 ...