Yes. My response was of course to clarify that "ordinary" type systems are Turing equivalent and incorporate classical logic. Dependent types correspond to fir

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]. 0. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2636 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2... 1. http://homepages.cwi.nl/~ralf/HList/paper.pdf http://homepages.cwi.nl/~ralf/HList/paper.pdf