Skip to main content
10 votes

Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic

I do not know if this answers your question, but in Propositions as [Types] we communicate in Remark 6.6 an observation by Thierry Coquand, namely that the statement $$ (\forall x .\, \exists y .\, R(...
Andrej Bauer's user avatar
  • 29.2k
10 votes

Example of a term in system F which is not typable in the simply typed lambda calculus

Reacting to the previous answers, I think this is the simplest self-application which only contains types which have closed inhabitants. $$\lambda\,(f\,:\,\forall\,\alpha.\,\alpha\to\alpha).\,f\,(\...
András Kovács's user avatar
7 votes

Example of a term in system F which is not typable in the simply typed lambda calculus

Damiano Mazza's example uses an uninhabited type, $∀ X ⋅ X$. It is correct, but raises the obvious question whether one can do without. Here is an example that I find quite natural: $$Λ \ A B ⋅ λ \ (p ...
Jean Abou Samra's user avatar
7 votes
Accepted

Example of a term in system F which is not typable in the simply typed lambda calculus

Every normal term may be typed in system F (I can't seem to find a reference now, I'll come back with one when I have some more time). So, for example, letting $A:=\forall X.X$, then $$x^A(A\to\alpha)...
Damiano Mazza's user avatar
6 votes
Accepted

Power of existential types

Universal types can be used to encode the least fixed point, while dually, existential types can be used to encode the greatest fixed point. For example, consider $F(X) = 1 + A \times X$, then the ...
Trebor's user avatar
  • 345
5 votes

What is a model theory / category theory basis of System F-omega that corresponds to what programmers actually do?

Your description of an idealized computer is a nescient form of realizability, and there are very simple realizability models of parametric polymorphism. Take a model of computatation (an "...
Andrej Bauer's user avatar
  • 29.2k
5 votes
Accepted

Generalizations, or extensions of W-types in MLTT

The representation issue of W-types was resolved by Jasper Hugunin. So from type formers $0$, $1$, $2$, $W$, $\Pi$, $\Sigma$, identity and a universe hierarchy we do get all indexed inductive families ...
András Kovács's user avatar
4 votes
Accepted

Is Linear Evaluation Parametric?

Here's an Agda formalization of the non-linear version of your argument, and my comment above: ...
Dan Doel's user avatar
  • 1,021
3 votes
Accepted

How to encode a function from an existential type

Using function extensionality, it suffices to prove: $$∀ Z\ z. e\ (E\ P)\ \mathrm{pack}\ Z\ z = e\ Z\ z$$ The naturality rule for $e$ is: $$f\ (e\ A\ k) = e\ B\ (ΛR. λr. f\ (k\ R\ r))$$ If we pick $k =...
Dan Doel's user avatar
  • 1,021
3 votes
Accepted

Is is true that every monad transformer is equivalent to its underlying/base monad?

The equation F Id ≅ ∀ (m: Monad). F m seems to be correct (for most transformers F, see below). However, I would not say that &...
winitzki's user avatar
  • 542
3 votes

Generalizations, or extensions of W-types in MLTT

You could start with Spartan type theory (which honestly should be upgraded to use evaluation-by-normalization) and add simple inductive datatypes to them. This would involve several steps. First, add ...
Andrej Bauer's user avatar
  • 29.2k
2 votes
Accepted

Denotational semantics of intersection types

Intersection types appear in typed programming languages to capture the idea that a given expression may carry multiple functionalities. For example, given a type $\mathsf{read}\;\alpha$ of readable ...
Andrej Bauer's user avatar
  • 29.2k
2 votes

Denotational semantics of intersection types

Later edit: When I wrote the answer below, I was thinking of intersection types as they are understood in the context of the untyped $\lambda$-calculus. It is now clear that this is not the right ...
Damiano Mazza's user avatar
2 votes
Accepted

Can you regain the Church-Rosser property in languages with continuations?

A simple fix is to add call-by-value let-expressions$$\text{let } x := t\text{ in }u$$that evaluate $t$ to a value and then substitute it for $x$. Having these in the language allows to restrict $+$ ...
xavierm02's user avatar
  • 556
2 votes

Derivability of `Vector` in pure calculus of constructions

Source 1 does not say anything about deriving the induction principle for inductive types, it's only about non-dependent recursion. Source 2 says that deriving the induction principle is not possible. ...
András Kovács's user avatar
2 votes

Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?

Using syntactic methods, it's quite easy to see the correspondence between $\forall \alpha. ((\alpha \to \alpha) \to \alpha) \to \alpha$ and $1 + 2 + 3 + \dots$ You already had that intuition, and it ...
Li-yao Xia's user avatar
2 votes
Accepted

Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?

I claim that $T \cong \mathbb 1+\mathbb2+\mathbb3\,+\,…$. I will prove the type equivalence and then show what terms of type $T$ correspond to values of type $\mathbb 1+\mathbb2+\mathbb3\,+\,…$ The ...
winitzki's user avatar
  • 542
1 vote
Accepted

Formalising Church numerals in Agda

I think your neutral-bad lemma is too general. For instance: $$f : τ ⇒ σ, x : τ ⊢ f\ x : σ$$ $σ$ does not occur in the context, but there is a neutral term with its ...
Dan Doel's user avatar
  • 1,021
1 vote

What are some practical applications of inductive-inductive and inductive-recursive types?

As far as I know, the software industry remains blissfully unaware of dependent types in general, and of inductive-inductive types and inductive-recursive types in particular. Intersection types have ...
winitzki's user avatar
  • 542
1 vote

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

Actually, your question is too narrowly-focused. For intuitionist logic, and its underlying Heyting lattice, for any formula $X$, the subset of formulae $\overline{A} = A → X$ is a reverse-mapping of ...
NinjaDarth's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible