Skip to main content
Share Your Experience: Take the 2024 Developer Survey
35 votes
Accepted

How do you get the Calculus of Constructions from the other points in the Lambda Cube?

First, to reiterate one of cody's points, the Calculus of Inductive Constructions (which Coq's kernel is based on) is very different from the Calculus of Constructions. It is best thought of as ...
Neel Krishnaswami's user avatar
22 votes

How do you get the Calculus of Constructions from the other points in the Lambda Cube?

I've often wanted to try and summarize each dimension of the $\lambda$-cube and what they represent, so I'll give this one a shot. But first, one should probably try to dis-entangle various issues. ...
cody's user avatar
  • 13.9k
11 votes
Accepted

"Spurious" Type Equivalences in MLSub/Algebraic Subtyping

in their ICFP 2000 paper Intersection types and computational effects, Rowan Davies and Frank Pfenning showed that the distributivity rule for function types is unsound in the presence of effects. ...
Neel Krishnaswami's user avatar
10 votes

"Spurious" Type Equivalences in MLSub/Algebraic Subtyping

A typechecker for an ML-like language has two tasks: Inference: given a program, come up with a type for it, or prove that none exists. Subsumption: given an inferred type and a user-written type ...
Stephen Dolan's user avatar
9 votes
Accepted

Intuition Behind Strict Positivity?

It sounds like you want an overview of normalization arguments for type systems with positive datatypes. I'd recommend Nax Mendler's PhD dissertation: http://www.nuprl.org/documents/Mendler/...
cody's user avatar
  • 13.9k
9 votes
Accepted

Recursive types and the empty type

First, note that nothing turns on the presence or absence of the empty type: if you have a nonlinear calculus with function types and unrestricted recursive types, then it is inconsistent. Indeed, ...
Neel Krishnaswami's user avatar
9 votes
Accepted

System F and System T names

I posted this to TYPES, but its probably worth copying here as well: In "The system F of variable types, fifteen years later", Girard remarks that there was no particular reason for the name F: ...
Neel Krishnaswami's user avatar
9 votes
Accepted

What are the issues with a set-like interpretation of quantifiers in type theory?

I think there may be a little nuance that can be applied to the situation, where 2 different possible hats may be applied, and which both are valid views of type systems. View 1: Types are intrinsic ...
cody's user avatar
  • 13.9k
8 votes
Accepted

Is there a formalization of normalization of impredicative system F?

Coq without Prop is not strong enough, because it's basically Martin-Löf type theory with universes. Coq with Prop is strong enough, because you can encode sets of normalizing terms via predicates $S :...
Neel Krishnaswami's user avatar
7 votes
Accepted

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

If you implement an evaluator for the terms of a language $A$ in a total system $B$, and you have furthermore proven that your evaluator is correct, that is for every $t$ well-typed in $A$, $$\mathrm{...
cody's user avatar
  • 13.9k
7 votes
Accepted

Determinism and pi-calculus

There are plenty such typing systems. Most work is based on the linear/affine typing system introduced in (1) and generalised in (2). Here are the main works on this subject. In (3) the typing system ...
Martin Berger's user avatar
7 votes
Accepted

Fixed points in dependent type theories

I think the idea of unifying type and term-level fixpoints is natural, though I have to admit I'm not sure that reducing the number of constructions of a system is not always a recipe for conceptual ...
cody's user avatar
  • 13.9k
7 votes
Accepted

Typing of substitution in a bidirectional type system

The key observation is that whether the substitution theorem holds, depends on the definition of substitution. For the usual definition of substitution of terms for variables, the substitution ...
Neel Krishnaswami's user avatar
7 votes

Typing of substitution in a bidirectional type system

One solution is indeed to restrict to substituting with synthesizing expressions. You can only hope to replace variables with terms of the same mode (i.e. inferrable terms), anything else just won't ...
gallais's user avatar
  • 635
7 votes
Accepted

Example of a function that you can write in Calculus of Constructions but not in System-F

Since the CoC has dependent types and system $F$ does not, I'll assume you mean a function whose types is in system $F$, but whose definition can only be written in CoC. Luckily in this case we can ...
cody's user avatar
  • 13.9k
6 votes
Accepted

Complexity of type-checking in relation to complexity of normalization

The relationship that you're looking for is indeed well-defined, but IMO it's not quite the right thing to look at. For example: Type checking for terms in the simply-typed lambda calculus is linear ...
Neel Krishnaswami's user avatar
6 votes

Intuition Behind Strict Positivity?

Another good source for going beyond strictly positive types is the PhD thesis of Ralph Matthes: http://d-nb.info/956895891 He discusses extensions of System F with (strictly) positive types in ...
Henning Basold's user avatar
6 votes
Accepted

Efficiently ordering typed programs

For ordered enumeration instead of random generation you are getting into the realm of combinatorics. I don't know of any generic results, but this paper Counting and Generating Lambda Terms describes ...
Max New's user avatar
  • 1,695
6 votes

Efficiently ordering typed programs

Two remarks first: I have used the "randomly generate terms and check that they are well-typed" approach (you mention that "untyped" terms are generated, you can also randomly generate terms in a ...
gasche's user avatar
  • 2,040
6 votes

Type checking, Hypothetical judgments, meaning explanations and computational type theory

Part of the problem is we cannot say that we have a checker for categorical judgments, because these often reduce to hypothetical judgments. For instance, the categorical judgment $M\in A\to B$ ...
Jonathan Sterling's user avatar
6 votes

How to prove relations between "classes" of types?

One approach to such questions is via encodings. Say you have a language $L_1$ and a language $L_2$ and you want to show that they are somehow "the same", you can do this by finding an encoding $$ ...
Martin Berger's user avatar
6 votes
Accepted

Is there any work relating type systems and Cook-Reckhow proof systems?

Cook-Reckhow propositional proof systems are nonunifrom. E.g. the computational complexity counterpart to the class of polynomial-size $\mathsf{Extended Frege}$ proofs is the nonuniform complexity ...
Kaveh's user avatar
  • 21.7k
6 votes
Accepted

Termination checking for Scott-encodings in System F with positive-recursive types

I'll first point you to Types for the Scott Numerals by Plotkin, Cardelli and Abadi, where they show how to encode Scott numerals in plain old system F. This at least shows that you can write the "...
cody's user avatar
  • 13.9k
6 votes
Accepted

PHOAS with extrinsic typing?

The standard well-formed-related predicate can be relatively easily extended to handle untyped PHOAS. The main subtlety is how to handle reduction at the type level. Here's a start of a two-place ...
Jason Gross's user avatar
6 votes
Accepted

Why would the term "dynamically typed" be considered a misnomer?

The discussion in the section surrounding that paragraph in Pierce's book explains why this is so. In particular, consider the definition of "type system" given on the page before: A type ...
Andreas Rossberg'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
Accepted

programming language with type-level functions

Yes, and this is much, much more common than you may have thought. You can do meaningful (and actually Turing-complete!) type-level computation in C++ (see this post by Matt Might for example). ...
xrq's user avatar
  • 1,175
5 votes
Accepted

Is there a 'very fast growing' hierarchy that would capture System F?

Typically, fast growing hierarchies are characterized by ordinal notations, which are really just ways to express fast-growing functions (but it's sometimes convenient to see them as ordinals in the ...
cody's user avatar
  • 13.9k
5 votes

Does the Hindley-Milner type system (i.e. STLC with prenex polymorphism) have a category-theoretic model?

Apart from what's already written in the slides you linked to, let me describe one possible approach. For studying type inference semantically we need a model in which a term can have many types, or ...
Andrej Bauer's user avatar
  • 29.2k
5 votes

Does the Hindley-Milner type system (i.e. STLC with prenex polymorphism) have a category-theoretic model?

This isn't an excessively deep answer, but you can express a type system based on STLC with prenex polymorphism as a Pure Type System in a quite simple way, using sorts $*_{\mathrm{mono}}$, $*_{\...
cody's user avatar
  • 13.9k

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