[m-users.] Impurity needed?

Volker Wysk post at volker-wysk.de
Wed Feb 22 16:36:46 AEDT 2023


Am Mittwoch, dem 22.02.2023 um 03:23 +1100 schrieb Mark Brown:
> On Wed, Feb 22, 2023 at 12:23 AM Volker Wysk <post at volker-wysk.de> wrote:
> > 
> > Am Dienstag, dem 21.02.2023 um 21:45 +1100 schrieb Mark Brown:
> > > On Tue, Feb 14, 2023 at 5:24 AM Volker Wysk <post at volker-wysk.de> wrote:
> > > > 
> > > > Am Dienstag, dem 14.02.2023 um 03:11 +1100 schrieb Zoltan Somogyi:
> > > > > 2023-02-14 02:13 GMT+11:00 "Volker Wysk" <post at volker-wysk.de>:
> > > > > > > It would be trivial to change the signature as you ask. It would also be
> > > > > > > a very bad idea to do so. The point of making an operation a transaction
> > > > > > > is to ensure that only two things can happen:
> > > > > > > 
> > > > > > > - the transaction succeeds, and ALL of its effects happen, or
> > > > > > > - the transaction fails, and NONE of its effects happen.
> > > > > > 
> > > > > > In my understanding, this applies only to the effects on the database...
> > > > > 
> > > > > Consider this sequence modelling an automatic teller machine:
> > > > > 
> > > > > 1. Start a transaction.
> > > > > 2. User specifies the account and the amount to withdraw.
> > > > > 3. Teller machine program commands cash dispenser
> > > > >     to give out the requested cash.
> > > > > 4. The program subtracts the amount from the account,
> > > > >     and discovers that the result is negative.
> > > > > 5. Because of this, the program aborts the transaction.
> > > > > 
> > > > > Disregard the fact that the test should have been done before
> > > > > giving out the requested cash. The point I am making is that
> > > > > giving out the cash should happen IF AND ONLY IF the same
> > > > > amount could be deducted from the account. Any violation
> > > > > of that rule either creates or destroys money. Creating money
> > > > > is illegal in most countries unless you are the central bank,
> > > > > and if you are anyone other than the central bank, you probably
> > > > > don't want to pointlessly destroy money either.
> > > > > 
> > > > > > > If you allowed I/O in the middle of a transaction, and then later
> > > > > > > it turned out that the transaction cannot succeed, then neither
> > > > > > > of those end states would be reachable.
> > > > > > 
> > > > > > So someone using a vanilla imperative language is forbidden to do IO when
> > > > > > being inside a transaction, too -?
> > > > > 
> > > > > In imperative language interfaces to DBMSs, there is no practical way to forbid
> > > > > the program to do I/O during a transaction, and, as your use case demonstrates,
> > > > > there are *some* kinds of I/O that you do want to permit. However, saying that
> > > > > database programmers should feel free to do ANY kind of I/O inside transactions
> > > > > is like saying that those programmers should feel free to point ANY device at the
> > > > > users of the database and pull the trigger, whether the device is a water pistol
> > > > > or a flame thrower.
> > > > 
> > > > I'm not saying that any kind of IO should be allowed inside transactions.
> > > > But how could a programming language restrict it to the right kinds of
> > > > IO?That isn't possible. It's the responsibility of the programmer to do it
> > > > right. In your example, he has the responsibility to first check the balance
> > > > of the account, before giving out the cash. You have to enable all kinds of
> > > > IO, so the correct ones are possible.
> > > 
> > > There's research being done in "coeffects" which I think includes
> > > things such as only allowing certain types of I/O.  Mercury's I/O
> > > mechanism can be thought of as a rudimentary coeffect system, and
> > > that's how it's being used in the library, but I think people are also
> > > interested in systems that allow more fine-grained control for
> > > situations like this.  As to what's currently possible I'm not sure,
> > > but I take your point about there being a need for at least some kinds
> > > of I/O.
> > 
> > Sounds advanced...
> 
> Perhaps so, I'm not sure of the current state of research.  Mercury
> and Clean were doing it long ago, at least for I/O. :-)
> 
> > 
> > So you think it would be okay to add the IO state to transactions in the
> > ODBC library? Such that IO in a transaction would be allowed? Of course the
> > programmer needs to be pointed to the fact that his IO actions can't be
> > backtracked.
> > 
> > Zoltan said this was a very bad idea...
> 
> Right, it would be unsafe in much the same way as unsafe_{get,set}_io,
> except the user's code wouldn't need to mention "unsafe" anywhere.  A
> better solution would be to use those as needed, which would at least
> alert people to the issue even if it can't be checked.

Maybe make two predicates: called "transaction" and "unsafe_transaction".
With only the latter allowing IO.


Cheers, Volker

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.mercurylang.org/archives/users/attachments/20230222/78696831/attachment.sig>


More information about the users mailing list