# 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. ...
• 31k
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 ...
• 511
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
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

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

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

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