[bitc-dev] Accurate static typing vs. Dependent Types

[Rohan Lean]

On Sun, 2008-12-07 at 22:37 -0500, Jonathan S. Shapiro wrote:

> All "statically typed" programming languages prior to dependent types
> actually stand somewhere in between static and dynamic typing. The
> litmus test question is: "Are there operations exist in the core
> language that can throw runtime exceptions that are not statically
> prevented by the type system?"

I think it is possible to design a useful language that passes the test
without being dependently typed. As an example consider Haskell 98, with
(/), head, tail, ... having remedied types, such as:

(/) :: (Monad m, Fractional a) => a -> a -> m a

And IO not being a Haskell monad anymore, missing fail.