6
$\begingroup$

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?

$\endgroup$

migrated from cstheory.stackexchange.com Jun 19 '13 at 7:07

This question came from our site for theoretical computer scientists and researchers in related fields.

  • $\begingroup$ Please see cstheory.stackexchange.com/questions/4122/… $\endgroup$ – Vijay D Jun 18 '13 at 17:54
  • $\begingroup$ I do not even understand the question. Are talking about detection of potential or actual problems ? Is it to be done at compile time or at run time ?... $\endgroup$ – babou Jun 19 '13 at 13:31
  • $\begingroup$ I do not understand the question either. A Java-style "PrinterOutOfPaperException" could be construed as "requiring the programmer to handle a system failure." $\endgroup$ – James Koppel Jun 19 '13 at 20:43
  • $\begingroup$ @babou I'm talking about compile time. Not sure how do you distinguish potential problems from actual. If something bad could happen it will eventually happen :) $\endgroup$ – CheatEx Jun 20 '13 at 12:03
  • $\begingroup$ @JamesKoppel No, they only allow to ensure that we have some code block to execute in case of particular exception thrown. What I meant in the second case is ability to say if procedure 'a' maintains the system in recoverable state and procedure 'b' uses it in some "right" way than system is recoverable during entire 'b' execution. $\endgroup$ – CheatEx Jun 20 '13 at 12:04
6
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

As something on the more extreme end, there is $\lambda_{\text{zap}}$, a typed lambda calculus designed to handle transient hardware faults e.g. cosmic rays. It is described in Static Typing for a Faulty Lambda Calculus by Walker et al.

As for things like "pulling out the plug", this is typically handled by transactions. Since programming language data structures and computations are not usually intended to be durable, this is rarely built into a language and instead it's handled by database systems. There is work on static analysis on detecting when coordination is necessary such as the Dedalus/Bloom work, and when transactions can be weakened or eliminated such as the coordination avoidance work by Peter Bailis. Related is the techniques Rust uses to avoid concurrency issues utilizing its substructural type system.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.