# Tag Info

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. ...
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 ...

### 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 ...
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 ...
Accepted

### Strict positivity

First a terminological explanation: negative and positive positions come from logic. They are about an assymetry in logical connectives: in $A \Rightarrow B$ the $A$ behaves differently from $B$. A ...
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 ...

### What is a brief but complete explanation of a pure/dependent type system?

Let's have a go. I'll not bother about Girard's paradox, because it distracts from the central ideas. I will need to introduce some presentational machinery about judgments and derivations and such. ...

### 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 ...
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, ...
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 ...