Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    text
    copied!<p>A "type and effect system" describes not only the kinds of values in a program, but the changes in those values. "Typestate" checking is a related idea.</p> <p>An example might be a type system that tracks file handles: instead of having a function <code>close</code> with return type <code>void</code>, the type system would record the <em>effect</em> of <code>close</code> as disposing of the file resource&mdash;any attempt to read from or write to the file after calling <code>close</code> would become a type error.</p> <p>I'm not aware of any type and effect system appearing in a mainstream programming language. They have been used to define static analyses (for example, it's quite natural to define an analysis for proper locking/unlocking in terms of effects). As such, effect systems are usually defined using inference schemes rather than concrete syntax. You could imagine a syntax looking something like</p> <pre><code>File open(String name) [+File]; // open creates a new file handle void close(File f) [-f] ; // close destroys f </code></pre> <p>If you want to learn more, the following papers might be interesting (fair warning: the papers are quite theoretical).</p> <ul> <li><a href="http://slang.soe.ucsc.edu/cormac/papers/atomic-toplas.pdf" rel="noreferrer">Types for Atomicity: Static Checking and Inference for Java</a>. Flanagan, Freund, Lipshin, and Qadeer.</li> <li><a href="http://research.microsoft.com/~maf/Papers/pldi01.pdf" rel="noreferrer">Enforcing High-Level Protocols in Low-Level Software</a>. Robert DeLine and Manuel Fändrich.</li> <li><a href="http://www.cs.ucla.edu/~palsberg/tba/papers/nielson-nielson-csd99.pdf" rel="noreferrer">Type and Effect Systems</a>. Nielson and Nielson.</li> </ul>
 

Querying!

 
Guidance

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload