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. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
