Some classes of effectful programs
I'm going to do something unusual for this blog and talk about functional programming for a bit. Jessica Kerr wrote a blog post about the concept of idempotence as it's used in math and programming, and I decided I wanted to lay the ideas out in more familiar terms to me. So, consider a pure mini-ML with functions, products, numbers, lists, polymorphism, and let-binding, but no references (or other effects -- for the duration of this post I'm going to limit my notion of "effect" to references into a store). This is Language 1 (L1). Now consider adding references and sequencing to this language (i.e. new expressions are ref v , r := v , !r , and (e; e) ). This is Language 2 (L2). The operational semantics of Language 2 includes a store mapping references to values, for which I'll use the metavariable S. In addition to giving types T -> T' to L2 functions, we can give them store specifications S -o S' (using the linear implication symbol -o su