9
$\begingroup$

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?

$\endgroup$
6
  • $\begingroup$ Refinement types can always be erased, which means that the proof theoretic strength doesn't increase, once you define "proof theoretic strength" properly. $\endgroup$
    – Trebor
    Feb 21, 2022 at 5:46
  • 2
    $\begingroup$ In CIC, Prop is designed to be erased yet it increases the proof theoretic strength tremendously when compared to MLTT. $\endgroup$ Feb 21, 2022 at 9:13
  • $\begingroup$ @Pierre-MariePédrot you're referring to impredicativity of Prop right? So I guess SProp doesn't increase strength? $\endgroup$ Mar 7, 2022 at 4:47
  • $\begingroup$ @Pierre-MariePédrot This doesn't control other variables. If we only change whether Prop is erased, CIC is not stronger. $\endgroup$
    – Trebor
    Jan 29 at 14:22
  • $\begingroup$ @Trebor I don't understand your comment, maybe what you call "erased" doesn't correspond to the notion I'm referring to. Terms of some type P : Prop in CIC are not computationally relevant and can be removed by realizability (aka extraction). Nonetheless, given that Prop is impredicative and most importantly that singleton elimination allows one to eliminate from Acc to Type, CIC proves e.g. that System F is SN while MLTT doesn't. The same proof doesn't go through if one uses SProp instead of Prop due to a weaker singleton elimination, but the details of the failure are funny. $\endgroup$ Feb 7 at 15:30

2 Answers 2

11
$\begingroup$

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.

$\endgroup$
8
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ Huh so something like Inductive sigR A (P: A -> bool) := | existR (a: A): (if P a then True else False) -> sigR A P might be a more faithful encoding of refinement types in a system like Coq as opposed to the existing sig? Might be useful for some stuff. $\endgroup$ Mar 7, 2022 at 4:54
  • $\begingroup$ @MolossusSpondee FTR, that's essentially the ssreflect approach. $\endgroup$ Mar 9, 2022 at 17:57
  • $\begingroup$ I'm sorry but your requirement of decidability for refinement predicates seems questionable to me. At least major languages with Refinement Types  — F* and Liquid Haskell  — employ an SMT solver to check the refinements, using semi-decidable fragment at best or outright undecidabe one (IIRC). Does it effectively makes Refinement Types a subset of Dependent Types modulo computational irrelevance? $\endgroup$ Apr 2, 2022 at 10:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.