58
votes
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
42
votes
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
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 ...
- 7,734
25
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 ...
- 28k
19
votes
Accepted
Can I have a "dependent coproduct type"?
The dependent sum is a common generalization of both the cartesian product $A \times B$ and the coproduct $A + B$. It just so happens that the HoTT book introduces dependent sum by generalizing $A \...
- 28k
18
votes
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 ...
- 11.8k
17
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....
- 29.1k
16
votes
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 ...
- 28k
16
votes
Accepted
Is path induction constructive?
It is an illusion that the computation rules "define" or "construct" the objects they speak about. You correctly observed that the equation for $\mathrm{ind}_{=_A}$ does not "...
- 28k
15
votes
Standard constructive definitions of integers, rationals, and reals?
Gilles answer is a good one, except for the paragraph on the real numbers, which is completely false, except for the fact that the real numbers are indeed a different kettle of fish. Because this sort ...
- 28k
13
votes
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
12
votes
Accepted
Standard constructive definitions of integers, rationals, and reals?
There are multiple ways to define a mathematical structure, depending on what properties you consider to be the definition. Between equivalent characterizations, which one you take to be the ...
12
votes
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 ...
- 7,734
12
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 ...
- 11.8k
11
votes
"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 ...
- 563
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 ...
- 29.1k
10
votes
Why are dependently typed languages such as Agda used for proofs, if supercompilers for simpler typed languages can do the same?
I think you're confusing two things: dependently typed languages are convenient for specifying properties and giving proofs about functional programs. The techniques you mention are possible decision ...
- 7,734
10
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 ...
- 2,005
8
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 ...
- 81
8
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 ...
- 28k
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:
...
- 28k
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 ...
- 11.8k
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 ...
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\...
- 7,734
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 ...
- 28k
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....
- 28k
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.
- 7,734
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-...
- 28k
7
votes
Is path induction constructive?
I'm no HoTT person, but I'll throw in my two-cents.
Suppose we are wanting to make a function $$f_A : \prod_{x,y : A}\prod_{p : x =_A y} C(x,y,p)$$
How would we do this? Well, suppose we're given any ...
- 884
7
votes
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'...
- 563
Only top scored, non community-wiki answers of a minimum length are eligible