patternMinor
What kinds of programming pitfalls modern languages are able to find?
Viewed 0 times
whatlanguagesareprogrammingkindspitfallsfindmodernable
Problem
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 pitfalls:
Haskell allows to express constraints required for safe handling of these situations. And compiler is able to warn programmer when he doesn't follow them.
Although pitfalls above are definitely the most common ones I can think of much more, for example:
Is there languages, libraries or at least models which allow to express constraints from the second set and yield a warning when they are not met?
- 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 allows to express constraints required for safe handling of these situations. And compiler is able to warn programmer when he doesn't follow them.
Although pitfalls above are definitely the most common ones I can think of much more, for example:
- Unexpected resource consumption. Memory, CPU, disk, bandwidth.
- Inconsistent access to shared resources. Like read and write interference, broken lock ordering.
- System-level failure. Like crashing process or pulled plugs.
- Unexpected execution time for IO, timing violation.
Is there languages, libraries or at least models which allow to express constraints from the second set and yield a warning when they are not met?
Solution
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.
-
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.
Context
StackExchange Computer Science Q#12759, answer score: 7
Revisions (0)
No revisions yet.