Patrick Logan wrote:
>
> In "Rolling Your Own Mutable ADT: A Connection Between Linear Types
> and Monads", p. 1, Chen and Hudak write:
>
> There are few formal connections between monads and
> single-threaded state... For any state-transformer monad... there
> is a trivial operation... that will instantly destroy any hope for
> single-threadedness: getState s = (s, s)
>
> In day-to-day Haskell 1.3 programming what is the solution to this
> problem? If a program is using a C interface to create a mutable
> state, say an external database, what is the simplest way of
> encapsulating the state so that this "trivial operation" cannot be
> defined except by the original author?
I don't think that either Alastair or Simon really addressed Patrick's
question, which is really two-fold:
1) how do you design the ADT in the first place to be sure that the
state is single-threaded, and
2) how do you implement the ADT correctly once you've designed it
My paper with Chen gives a strategy for doing (1). It also hints how
you could do (2) with a suitably smart compiler, although does not say
anything about how to do it in C, which opens a whole new can of worms.
What we had in mind is that a user could write an ADT, wrap it up in a
module, and then, if the ADT passes a particular linearity test (which
would reject operations like "getState" above), a smart compiler could
implement the state "in situ", which you can think of as a form of
compile-time GC.
But as I said, I don't know how to formally guarantee this for a given C
implementation, which, for example, would clearly require a formal
operational semantics for C.
-Paul
