Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
Could somebody explain the difference between dependent types and refinement types? As I understand it, a refinement type contains all values of a type fulfilling a predicate. Is there a feature of dependent types which distinguishes them?
If it helps, I came across Refined types via the Liquid Haskell project, and dependent types via Coq and Agda. That said, I'm looking for an explanation of how the theories differ.
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 "proof terms" of the sort needed in the full dependent setting. This leads to significant automation. For example, compare insertion sort in LH:
http://ucsd-progsys.github.io/lh-workshop/04-case-study-insertsort.html#/ordered-lists
vs. in Idris
https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr
However, the automation comes at a price. One cannot use arbitrary functions as specifications as one can in the fully dependent world, which restricts the class of properties one can write.
Thus, one goal of refinement systems is to extend the class of what can be specified, while that of fully dependent systems is to automate what can be proved. Perhaps there is a happy meeting ground where we can get the best of both worlds!
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 dependent types (like sigma-types) are not allowed.
Liquid Type system, described in [1] is indeed decidable and Liquid Haskell does use SMT solvers. However, Liquid Haskell also requires proof terms (or values,as those are called in a non-dependently typed language): if you sit down to write a Liquid Haskell program, you write your own functions, not just the types.
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, you can also reasonably have dependent refinement types, like "type of all numbers greater than n".
0"?
$\endgroup$
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 type is the product type of two types where the second type depends on the value of the first: $$(x : T) \times q(x)$$ where $x$ is a variable name, $T$ is a type and $q(x)$ is a type dependent on x.
Thus, refinement types are similar to dependent pair types whose second type are restricted to being a decidable predicate.
Not every type is a predicate. For example $p_1(x) = x>0$ is a type and a predicate, but $q_1(x) = \text{list}(\text{list}(x))$ is only type and not a predicate e.g., something that is not possible to describe as a refinement type would be $(x : \text{Type}) \times \text{list}(\text{list}(x))$.
Not every predicate is decidable. In Liquid Haskell, only structural recursive functions on a single argument with a single equation per constructor are allowed to be used in decidable predicates, together with operators from the quantifier-free logic of linear arithmetic and uninterpreted functions (namely ==, <, +, ...) [1]. In Coq, all (total) functions can be used inside dependent types. Total in parenthesis, because in Coq all functions have to be total anyway.
Let us also look at the inhabitants of the types via their typing rules [2]. $$ \frac{e : T ~~~~~~ \text{true} : p(e)}{e : \{x:T ~|~ p(x)\}} \text{refinement} ~~~~~~~~~~~~~~~ \frac{e_1 : T ~~~~~~ e_2: q(e_1)}{(e_1, e_2) : (x : T) \times q(x)} \text{dependent} $$
All values $e$ which are inhabitants of the refined type are also inhabitants of the type $T$. Refinement types refine types, because they put an additional constraint on the values via the predicate. On the other hand, the inhabitants of dependent pair types are pairs of two values.
This is actually directly related to $p$ being restricted to being decidable, whereas $q$ is not restricted. A decidable $p$ means that we can pass $\text{true} : p(e)$ to a SMT-solver who will decide for us whether this formula holds or not. On the other hand, for an unrestricted $q(e)$ no such algorithm to decide it exists, meaning that you have to provide a proof $e_2$ that $q(x)$ holds, only then we can pass $e_2 : q(x)$ to a type-checker to decide whether it holds or not. In case the type $q$ is not an arbitrary type (like $\text{nat}$ with its many inhabitants $1$, $2$, $3$,...) but also a predicate (meaning that it has a most one inhabitant, e.g. $\text{true}$) the value $e_2$ becomes computationally irrelevant at run-time and can be erased during program extraction.
[1] Vazou et al, Haskell'14. LiquidHaskell: Experience with Refinement Types in the Real World
[2] Our rule $\text{refinement}$ is rule LT-Sub and DEC-<:-BASE from [3] merged into one rule. In abuse of notation, we omit type contexts for simplicity, and write $\text{true} : f$ instead of $valid([[f]])$ to say that formula $f$ is true, making it look more like the dependently typed language. For the rule $\text{dependent}$ see "term introduction" at Dependent Sum Type, although we write $(x:T) \times q(x)$ instead of $\Sigma x:T, q(x)$.
[3] Rondon et al, PLDI'08. Liquid Types
