51
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, having data and codata is enough to model Turing Completeness since you can write a monad for partial functions. I did this, years ago, in Coq - it's probably ...
39
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 refinement type systems generally, is restricted to decidable fragments
so that verification (and inference) is completely automatic, meaning one does not require ...
37
For a rather simple version of dependent type theory, Gilles Dowek gave a proof of undecidability of typability in a non-empty context:
Gilles Dowek, The undecidability of typability in the $\lambda\Pi$-calculus
Which can be found here.
First let me clarify what is proven in that paper: he shows that in a dependent calculus without annotations on the ...
29
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 way (this is a good exercise!). However, $(\lambda x.x\ x)(\lambda x.x\ x)$ cannot be well typed in this system, assuming $\omega$-consistency of 2nd order ...
23
Refinement types are simply usual types with predicates.
That is, given that $T$ is a usual type and $P$ is some predicate on $T$
$$\{v:T \mid P(v)\}$$
is a refinement type. $T$ in this case is called a base type.
AFAIK, in Liquid Haskell, they also allow some dependend function types, that is types $\{x:T_1 \to T_2 \mid P\}$ [1]. Notice that fully ...
23
It is a common misconception that we can translate let-expresions to applications. The difference between let x : t := b in v and (fun x : t => v) b is that in the let-expression, during type-checking of v we know that x is equal to b, but in the application we do not (the subexpression fun x : t => v has to make sense on its own).
Here is an example:
...
19
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 \times B$, because that does not require the boolean type to be defined first.
The coproduct is a special case of dependent sum. Given types $A$ and $B$, consider ...
18
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 Systems. There's also a video of a talk on the first one.
I think there is a lot of confusion around refinement types due to people thinking of particular systems ...
16
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 them. CoC does precisely that.
There are many variants of CoC, but most would have
$$\mathsf{Prop} : \mathsf{Type}$$
but not $\mathsf{Type} : \mathsf{Prop}$. ...
15
Dependent types are types which depend on values in any way. A classic example is "the type of vectors of length n", where n is a value. Refinement types, as you say in the question, consist of all values of a given type which satisfy a given predicate. E.g. the type of positive numbers. These concepts aren't particularly related (that I know of). Of course, ...
15
The question under what circumstances we need to jump from a universe to one higher in the hierarchy is a good one. Having the hierarchy and the ability to climb it is important. You need to jump levels when you want to treat a universe as a type or as part of a type. For example to define functions of (non-dependent) type
$$
A \rightarrow \mathcal{U}_i
$$...
15
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 of misinformation seems to be quite widespread, I would like to record here a detailed rebuttal.
It is not true that all inductive types are denumerable. For ...
14
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 "define" it, but failed to observe that the same is true in other cases as well. Let us consider the induction principle for the unit type $1$, which seems particularly obviously "...
14
First, I assume you've already heard of the Church-Turing thesis, which states that anything we call “computation” is something that can be done with a Turing machine (or any of the many other equivalent models). So a Turing-complete language is one in which any computation can be expressed. Conversely, a Turing-incomplete language is one in which there is ...
answered Jan 8 '14 at 19:42
Gilles 'SO- stop being evil'
39.1k7 gold badges103 silver badges167 bronze badges
13
I will slightly amend Martin's answer to explain where cumulativity comes in (the rule which says that $X : \mathcal{U}_i$ and $i \leq j$ entail $X : \mathcal{U}_j$). Suppose we have $A : \mathcal{U}_{42}$ and we would like to give a type to $A \to \mathcal{U}_{99}$. The formation rule for $\to$ is this:
$$\frac{\Gamma \vdash X : \mathcal{U}_i \qquad \Gamma \...
13
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, I'll sketch an elementary one, only.
We will use a Coq-like notation. We start by defining a predicate requiring that f: nat -> nat acts as a permutation ...
12
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 definition and which one you take to be an alternative characterization is not important.
In constructive mathematics, it is preferable to pick a definition that makes ...
answered Mar 16 '15 at 17:14
Gilles 'SO- stop being evil'
39.1k7 gold badges103 silver badges167 bronze badges
12
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 theory. The relationship between Church's type theory and the CoC is not that simple, but has been explored, notably by Geuvers excellent article.
For most ...
12
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 gave. A dependent type system doesn't need to have a "type" of types (a universe) in general (MLTT does have universes though), nor do you need dependent types ...
12
Coq has 3 "big" types:
Prop is meant for propositions. It is impredicative, meaning that you can instantiate polymorphic functions with polymorphic types. It also has proof irrelevance, meaning that if $p_1, p_2 : P$ then $p_1 = p_2$. This allows terms that are only used for proof to be erased in any code generated by Coq.
Set is meant for computation. It's ...
11
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 minimality of the system, one path mentioned in the comments is to use containers and (W / M)-types however they are rather extensional so that's not really ...
11
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 combine a lambda calculus (values abstracted over values) with all possible combinations of three features:
Values abstracted over types (parametric polymorphism)
...
10
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 procedures for certain properties of functional programs.
The ability to specify program properties usually takes place within a logic. Dependent types are a ...
8
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 follows:
A type checking system can be turned into a type inference system by making the rules linear and adding constraints.
I'll use the application rule as an ...
8
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:
idd : (A : Set) → A → A
idd A a = a
The type of idd is (A : Set) → A → A. It is a dependent product, i.e., it could be written as $\prod_{A : \mathsf{Set}} A \to A$ in mathematical ...
8
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 the video Anton mentioned is Daniellson's work in Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. This does indeed use a ...
8
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 value, but update the value for all associated aliases. Let's apply it to the example:
{True} int i=0; {i = 0}
{i = 0} int*p=&i; {i = 0; [*p, i]} ...
8
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.
Given any type $A$, we may inhabit $A$ with a non-normalizing term as follows. Consider the recursive type
$$D = D \to A.$$
The term $\omega \mathrel{{:}{=}} ...
8
The canonical reference for this is Peter Dybjer, Inductive Families, which gives a pretty comprehensive treatment of inductive families based on eliminators.
8
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-Forti paradox in type theory.
A simplification of the paradox was found by Hurkens. Here is Agda code for it, and here is Coq code.
Only top voted, non community-wiki answers of a minimum length are eligible
