Questions tagged [type-theory]

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

Filter by
Sorted by
Tagged with
0 votes
0 answers
12 views

What is an efficient algorithm to check for equivalence on symmetric interaction combinators?

Symmetric interaction combinators are a graph-rewriting model of deterministic computation derived from Lafont's interaction nets. In the paper "Observational Equivalence and Full Abstraction in ...
MaiaVictor's user avatar
  • 3,077
3 votes
1 answer
120 views

Is there an efficient algorithm to check for duplicator-invariant equivalence on symmetric interaction combinators?

Consider the 3 symmetric interaction combinator nets below: Despite being different nets, they are equal, in the sense that, if we view white nodes as lambdas and applications, and black nodes as ...
MaiaVictor's user avatar
  • 3,077
12 votes
4 answers
1k views

Where is the model theory in programming language theory?

I have a background in mathematical logic and am trying to learn some programming language theory. In the syntax of, say, first-order logic, one of the first distinctions you learn about is between ...
Siddharth's user avatar
  • 693
1 vote
1 answer
178 views

Type of the Recursor in Lean

I need some help working through the type of the recursor, the eliminator for the inductive type. If $F=\forall a::\alpha.\mathsf{U}_\ell$ $P=\mu t:F.K$ $K=\sum_c(c:\forall b::\beta.tp[b])$ $u::\...
Alex Byard's user avatar
-1 votes
1 answer
52 views

Typing rule for corresponding `val` and `let` bindings

$\newcommand{\clet}{\texttt{let }} \newcommand{\cval}{\texttt{val }} \newcommand{\cin}{\texttt{ in }} $I have the syntax for a programming language containing both let-bindings of the form $\clet x = ...
llilibbou's user avatar
1 vote
1 answer
63 views

Intuition behind UTT's internal logic

The "internal logic" of type theory UTT is defined in LF as follows: What's the intuition behind this definition? I can kind of understand the declaration of the the first three constants - ...
user175254's user avatar
1 vote
0 answers
33 views

Confusion about $T$ and $El$ when defining universes in LF

This is a technical follow-up question to Formulation of Tarski-style universes in LF Consider LF, the logical framework used to define UTT (unified theory of dependent types). The next two quotes ...
user175254's user avatar
1 vote
1 answer
75 views

Formulation of Tarski-style universes in LF

Lately I've been asking questions on type theory on MSE, and I've been getting great answers, but I decided to give a try to this site and see if it will be helpful as well. I'm looking at this note ...
user175254's user avatar
4 votes
2 answers
290 views

Lambda-calculus: Beta-equivalent terms have the same type

In the simply-typed lambda calculus, how do you prove that: If two terms are beta-equivalent, then they have the same type? My guess is that I should use the subject reduction, and maybe the ...
Bob's user avatar
  • 371
4 votes
1 answer
80 views

Free type variables in Hindley-Milner type inference

I'm trying to understand how generalization works in H-M type inference. In order to generalize a function, we: Collect all the free type variables in the type of the function body, Subtract away any ...
Brian Berns's user avatar
6 votes
0 answers
99 views

List Functions That Don't Depend on Length

Intuitively, a polymorphic function of type $f : \forall a. [a] \to [a]$ cannot inspect the type of its elements. This intuition can be captured formally using either natural transformations or ...
vigenary's user avatar
5 votes
1 answer
169 views

Stronger "induction" principles than induction-recursion

Are there type theories in the literature with "induction" principles stronger than induction-recursion? This answer gives System F as an example of a theory stronger than MLTT + induction-...
technosentience's user avatar
5 votes
1 answer
175 views

The precise definition of Normalization By Evaluation?

The Wikipedia article suggests that NbE is a technique for obtaining "the normal form of terms" by translating the object language into abstractions of the meta (host) language: The ...
Hirrolot's user avatar
1 vote
0 answers
63 views

Interpretation of the degree of a redex

In Girard Proofs and Types, The degree of a type is defined as follows $$\begin{align*}\partial(T_i)&=1\text{ if }T_i\text{ is atomic}\\\partial(U\times V)=\partial(U\rightarrow V) &=\max(\...
Sam Ezeh's user avatar
5 votes
1 answer
247 views

Dependent type theory and definitions of cumulativity

Many dependent type theories employ an universe hierarchy to compensate for the fact that Type : Type is inconsistent (due to Girard's paradox). A cumulativity relation is then defined to lift terms ...
Qiancheng Fu's user avatar
2 votes
0 answers
133 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$. ...
Oleg Dats's user avatar
  • 121
3 votes
1 answer
142 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 ...
Nift's user avatar
  • 841
3 votes
1 answer
158 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 ...
Ember Edison's user avatar
1 vote
1 answer
167 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 ...
Nift's user avatar
  • 841
2 votes
0 answers
105 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 ...
Max New's user avatar
  • 1,548
10 votes
0 answers
148 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 ...
ionchy's user avatar
  • 325
0 votes
1 answer
101 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 ...
user3113723's user avatar
5 votes
2 answers
177 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 ...
Max New's user avatar
  • 1,548
2 votes
2 answers
267 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: ...
Jonathan's user avatar
2 votes
1 answer
77 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 ...
EDJ's user avatar
  • 133
1 vote
1 answer
59 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 ...
EDJ's user avatar
  • 133
0 votes
0 answers
126 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 ...
Duyal Yolcu's user avatar
0 votes
0 answers
84 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 ...
Duyal Yolcu's user avatar
0 votes
0 answers
60 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 ...
Molossus Spondee's user avatar
5 votes
1 answer
266 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 ...
Nift's user avatar
  • 841
6 votes
1 answer
174 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 ...
Kaa1el's user avatar
  • 163
10 votes
2 answers
547 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-...
daniel gratzer's user avatar
8 votes
3 answers
716 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 ...
paulotorrens's user avatar
7 votes
0 answers
132 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 ...
while1fork's user avatar
11 votes
1 answer
651 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\...
Mike Shulman's user avatar
10 votes
2 answers
431 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 ...
Jozef Mikušinec's user avatar
8 votes
4 answers
390 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 ...
Nift's user avatar
  • 841
0 votes
0 answers
156 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 ...
MaiaVictor's user avatar
  • 3,077
7 votes
1 answer
422 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 ...
Alvaro P.'s user avatar
  • 173
4 votes
1 answer
182 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 ...
Guest0x0's user avatar
  • 151
9 votes
2 answers
517 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 ...
JoJoModding's user avatar
6 votes
1 answer
191 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 ...
ice1000's user avatar
  • 945
3 votes
2 answers
379 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 ...
Grant Jurgensen's user avatar
1 vote
1 answer
107 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 ...
yelena's user avatar
  • 11
7 votes
0 answers
183 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 ...
Andrew Bacon's user avatar
8 votes
2 answers
459 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'. ...
ice1000's user avatar
  • 945
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 ...
Arjo's user avatar
  • 169
2 votes
2 answers
197 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 ...
Rchjk's user avatar
  • 31
5 votes
1 answer
134 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 ...
capor's user avatar
  • 61
2 votes
0 answers
72 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 ...
mudri's user avatar
  • 121

1
2 3 4 5
8