56
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 ...
40
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 ...
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 ...
24
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:
...
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 ...
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
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'
41k7 gold badges108 silver badges173 bronze badges
16
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, ...
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}$. ...
16
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 "...
16
Coq has 4 "big" types:
Prop is meant for propositions. It is impredicative, meaning that you can instantiate polymorphic functions with polymorphic types. It is also erased at run-time, meaning you can't pattern match on a Prop value to build a Type value, unless there's only one possibility.
SProp is like Prop, but with definitional proof ...
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 ...
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'
41k7 gold badges108 silver badges173 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 ...
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 ...
9
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 programmer wanting to use the type theory to compute something. For instance, we might want to compute some natural number satisfying some specification we've come ...
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
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 numbers):
A dependent type $P : \mathtt{nat} \to \mathtt{Type}$ is like a family of sets $P(0), P(1), P(2), \ldots$
A dependent type $P : \mathtt{nat} \to \...
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
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\qquad S:N\rightarrow N $$
such that
$$\mathrm{ind}:\Pi P:N\rightarrow \mathrm{Type}.P\ Z\rightarrow (\Pi m:N.P\ m\rightarrow P\ (S\ m))\rightarrow \Pi n:N. P\...
8
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 impredicative universe, see Impredicative Encodings of Inductive Types in HoTT blog post.
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.
Only top voted, non community-wiki answers of a minimum length are eligible