principleMajor
Dependent types vs refinement types
Viewed 0 times
refinementdependenttypes
Problem
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.
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.
Solution
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!
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!
Context
StackExchange Computer Science Q#21728, answer score: 44
Revisions (0)
No revisions yet.