62
votes
Accepted
What exactly is the semantic difference between set and type?
To understand the difference between sets and types, ones has to go back to pre-mathematical ideas of "collection" and "construction", and see how sets and types mathematize these.
...
- 31k
40
votes
Accepted
Why is C's void type not analogous to the empty/bottom type?
In C, void is used for multiple unrelated things. Depending on what it's used for, its meaning may be a unit type, an empty type, or something else.
When ...
40
votes
What's the difference between a type and a kind?
Here, "values", "types", and "kinds" have formal meanings, so considering their common English usage or analogies to classifying automobiles will only get you so far.
My answer pertains to the formal ...
- 511
32
votes
Accepted
Why must a function with polymorphic type `forall t: Type, t->t` be the identity function?
The first thing to note is that this isn't necessarily true. For example, depending on the language a function with that type, besides being the identity function, could: 1) loop forever, 2) mutate ...
- 12.1k
27
votes
Accepted
Why does Coq include let-expressions in its core language
It is a common misconception that we can translate let-expresions to applications. The difference between let x : t := b in v ...
- 31k
23
votes
What's the difference between a type and a kind?
If you know about the difference between sets and classes in set theory, then it may help to think about the matter as
$$\mathrm{type} : \mathrm{kind} = \mathrm{set} : \mathrm{class}.$$
If not, you ...
- 31k
19
votes
Accepted
Is there a difference between type safety and type soundness?
Type safety and type soundness are synonyms in most theoretical work. Type soundness is often formulated with respect to an operational semantics as (type) preservation and progress. Preservation ...
- 12.1k
19
votes
Accepted
What does the leading turnstile operator mean?
On the left of the turnstile, you can find the local context, a finite list of assumptions on the types of the variables at hand.
$$
x_1:T_1, \ldots, x_n:T_n \vdash e:T
$$
Above, $n$ can be zero, ...
- 14.6k
18
votes
Accepted
What is induction-induction?
Supplemental 2016-10-03: I mixed up induction-induction and induction-recursion (not the first time I did that!). My apologies for the mess. I updated the answer to cover both.
I find the ...
- 31k
18
votes
Accepted
Is there a non-trivial type which is equal to its own derivative?
Consider the finite multisets $\mathbf{Bag}\:X$. Its elements are given by $\{x_1,\ldots,x_n\}$ quotiented by permutations, so that $\{x_1,\ldots,x_n\}=\{x_{\pi 1},\ldots,x_{\pi n}\}$ for any $\pi\in\...
- 546
18
votes
Accepted
Why product type is a dependent SUM?
Let's do products first.
The usual cartesian product $A \times B$ is also called a binary product because we are making a product of two sets. We could make a ternary product $A \times B \times C$. ...
- 31k
17
votes
Accepted
What is the use case for multi-type-parameter generics?
Some use cases for multiple type arguments include
maps/dictionaries Map<K,V>, where you have one key parameter and one value parameter
product types ...
- 14.6k
17
votes
Is there any use case for the bottom type as a function parameter type?
One of the defining properties of the $\bot$ or empty type is that there exists a function $\bot \to A$ for every type $A$. In fact, there exists a unique such function. It is therefore, fairly ...
- 12.1k
16
votes
What exactly is the semantic difference between set and type?
In practice, claiming that $x$ being of type $T$ usually is used to describe syntax, while claiming that $x$ is in set $S$ is usually used to indicate a semantic property. I will give some examples to ...
- 8,322
15
votes
Accepted
Reference request: Category theory as it applies to type systems
Category theory is not necessary to understand programming languages, it's not even necessary to do advanced research on programming languages. Most programming language people don't know (much) ...
- 8,358
15
votes
Why must a function with polymorphic type `forall t: Type, t->t` be the identity function?
The proof of the claim is quite complex, but if that's what you really want, you can check out Reynolds' original paper on the topic.
The key idea is that it holds for parametrically polymorphic ...
- 30k
15
votes
What do the ∀ and ∃ symbols mean in the Axiom of Choice?
$\forall$ reads as "for all", and $\exists$ reads as "there exists".
So, in english we have
$$\text{"if }\underbrace{\text{for all $x$}}_{\forall x^\sigma}\text{ }\underbrace{\text{exists a $y$}}_{\...
- 290
14
votes
Accepted
Question on the "Tutorial implementation of dependently typed lambda calculus"
$\mathsf{id}$ and $\mathsf{const}$ are not variables of the calculus, but syntactic sugar for $\lambda x \rightarrow x$ and $\lambda x \rightarrow \lambda y \rightarrow x$ respectively. This is stated ...
13
votes
Dependent types vs refinement types
A refinement type is a type together with a decidable predicate:
$$ \{x:T ~|~ p(x)\} $$
where $x$ is a variable name, $T$ is a type, and $p(x)$ is a decidable predicate over $x$.
A dependent pair ...
- 131
13
votes
Accepted
Relation between type-checking decidability, typability decidability and strong normalization
I'll give a more focused and technical answer to Martin's. If we're interested in dependent type theories, then neither direction is obvious, but both are generally assumed to hold. However the ...
- 8,262
13
votes
Accepted
What fragment of Martin-Löf dependent type theory can be expressed using generic types in Java?
There are a lot of misconceptions here. To begin, MLTT doesn't have subtypes, so Java is not going to simply be a fragment of it. It does not require dependent types to make either of the types you ...
- 12.1k
13
votes
Accepted
What does canonicity property mean in Type Theory?
There are potentially multiple ways of presenting canonicity (and I think complications depending on the theory). However, I think the simplest way to think about it is from the perspective of a ...
- 2,792
13
votes
Accepted
What do the ∀ and ∃ symbols mean in the Axiom of Choice?
The symbols are quantifiers. They bind a new variable name to the symbolic logic statements. ∃ reads as there exists. ∀ reads for all so the first part of the statement would be read as:
forall x (...
- 659
13
votes
Rigorous proof that parametric polymorphism implies naturality using parametricity?
The missing part is the "identity extension lemma", which is mentioned in Reynolds' original paper but not in Wadler's.
For $F : \text{Type} \to \text{Type}$, this says that if the ...
- 948
12
votes
What is the Curry-Howard analogue for linear logics?
Linear logic corresponds to a type system for a process calculus (a variant of the internal π-calculus), where:
proofs correspond to processes;
propositions correspond to session types (communication ...
- 171
12
votes
Accepted
What is a fixpoint?
Putting it very simply, a fixed point is a point that, when provided to a function, yields as a result that same point. The term comes from mathematics, where a fixed point (or fixpoint, or "invariant ...
- 273
12
votes
Accepted
Is Coq synthetic or analytic?
The remark is about one specific usage of Coq, namely formalization of programming language theory.
Let us first make clear the distinction between synthetic and analytic:
In a synthetic approach to ...
- 31k
11
votes
Why is C's void type not analogous to the empty/bottom type?
The name “empty type” is perhaps confusing. What this means is, as you say yourself, the type contains no values. The “empty” refers not to any individual values of the type, it refers to the type as ...
- 1,681
11
votes
Accepted
Are there any type constructors which are *not* functors?
One obvious counterexample is a binary search tree. You cannot freely substitute the values in a binary search tree because a substitution might change the ordering (relative to ...
- 23.1k
11
votes
Accepted
What is a super universe?
One intention behind having a universe operator and a super-universe closed under it, is to give a type-theoretic version of large cardinal axioms known from set theory. An inaccessible cardinal is ...
- 31k
Only top scored, non community-wiki answers of a minimum length are eligible