2
$\begingroup$

Looking at the examples here and here both refinement type and liquid types look very similar. What are the differences and similarities?

$\endgroup$
1
  • $\begingroup$ They're essentially the same; from a quick browse it seems neither insists on there being a proof object ---if it's there, you get dependent types. $\endgroup$ – Musa Al-hassy Mar 3 '20 at 11:19
3
$\begingroup$

They are, to a first approximation, the same thing. "Liquid types" come from LiquidHaskell (1, 2), which is a programming language and verification framework based on refinement types. The Scala repository that you link to is an implementation of refinement types for Scala.

In terms of programming language theory, refinement types is the technically correct and more general term. LiquidHaskell and the Scala repository are examples of implementations of refinement types.

$\endgroup$
2
$\begingroup$

Your second link gives an answer, in 'The Liquid Story (Further Reading)':

  • a dependant type depends on an arbitrary expression
  • a refinement type depends on a logical predicate of a specification language
  • a liquid type depends on a logical predicate of a decidable specification language
$\endgroup$
2
  • $\begingroup$ What difference does decidable specification language and just specification language make? $\endgroup$ – Suminda Sirinath S. Dharmasena Mar 4 '20 at 4:39
  • $\begingroup$ The link details: "implication checking is decidable". That means that there is an algorithm that is able to conclude by yes or no, for any predicates P1 and P2 of the specification language, if P1 is a logical consequence of P2. This is of course possible only by restricting what can be expressed in the specification language. $\endgroup$ – L. Garde Mar 4 '20 at 21:05

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.