Re: [m-users.] Impurity needed?

Volker Wysk <[email protected]>
Newsgroups gmane.comp.lang.mercury.general
Message-ID <[email protected]>
Am Mittwoch, dem 22.02.2023 um 03:23 +1100 schrieb Mark Brown:
> On Wed, Feb 22, 2023 at 12:23 AM Volker Wysk <[email protected]> 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 <[email protected]> wrote:
> > > > 
> > > > Am Dienstag, dem 14.02.2023 um 03:11 +1100 schrieb Zoltan Somogyi:
> > > > > 2023-02-14 02:13 GMT+11:00 "Volker Wysk" <[email protected]>:
> > > > > > > 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

_______________________________________________
users mailing list
[email protected]
https://lists.mercurylang.org/listinfo/users
signature.asc (application/pgp-signature, 833 B)
-----BEGIN PGP SIGNATURE-----

iQIzBAABCgAdFiEE6QXGh82Ov3+2nrxp+K4ydFOsHoUFAmP1qe4ACgkQ+K4ydFOs
HoVVQw/+Jf4V5+2eecIj/oMeiC+nr33o1hHst37gVKotKepsY5rSIsdGCrVErMFj
d+O/UwFb5bQ1ipXgaYC7X87F/W4tWT3bBviaO7Bb/NhH/SnzjLrHFa5ZaXAVddVS
D11zOFVPOR+2bCvHMQhTobND1gRr/MD9RT/kREvmUC1r9I43tzqt3V7Za+BCVDIb
Xl8iN2mLJ3CEILPoZxbsLs+0Zafn4Ue44vG9MREi8hNFgShhLbHoDBdnP3y2J+gY
e6ZR1RUkZG/YTBXV399RMzDuAdU581IUQIW/kZiLRcqVCbiiWU69FsmcuRXklrx3
Rr5tHyshKOvrhrSEG+JaL6DAkwz7agpJ80wuVhOrI6/dDWeW775zbcb60ae9QtHC
vRGvVurmwh6it9QCK4Jvz0W+muye/RGeoisJaMWeSHNZgIye2sIDf3jZ7/IY2d7R
g2bDVyK6JsQZqejh/h+Mt5kbstIufaduzgu+3bx9b4cy7C3YnNatdE+PhPXbqKPk
7mSCqsF4fRbxt92SwUMIZtLuT7tGn27X2ADWsmyAQWhobQSflE0pvUANiBYLb9QA
vfGssSXvW+xJ2qpawouC7hq8qxq1R3yM5lTKO/LghmxmIm2/FtxeHGhkyC5PLcwF
EBP3flsK7RVRXftLEBNAtHCB52MZZZlEnBHRHYa6rI3Pf+Z8h68=
=MF2g
-----END PGP SIGNATURE-----
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.