# Tag Info

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

### Difference between Dependent type , refinement type and Hoare Logic

There is recent work by Paul-André Melliès and Noam Zeilberger that explores this. In particular the papers Functors are Type Refinement Systems and An Isbell Duality Theorem for Type Refinement ...

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

### "Minimal" intuitionistic type theory?

To elaborate on gallais' clarifications, a type theory with impredicative Prop, and dependent types, can be seen as some subsystem of the calculus of constructions, typically close to Church's type ...
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,...
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 ...
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 ...

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

### "Minimal" intuitionistic type theory?

The problem with Church encodings is that you cannot obtain induction principles for your types meaning that they are pretty much useless when it comes to proving statements about them. In terms of ...
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 ...
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 ...

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

Accepted

### Difference between "sort" and "universe"

Sort is (typically, though see Pure Type Systems) a meta-level concept and universes are an internalization of a particular case of a sort. The second chapter of Bart Jacobs' thesis covers a fairly ...
Accepted

### Generating constraints to solve dependently-typed metavariables?

There's a nice idiom, which is explained more in chapter 22 of Types and Programming Languages (it's used for polymorphism rather than dependent types, but the idea is the same). The idiom is as ...
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$ ...

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

### Proving a sorting operation in type system

Twan van Laarhoven has a nice fully worked out example in Agda of the "Correctness and runtime of mergesort, insertion sort and selection sort". The comments are also interesting: in them, Bob Atkey'...
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 ...
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, ...
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 \...