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. 
Dependent types vs refinement types
terminology;programming languages;type theory;functional programming;dependent types
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 fragmentsso 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-listsvs. in Idrishttps://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idrHowever, 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 whatcan be specified, while that of fully dependent systems is to automatewhat can be proved. Perhaps there is a happy meeting ground where we can get the best of both worlds!