Standard type systems are Turing equivalent. This includes the type systems of functional languages like ML and Haskell. In fact, there's a neat correspondence [0] between algebraic data types and propositional logic (examples in Haskell):
union types (data T = mkTA A | mkTB B) <-> logical disjunction (A ∨ B)
product types (data T = mkT A B) <-> logical conjunction (A ∧ B)
function types (type T = A -> B) <-> logical implication (A → B)
the unit type (()) <-> true (⊤)
bottom (⊥) <-> false (⊥)
(And, if you were wondering, that's where the symbol for "bottom" comes from!)
Inference on richer type systems, e.g., systems that support dependent types (types built up from expressions about the values they represent) is in general undecidable, which is why some dependently typed languages (e.g., Coq) have type systems that are not Turing equivalent—the language designers have consciously pared down parts of the type system in order to guarantee that type-checking terminates.
Yes. My response was of course to clarify that "ordinary" type systems are Turing equivalent and incorporate classical logic.
Dependent types correspond to first-order logic in the Curry-Howard interpretation. I don't know much of anything about Shen, so I can't comment further on it specifically.
By the way, limited dependent types can also be implemented in Haskell through type-level programming. The paper that introduced this idea [0] is a good read, and doing some type-level programming is a great way to get to grips with the ins and outs of Haskell's type system. If you're interested in type-level hackery, also be sure to read the HList paper [1].
The argument is that agda is relatively straightforward for haskellers and similarly, coq for ocaml devs to adopt. This is a good succinct example of former. Coq has lots of tutorials
Inference on richer type systems, e.g., systems that support dependent types (types built up from expressions about the values they represent) is in general undecidable, which is why some dependently typed languages (e.g., Coq) have type systems that are not Turing equivalent—the language designers have consciously pared down parts of the type system in order to guarantee that type-checking terminates.
0. This is the Curry-Howard correspondence: http://en.wikipedia.org/wiki/Curry–Howard_correspondence#Cor...