Last call to make your voice heard! Our 2022 Developer Survey closes in less than a week. Take survey.

# Tag Info

Accepted

### What can Idris not do by giving up Turing completeness?

Idris is Turing Complete! It does check for totality (termination when programming with data, productivity when programming with codata) but doesn't require that everything is total. Interestingly, ...
• 696
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. ...
• 28.1k
Accepted

### Dependent types vs refinement types

The main differences are along two dimensions -- in the underlying theory, and in how they can be used. Lets just focus on the latter. As a user, the "logic" of specifications in LiquidHaskell and ...
• 536
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 ...
• 451
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 ...
• 11.8k
Accepted

### Which research languages have a stronger typesystem than Haskell and why?

The question is somewhat problematic, since it relies on a subjective definition of "better." Dependently-typed languages such as Agda, Idris, and Coq have a stronger type system than ...
• 29.1k

### 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. ...
• 546
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 ...
• 28.1k
Accepted

### What do we gain by having "dependent types"?

Expanding my comment: Dependent types can type more programs. "More" simply means that the set of programs typable with dependent types is a proper superset of the programs typable in the simply-typed ...
• 8,178
Accepted

### Does the Y combinator contradict the Curry-Howard correspondence?

The original Curry-Howard correspondence is an isomorphism between intuitionistic propositional logic and the simply-typed lambda calculus. There are, of course, other Curry-Howard-like isomorphisms; ...
• 18.8k
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 ...
• 28.1k

### 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 ...
• 28.1k
Accepted

• 546
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.1k

### 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 ...
• 11.8k
Accepted

### What is $Prop$ in the calculus of constructions?

In traditional Martin-Löf type theory there is no distinction between types and propositions. This goes under the slogan "propositions as types". But there are sometimes reasons for distinguishing ...
• 28.1k
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 ...
• 28.1k
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 ...
• 11.8k
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,178
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$. ...
• 28.1k

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

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

### Proving a sorting operation in type system

Yes, it is possible to express a precise type for a sorting routine, such that any function having that type must indeed sort the input list. While there might be a more advanced and elegant solution,...
• 14.1k
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 (...
• 619
Accepted

### Universal/existential quantification?

It helps to remember that $\forall$ (or $\Pi$ as you sometimes see) is a type. It's generalizing $\to$. So while it makes perfect sense to say $(\lambda x : A. M)\ N$, it doesn't make sense to say \$(\...
• 1,450