On Sat, 2004-12-18 at 21:19 +0100, Marcin 'Qrczak' Kowalczyk wrote:

Robert Dockins writes:

...

So, to be safe, the action of a finalizer must commute with every other finalizer (they must be central).

What does "should" mean?

I am suggesting that being "affine central" is a sufficent condition for being safe to run in a finalizer. It is likely that a weaker condition would also be sufficent. Trying to characterize this weaker condition seems important; unfortunatly, specifying exactily what actions are safe inside a finalizer would probably require analyzing the exact formal semantics of finalizers in Haskell. This sounds pretty complicated (especially given concurrency). I am not sure I have the skills, and I am not completely certain that the formal semantics of haskell finalizers has ever been spelled out. (anyone know?)

There are useful finalizers which don't have this property.

Some of them are broken, but happen to mostly work. In my mind "mostly works" is the same as "contins hard to find bugs."

E.g. a finalizer can remove an entry from a weak dictionary,

Interacting with weak pointers is one of those areas where I think you might be able to get away with something weaker than "affine central". I also think that some patterns of interacting with MVars are OK as well. 'tryPutMVar' seems pretty safe, as does 'modifyMVar'.

call a C function which will free some foreign object,

I think we can safely consider foreign calls which only release memory affine central.

or send a message over a network that a particular object is no longer needed.

Sending a network packet inside a finalizer sounds like a bad idea to me. I think that's exactily the kind of thing we want to keep people from doing. I would rather see a long running thread that is woken up by a finalizer that performs such actions. This has the advantage of allowing you to explicitly tell the thread to release all resources at program end. Even better, make sure to use bracket style allocations and avoid finalizers altogether (this seems like a must to me for remote or hardware resources).

...

So a separate ACIO monad for affine central IO actions would be the appropriate context for finalizers.

It would not be enough without unsafeIOtoACIO.

Fair enough. That at least flags the user that they have incurred a proof obligation.

There is a lot of interesting discussion on this list about finalizers in Java. It is hard to say exactily how much is transferable to the haskell setting. This appears to be the direction the java folks are leaning: http://www.cs.umd.edu/~pugh/java/memoryModel/archive/2266.html Andy Georges wrote:

On Saturday 18 December 2004 20:15, Robert Dockins wrote:

...

Due to one of the threads on cafe recently, I have been doing some thinking about finalizers.

Iirc, there was a rather large discussion on finalizers on the Java memory model list. Perhaps some useful ideas can be gathered from their proposal. I haven't read it in a while (and right now, I haven't got the time to do so), so I may be off track here.

http://www.cs.umd.edu/~pugh/java/memoryModel/

Regards, Andy _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe