66
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ So when do we get verified Tetris? $\endgroup$ – Andrej Bauer Jun 4 at 15:29
  • $\begingroup$ @AndrejBauer Well, Idris is pac-man complete $\endgroup$ – jmite Jun 4 at 15:36
39
$\begingroup$

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!

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Is there a way to somehow mechanically map from refinement type based specifications to dependent type based specification? Or has such "isomorphism" not been studied enough yet? $\endgroup$ – Erik Kaplun Jan 7 '16 at 18:12
  • 1
    $\begingroup$ AFAIK such an "isomorphism" hasn't been studied a lot. There is some recent work though, see: "Formalizing Simple Refinement Types in Coq" by Lehmann and Tanter (which will appear soon ... here's a GH repo: github.com/pleiad/Refinements) $\endgroup$ – Ranjit Jhala Jan 8 '16 at 19:32
  • $\begingroup$ How about path-dependent types in Scala? $\endgroup$ – Yang Bo Jul 23 '17 at 19:21
  • 1
    $\begingroup$ @RanjitJhala I think you accidentally got your goals in the final paragraph the wrong way round? $\endgroup$ – Noldorin May 12 '18 at 22:49
  • 2
    $\begingroup$ @Noldorin I'd say Ranjit got his last paragraph right. "refinement type ... restricted to decidable fragments so that verification (and inference) is completely automatic" vs "proof terms ... needed in ... dependent [types]". Thus folk working in refinement types are trying to extend how much can be specified in a refinement type while still being automatically inferencable/verifiable, while those working in dependent types are trying to automate generation of proof terms. $\endgroup$ – raiph Jun 20 '19 at 8:48
23
$\begingroup$

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.

[1] http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf

| cite | improve this answer | |
$\endgroup$
  • 2
    $\begingroup$ sigma can be encoded with pi using a church-like encoding, but AFAIK liquid haskell's refinement function types isn't pi (dependent function) types. $\endgroup$ – fread2281 Jan 5 '15 at 22:25
15
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$
  • 4
    $\begingroup$ Is one a subset of the other? Refinement types seem to be solveable using SMT, but dependent types require your own proof terms... $\endgroup$ – jmite Feb 17 '14 at 20:18
  • 4
    $\begingroup$ "Is one a subset of the other?" No. That's why I gave the examples of a refinement type which isn't dependent and a dependent type which isn't a refinement. $\endgroup$ – Alexey Romanov Feb 18 '14 at 10:02
  • 8
    $\begingroup$ can't refinement types be encoded with sigma? $\endgroup$ – fread2281 Jan 6 '15 at 15:48
  • 3
    $\begingroup$ Your example does not seem to demonstrate your point. The positive numbers are defined as those numbers greater than 0. Does this not mean that "the type of positive numbers" is precisely "the type of all numbers greater than 0"? $\endgroup$ – akdom Apr 8 '16 at 13:23
  • 3
    $\begingroup$ Is it not possible for there to be a refinement predicate that enforces the length of the vector as well? $\endgroup$ – CMCDragonkai Jun 16 '16 at 8:26
3
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.