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 ...
- 32.5k
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. ...
- 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.
...
- 32.5k
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 ...
- 101
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:
...
- 32.5k
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, ...
- 32.5k
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/...
- 13.9k
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
...
- 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 :...
- 32.5k
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{...
- 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 ...
- 11.4k
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 ...
- 32.5k
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 ...
- 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 ...
- 13.9k
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 ...
- 21.6k
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 ...
- 1,685
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 ...
- 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$ ...
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
$$
...
- 11.4k
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 ...
- 32.5k
6
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 ...
- 13.9k
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 ...
- 326
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 "...
- 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 ...
- 271
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 ...
- 1,310
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 ...
- 345
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 ...
- 13.9k
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). ...
- 1,175
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 ...
- 28.9k
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}}$, $*_{\...
- 13.9k
Only top scored, non community-wiki answers of a minimum length are eligible