50
$\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.

|cite|improve this question
$\endgroup$
26
$\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 Allik 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
  • $\begingroup$ @Noldorin retweet? $\endgroup$ – Elliot Gorokhovsky Sep 3 '18 at 0:56
21
$\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$
  • 1
    $\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
14
$\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$
  • 3
    $\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
  • 1
    $\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

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.