Skip to main content
29 votes
Accepted

if (λ x . x x) has a type, then is the type system inconsistent?

Certainly, assigning a type to $\lambda x. x\ x$ is not enough for inconsistency: in system $F$, we can derive $$ \lambda x.x\ x:(\forall X.X)\rightarrow (\forall X.X)$$ in a pretty straightforward ...
cody's user avatar
  • 8,233
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 ...
Andrej Bauer's user avatar
  • 30.9k
19 votes

What is different between Set and Type in Coq?

Coq has 4 "big" types: Prop is meant for propositions. It is impredicative, meaning that you can instantiate polymorphic functions with polymorphic types....
Joey Eremondi's user avatar
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 ...
Derek Elkins left SE's user avatar
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 ...
Dan Doel's user avatar
  • 2,707
12 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 ...
drcicero's user avatar
  • 121
11 votes
Accepted

Where are C++ templates inside of the lambda cube?

But is that exactly where they are located in the lambda cube? The lambda cube is not a giant spectrum on which all programming languages can be classified. It is precisely eight languages, which ...
Joey Eremondi's user avatar
9 votes
Accepted

Examples of Dependent Types

I think it helps to keep in mind the propositions as types mantra. Every type can be read either as a propostion or a set. This gives us two readings (let's just consider types dependent on natural ...
Andrej Bauer's user avatar
  • 30.9k
8 votes

Reducing products in HoTT to church/scott encodings

To get your idea working you need something extra, as was pointed out in @cody's answer. Sam Speight worked under the supervision of Steve Awodey to see what can be achieved in HoTT using an ...
Andrej Bauer's user avatar
  • 30.9k
8 votes
Accepted

Reducing products in HoTT to church/scott encodings

The standard reference I often give is Induction is not derivable in second order dependent type theory by Herman Geuvers, which says that there is no type $$N : \mathrm{Type}$$ with functions $$Z:N\...
cody's user avatar
  • 8,233
8 votes
Accepted

Relation between Hoare Type Theory and pointers

A pointer to a variable creates an alias. When the alias is modified, the corresponding variable is modified as well. Therefore, the rule for an assignment in Hoare's logic is not just update the ...
Alexander Kogtenkov's user avatar
8 votes

Can properties such as memory usage of a function be expressed in a dependently typed language?

Yes, it can. While conceptually it's not that difficult, it hasn't been studied all that much. One aspect of the field is cost semantics such as the research done by Guy Blelloch. In the vein of ...
Derek Elkins left SE's user avatar
8 votes
Accepted

How to derive dependently typed eliminators?

The canonical reference for this is Peter Dybjer, Inductive Families, which gives a pretty comprehensive treatment of inductive families based on eliminators.
cody's user avatar
  • 8,233
8 votes
Accepted

What are the rules for positive recursive types in dependent type theory?

Why are recursive types seldomly seen in dependent type theory? The point of inductive types is precisely that you get normalization. Unrestricted recursive types simply lead to non-normalizing terms....
Andrej Bauer's user avatar
  • 30.9k
8 votes
Accepted

About the Identity function in Agda

Your code does not work. I would suggest that you forget about the universe levels for the time being (the $\ell$ thing) and focus on simpler things first. Here is working code: ...
Andrej Bauer's user avatar
  • 30.9k
8 votes
Accepted

Show how lack of universe levels would create contradiction in homotopy type theory (in Agda)

The problem is not specific to homotopy type theory. In type theory in general, if there is a type of all types, then every type is inhabited. This was shown first by Girard who encoded the Burali-...
Andrej Bauer's user avatar
  • 30.9k
7 votes

Why are recursive types needed as primitives for proofs in dependent type systems?

I'm not an expert, but I'll share what I understood so far with an example. Let's consider the boolean type in CoC, using its standard encoding: $$ \begin{array}{l} \mathbb{B} = \Pi_{\tau:*} \tau \to ...
chi's user avatar
  • 14.6k
7 votes

What are the strongest known type systems for which inference is decidable?

[EDIT: Voilà a few words on each] There are several ways of extending HM type inference. My answer is based on many, more or less successful, attempts at implementing some of them. The first one I ...
dader's user avatar
  • 214
7 votes
Accepted

Indexing a dependent type on a value?

The best answer I can give is that you are confused about the meaning of words. I tried to explain this already in another answer to you, so let me be more explicit this time. To say type $A$ ...
Andrej Bauer's user avatar
  • 30.9k
7 votes
Accepted

Dependent Type Theory Implementation of a Graph

So, there are two different things you are talking about. The definition of a graph The encoding of a graph A Graph is always defined as a set of vertices and edges. This tells us what vertices are ...
Joey Eremondi's user avatar
7 votes
Accepted

Dependent type system with different computation model

Yes, realizability theory allows you to model dependent type theory based on a variety of computational models, such as: Turing machines (with or without oracles), various $\lambda$-calculi, ...
Andrej Bauer's user avatar
  • 30.9k
7 votes

When is cumulative type universes useful?

Without cummulative universes, if you have $A : \mathsf{Type}_3$ then you do not have $A : \mathsf{Type}_7$. Instead, we also have to introduce lifting functions $\iota_{i,j} : \mathsf{Type}_i \to \...
Andrej Bauer's user avatar
  • 30.9k
7 votes

What is the runtime/time complexity of Coq’s (Dependent) Type Inference?

There are actually two questions here. Is the Coq type system decidable? Long answer short, we hope so, as in it would be a bug if it were not. It is not a universal requirement for a type theory to ...
Pierre-Marie Pédrot's user avatar
6 votes
Accepted

Family of types in type theory

Consider the example of the dependent type of number sequences of length $n$. It might be defined like this in Coq: ...
Andrej Bauer's user avatar
  • 30.9k
6 votes
Accepted

Domain Theory and Polymorphism

There are many ways to model polymorphism via domain theory, let me just describe one that is easy to understand, so you can think about it yourself. It's a "PER model". Take any model of the untyped ...
Andrej Bauer's user avatar
  • 30.9k
6 votes
Accepted

Is there any difference between extensible records and dependent maps

Simple records correspond to maps of dependent type (and we don't have a merge operation yet). More precisely, the record type ...
Andrej Bauer's user avatar
  • 30.9k
6 votes

How to derive dependently typed eliminators?

You might find some of our recent papers on this useful, as we derive eliminators for lambda-encoded datatypes. For example, see this one for generic derivation of eliminators, and this one for the ...
Aaron Stump's user avatar
6 votes

Why values can not be replaced with their extensionally equal values in an intensional system?

Supposing we have $a$ and $b$ of type $A$ and $p : \mathrm{Id}_A(a,b)$, there simply is not any rule of type theory that would allow you to replace $b$ with $a$ arbitrarily. So one answer is "because ...
Andrej Bauer's user avatar
  • 30.9k
5 votes
Accepted

Is it possible to prevent arithmetic errors with a dependent type system?

In theory, you can do anything of this sort with dependent types! Typically you would define your own (dependent) type, say ...
cody's user avatar
  • 8,233
5 votes

What's the difference between the rank and the degree of a type function?

The book states that the rank of a term is the number of $\Pi$'s in its (normal) form. But doesn't the number of such $\Pi$'s correspond exactly to the number of arguments it takes? That is, if a type ...
chi's user avatar
  • 14.6k

Only top scored, non community-wiki answers of a minimum length are eligible