Problem Detail: I often see claims that modern functional strictly-typed languages are ‘safer’ than others. These statement mostly linked with type systems and their ability to explicitly express the following sources of pitfalls:
- Alternatives in function result. Maybe and Either datatypes vs. exceptions and null-pointers in C++-like languages.
- Access to mutable state (possibly inconsistent behavior over time). State datatype in Haskell vs. variables in C++-like languages.
- Performing IO. IO datatype in Haskell vs. just doing things in C++-like languages.
Haskell compiler is able to warn programmer when he doesn’t properly handle theses kinds risky operations. Althought pitfalls above are definitely the most common ones I can see much more, for example:
- Unexpected resource consumption. Memory or CPU, the former is common for Haskell AFAIK.
- System-level failure. Like crashing process or pulled plug.
- Unexpected execution time for IO, timing violation.
Is there languages, libraries or at least models which allow to express risks from the second set and yield a warning when they are not handled?
Asked By : CheatEx
Answered By : James Koppel
Substructural types ( http://en.wikipedia.org/wiki/Substructural_type_system ) can be used to provide some version of each of those. As a summary, while normal types control how something may be used, substructural types further control when or how often it may be used.
- Affine types can be used to construct languages capable of expressing all, and only, polynomial-time functions. http://www.cs.cmu.edu/~fp/courses/15816-s12/misc/aehlig02tocl.pdf
- Linear types can enforce that memory is accessible when variables go out of scope, enabling a kind of “static garbage collection.” Similarly, ordered types can be used to require that variables are used in a LIFO order, allowing them to be stack-allocated. Regions ( http://en.wikipedia.org/wiki/Region-based_memory_management ) are also useful here. The first chapter of Advanced Topics in Types and Programming Languages provides a nice introduction to using linear and ordered types for this purpose.
- Affine types also enable typestate-oriented programming ( http://www.cs.cmu.edu/~aldrich/papers/onward2009-state.pdf ). Typestate is used to enforce certain orderings in APIs (e.g.: can’t read from a closed file), but can also be used to enforce safety properties. Requiring a block that handles some error can be encoded as requiring a function that transitions some object from an error state to a recovery state.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/12759 Ask a Question Download Related Notes/Documents
