What’s the difference between refinement types and dependent types? The types as written in this post seem to meet the definition of dependent types (a type that depends on something that is not a type) because various integer values are present in the type statement. Is the difference that refinement types can only be a subset of a larger type?
IANATT (type theorist), but I believe refinement types are understood to be written in a limited language that can be fed into a SAT solver, whereas dependent types require that types can be used as values and vice versa ‘anywhere’ in the language.
With dependent types you could write down a function that takes a boolean and varies the type of its second parameter according to the value of the boolean, at runtime. I don’t think that liquid-rust and liquid-haskell support this.
[Edit: You could simulate this in liquid-haskell with something like b:Bool -> {e:Either String Int | if b then (isLeft e) else (isRight e) -> ... but this is somewhat different from what you get in Agda and Coq. Refinement types here refine the Either String Int to being just one of its variants according to the value of the boolean, but in a dependently typed language you’d just have the two different types.]
I believe it’s built on liquid-fixpoint, which is the same backend that liquid-haskell uses, and so my guess is that it’s similarly a compile time analysis only.
What’s the difference between refinement types and dependent types? The types as written in this post seem to meet the definition of dependent types (a type that depends on something that is not a type) because various integer values are present in the type statement. Is the difference that refinement types can only be a subset of a larger type?
IANATT (type theorist), but I believe refinement types are understood to be written in a limited language that can be fed into a SAT solver, whereas dependent types require that types can be used as values and vice versa ‘anywhere’ in the language.
SMT solvers as well
With dependent types you could write down a function that takes a boolean and varies the type of its second parameter according to the value of the boolean, at runtime. I don’t think that liquid-rust and liquid-haskell support this.
[Edit: You could simulate this in liquid-haskell with something like
b:Bool -> {e:Either String Int | if b then (isLeft e) else (isRight e) -> ...but this is somewhat different from what you get in Agda and Coq. Refinement types here refine theEither String Intto being just one of its variants according to the value of the boolean, but in a dependently typed language you’d just have the two different types.]Is there a runtime component to this or is entirely static?
I believe it’s built on liquid-fixpoint, which is the same backend that liquid-haskell uses, and so my guess is that it’s similarly a compile time analysis only.