What's the relationship between refinement types and dependent types?

Question

In the F* proof assistant, they use refinement types together with dependent types. Based on my impression of F*, it seems to me that refinement types are just predicates in dependent type theory that are like "something something of type boolean should equal to true". I think I'm probably (extremely) biased (and probably wrong), as I have only ever seen refinement types in one language.

I am slightly more experienced with dependent types, and I'm wondering how are dependent types and refinement types related. Is there something that is only possible with refinement types, but not possible (or extremely hard to imitate) in dependent types?

Answer 1

Is there something that is only possible with refinement types, but not possible (or extremely hard to imitate) in dependent types?

Yes. Refinement types make the notion of logical or ghost term available. These are terms which can occur in types, but cannot directly be used for any computationally relevant purpose.

Consider the following type for a function which takes a vector and returns how long it is.

length : Πn: Nat → Vector n A → Σm:Nat. m ≡ n

This says that if you give the function a vector, it will return a number equal to the length of that vector. You can implement it like this in Agda:

length _ [] = (0, refl)
length _ (x :: xs) = let (k, pf) = length xs in 
                     (suc k, cong suc pf)

which is a function which traverses the list and counts how many cons cells there are.

Unfortunately, you can also write it like this:

length n _ = (n, refl)

and just immediately return the index. In other words, you can't call the length function unless you tell it how long the list is! So there's no point to this function even existing.

With a refinement type discipline, you can write a function type like the following.

length : ∀n: Nat → Vector n A → Σm:Nat. m ≡ n

By switching from pi to forall, I mean to indicate that the length argument is computationally irrelevant. (Note that this is not proof-irrelevance! E.g., note the occurrence of n in m ≡ n in the return value.) As a result, the first definition of length typechecks, but the terrible second definition won't.

This is super useful! (For example, termination metrics like Bove-Capretta accessibility predicates really want to be computationally irrelevant.)

The general theory of these things can be found in Noam Zeilberger and Paul-André Melliès POPL 2015 paper, Functors are Type Refinement Systems. Noam also has a set of OPLSS notes, which introduces these ideas more gently.

Answer 2

I am not sure that there is a unique definition of refinement types, but there is a common theme. In general, a system featuring refinement types is some kind of ML extended with a subset type construct $\{x : A \mid P\}$.

There are two key points that make this different from the dependently-typed Σ type, though.

• First, P must live in some decidable fragment of the ambient logic
• Second, the proof part is definitionally proof-irrelevant.

Without the decidability requirement, one would be able to encode dependent types into refinement types using some kind of realizability model. As a matter of fact, refinement types were inspired by the PRL approach, which is precisely a realizability interpretation of dependent types.