[Solved]: Difference between Dependent type , refinement type and Hoare Logic

Problem Detail: 

I know little dependent type theory. From wikipedia :

A dependent type is a type whose definition depends on a value.

And from my Type theory course i recall that a dependent type is :

Family of types indexed by a type.

But i have a confusion regarding dependent types and refinement types and hoare logic.

Because from Depenedent vs refinement type the refinement types looks like a Hoare logic. What more power refinement types gives besides just allowing to state predicated that has to be satisfied (Which looks like nearly same as Hoare Logic)?

What additional thing that dependent type gives in comparison to refinement types ? And is Dependent type more powerful than Refinement types + Sat/Constraint solver.

can anyone clear the air with examples.

Asked By : Pushpa

Answered By : Derek Elkins

There is recent work by Paul-André Melliès and Noam Zeilberger that explores this. In particular the papers Functors are Type Refinement Systems and An Isbell Duality Theorem for Type Refinement Systems. There's also a video of a talk on the first one.

I think there is a lot of confusion around refinement types due to people thinking of particular systems as representative which causes goals and details of those particular systems to be attributed to the general idea. The short of it is type refinement systems classify terms that exist independently whereas (non-refinement) types, dependent or otherwise, are part of terms. This may sound familiar and possibly even a bit contradictory.

The potentially familiar and possibly contradictory seeming part comes about if you view types à la Curry (extrinsically) versus types à la Church (intrinsically). When we think of types à la Curry, we think of types as classifying untyped terms that already have meaning. In types à la Church, the only terms that exist are well-typed terms, i.e. the type constraints are part of our syntax. So what I'm saying is that a Curry-style type system is actually a type refinement system refining untyped terms, while a Church-style type system is not a type refinement system. This means that, for example, we can think of the simply typed lambda calculus as either a type refinement system or as a non-refinement type system.

Of course, no one says that our terms have to be untyped terms. We could just as well apply a type refinement system to typed terms, and, historically, this is the context in which refinement types (by that name) arose. However, applications to soft typing illustrate something closer to the situation described above.

So far I haven't said anything about dependent types. The reason is that it is a completely orthogonal concern. I would say the archetypal dependent type systems are usually presented in a Church-style, and thus are not type refinement systems, but NuPRL (based on Computational Type Theory, a variant of the most archetypal dependent type theory, Martin-Löf type theory) is blatantly a type refinement system as I've described. Terms in NuPRL may not even have types! Admittedly, the fact that "PRL" stands for "Program Refinement Logic" might be a tip-off too. On the flip side, Refinement Types for ML describes a refinement type system, possibly the origin of the term, which is not a dependent type system in any way.

As for Hoare triples, they are a type refinement system. They are actually used as an example of a type refinement system in the first paper. However, Hoare Type Theory gives something which can be viewed as a non-refinement type system for a language having Hoare triples.

To have an answer about the "power" of different systems, you need to specify a particular (family of) dependent type system(s) and a particular (family of) refinement type system(s). The term "dependent type system" covers a very broad class of type systems, and "type refinement systems" is even broader. Even then, the terms aren't mutually exclusive, so it would not be a comparison between "dependent type systems" and "refinement type systems". However, if by "dependent type system" you are thinking of something like Coq, and for "refinement type system" something like Liquid Types then it is pretty one-sided. Coq is generally viewed as powerful enough to handle virtually all of mathematics in practice; you could literally implement and prove correct a SMT solver within Coq and then use it; and a very close analog to the subset type can be formulated. (NuPRL literally has subset types.) On the other side, SMT solvers are usually restricted to decidable theories where Coq has no such limitation; and many systems like Liquid Types have a limited and non-extensible language for specifying predicates. (Of course, by "dependent type system" you could mean Dependent ML, and by "type refinement system" NuPRL [which is also a dependent type system] which would be one-sided in the other way.)

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/54957