jeff1.61803:

On Feb 6, 2008 1:18 AM, Jonathan Cast <[1]jonathanccast@fastmail.fm> wrote:

On 5 Feb 2008, at 10:14 PM, Jeff I* wrote:

On Feb 5, 2008 4:58 PM, ChaddaA- FouchA(c) <[2]chaddai.fouche@gmail.com> wrote:

2008/2/5, Jeff I* <[3]jeff1.61803@gmail.com>: > This is interesting. I've been programming in Concurrent Clean for a while. > Instead of monads, Clean supports unique types for mutable arrays and IO. > In Clean, I can write code that iterates through a mutable array by > converting it to a lazy list. This is convenient because I can use all the > nice list processing functions that are available. >

You could absolutely write something like that in Haskell, but as some have pointed out, this is probably _not a Good Idea_, even though it works in your particular case, the array could be modified between the time you get the lazy list and the time you actually read it... And there's no way to insure it's not happening in Haskell, and I strongly doubt there is in Concurrent Clean, could you confirm ?

Concurrent Clean can handle this in a safe way. Here's a code snippet for normalize_2D_ary from ArrayTest.icl:

uToList_2D :: *(a u:(b c)) -> (.[c],*(a u:(b c))) | Array a (b c) & Array b c map_in_place_2d_arr :: (a -> a) *(b *(c a)) -> *(b *(c a)) | Array b (c a) & Array c a normalize_2D_ary :: *(a *(b c)) -> *(a *(b c)) | Array a (b c) & Array b c & / c & Ord c normalize_2D_ary ary = let (lst,ary2) = uToList_2D ary max_elem = foldl1 max lst in map_in_place_2d_arr (\ x -> x / max_elem) ary2 uToList_2D takes a unique array, ary, and returns a tuple containing a list of the array elements and a "new" array, ary2. uToList_2D does not modify ary, but Clean's type system forces any function that accesses a unique array to thread the array through and return a "new" array. Under the hood the "new" array actually uses the same memory storage as the original array. So, it is effecient. Threading the array serializes access insuring the array won't be modified until the list is complete.

I'm confused --- does uToList_2D return the head of the list before or after it finishes reading the array? If before, then I don't see how the type system prevents me from modifying the array before I finish examining the list, as you claim. If after, then the list isn't truly lazy.

uToList_2D can return the head of the list before it finishes reading the array. I could modify the code so that it is ambiguous whether the array is modified before the list processing is finished.

normalize_2D_ary ary = let (lst,ary2) = uToList_2D ary max_elem = foldl1 max lst in map_in_place_2d_arr (\ x -> x / max_elem) ary // I changed ary2 to ary

However, the type system will generate an error with this code because ary is no longer unique because it is referenced in two expressions. Clean produces this error message:

Uniqueness error [ArrayTest.icl,55,normalize_2D_ary]: "ary" demanded attribute cannot be offered by shared object

I should mention that a problem with the code I've shown is that it is very sensitive to the order in which the expression graph is evaluated. Simple changes can cause lst to become strict and the program to run out of heap. By the way, Clean has it's share of rough edges. The reason I'm hanging out on Haskell-Cafe is because I'm trying to get away from those rough edges. But, I am missing Clean's uniqueness types. I'm starting to see Haskell's unsafe functions as a blunt work around that could be fixed elegantly and safely by implementing uniqueness types.

That's a reasonable critique : its hard to enforce uniqueness, in the type system in Haskell, -- I'd be interesting to see approaches that avoid extending the compiler. -- Don

On Feb 6, 2008, at 12:12 , Peter Verswyvelen wrote:

...

That's a reasonable critique : its hard to enforce uniqueness, in the type system in Haskell, -- I'd be interesting to see approaches that avoid extending the compiler.

Isn't the compiler already "modified" in a way to deal with the RealWorld type that is used in the IO monad? Surely the RealWorld is unique...

You might want to look at the definition of unsafePerformIO before asserting that. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

Hi

Isn't the compiler already "modified" in a way to deal with the RealWorld type that is used in the IO monad? Surely the RealWorld is unique...

No. The monad and the primitive operations ensure it is unique, the IO monad is abstracted away properly, and it all works neatly so you can't violate the uniqueness. However, the realWorld thing is not actually unique, for example unsafeInterleaveIO and unsafePerformIO violate this. Thanks Neil

On 2/6/08, Peter Verswyvelen wrote:

Yeah, I also believed that, but then I'm confused:

So monads *do* enforce uniqueness... So what is the difference between Haskell's monad approach and Clean's uniqueness typing? I always thought these were just two different ways to tackle the same problem, and I had the feeling Haskell's approach was actually more general.

IO and mutable array monads could be implemented on top of Clean's unique arrays and world objects. So, I'd argue that Clean is at least as general as Haskell. On the other hand, I've posted two similar problems to this list. In Haskell I want to . . . 1) turn a mutable array into a lazy list 2) turn the contents of a file into a lazy list The responses I've received are typically: 1) Use unsafeFreeze / unsafeThaw 2) Use hGetContents. (which uses unsafePeformIO under the hood.) 3) Don't use a lazy list. Rewrite the code to break the data up into smaller chunks and process the chunks in a loop. I have solved both of these problems in Clean using a lazy list without resorting to unsafe operations. So, it seems to me that uniqueness types are more general than monads. By the way, I'm not good enough to use unsafe functions. My code would crash for sure. :-)

2008/2/6, Jeff φ :

I have solved both of these problems in Clean using a lazy list without resorting to unsafe operations. So, it seems to me that uniqueness types are more general than monads.

Are you aware that your code in Clean has some issues, like the lst not being so lazy if you operate on ary2 before you operate on lst (it is completely put in memory in this case) ? You've effectively created a big uncertainty on the space taken by your function. Is this ok with you ? The monadic fold (like I and some others proposed) guarantee you a constant amount of memory consumed and is perfectly safe too, is the Clean solution really so much better ? Jonathan Cast :

I'm confused --- does uToList_2D return the head of the list before or after it finishes reading the array? If before, then I don't see how the type system prevents me from modifying the array before I finish examining the list, as you claim. If after, then the list isn't truly lazy.

What happens here is that the array can't be modified without evaluating ary2 and ary2 can't be evaluated without completely evaluating the list before, so you effectively get the list lazily as long as you don't touch ary2 before touching the list, and you can't damage the list by modifying the array (because in this case, lst would be completely evaluated in the first place). You can do the same in Haskell in fact, but you'll need to discipline yourself to evaluate the "witness" before modifying the array. So uniqueness here seems to have an advantage over monads, still, the monads look much cleaner (sic) than Clean code with all those unique value passing around... -- Jedaï

Hello Jeff, Thursday, February 7, 2008, 1:31:59 AM, you wrote:

I noticed that GHC implements mutable arrays in the IO monad.  This seems odd to me.  Arrays aren't related to IO. 

IO monad isn't only about I/O but about imperative stuff in general. there is also special monad limited to mutable vars and arrays, namely ST. read also this: http://haskell.org/haskellwiki/Modern_array_libraries http://haskell.org/haskellwiki/IO_inside -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

IO(U)Arrays are only one variant of mutable Array, there are also ST(U)Arrays, which are often preferred.

I should have worded my question better. The MArray interface is implemented in both the ST and IO monad. A state monad seems like a logical place for mutable arrays. However, I don't understand the motivation for implementing it in IO. Were mutable arrays added to IO because it would be difficult to write code that does both IO and manipulates arrays otherwise?

Hello Jeff, Thursday, February 7, 2008, 4:17:27 AM, you wrote:

logical place for mutable arrays.  However, I don't understand the motivation for implementing it in IO.  Were mutable arrays added to IO because it would be difficult to write code that does both IO and manipulates arrays otherwise?

yes. you can't perform separate ST actions in IO monad, you may call only entire computations with pure results - the same as you can do from pure code IO monad implements idea of sequencing actions and it is used ro "import" any actions written in other languages (C/C++ in most cases). ST monad is just the same internally but it was directive limited to only two types of actions - with variables and mutable arrays. this, together with some type tricks ensures that its results are referentially-transparent and therefore may be called from pure code -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

I see. Unfortunately I did not spent enough time playing with Clean, and I'm still learning Haskell, so I can't give any feedback on your questions J Now from the little time I've spent in the company of Clean, I must say there's another advantage of uniqueness typing: it is very easy to understand. While monads are a tiny bit more demanding! But monads give such a mental satisfaction once you see the light ;-) So you say uniqueness typing might be more general. Can one make list monads and all the other funky Haskell monads with Clean's uniqueness typing then? Peter From: Jeff φ [mailto:jeff1.61803@gmail.com] Sent: woensdag 6 februari 2008 20:21 To: Peter Verswyvelen; Neil Mitchell; Don Stewart Cc: haskell-cafe@haskell.org Subject: Re: [Haskell-cafe] Mutable arrays On 2/6/08, Peter Verswyvelen wrote: Yeah, I also believed that, but then I'm confused: So monads *do* enforce uniqueness... So what is the difference between Haskell's monad approach and Clean's uniqueness typing? I always thought these were just two different ways to tackle the same problem, and I had the feeling Haskell's approach was actually more general. IO and mutable array monads could be implemented on top of Clean's unique arrays and world objects. So, I'd argue that Clean is at least as general as Haskell. On the other hand, I've posted two similar problems to this list. In Haskell I want to . . . 1) turn a mutable array into a lazy list 2) turn the contents of a file into a lazy list The responses I've received are typically: 1) Use unsafeFreeze / unsafeThaw 2) Use hGetContents. (which uses unsafePeformIO under the hood.) 3) Don't use a lazy list. Rewrite the code to break the data up into smaller chunks and process the chunks in a loop. I have solved both of these problems in Clean using a lazy list without resorting to unsafe operations. So, it seems to me that uniqueness types are more general than monads. By the way, I'm not good enough to use unsafe functions. My code would crash for sure. :-)

Peter Verswyvelen wrote:

So monads *do* enforce uniqueness... So what is the difference between Haskell's monad approach and Clean's uniqueness typing? I always thought these were just two different ways to tackle the same problem, and I had the feeling Haskell's approach was actually more general.

Yes (1), and no (2). ! Long pedantic post follows (1) They are two different ways to tackle the same problem: how to have I/O in a pure functional language when I/O neccessarily requires the "world state" to be destructively updated (e.g. we can't copy the entire filesystem, or the (truly) global internet state). The solution is based on the following observation: imagine we a have a large datastructure (e.g. big tree) and a function that updates it, then, *in general*, pure functional semantics requires the implementation to return a copy of its argument with the update applied, leaving the original argumment intact. However, if in a given program, we know that the old value of the big structure is never referenced once the function is applied, then we can *implement* the function application "under the hood" as a true destructive update, without breaking the pure referential semantics of the language. Such a use of a structure in a program is said to "single-threaded". For example, the program f (g (h bigThing)) makes single-threaded use of bigThing, so *in this program*, we could implement f, g and h using destructive update without altering the outcome as predicted by a copy semantics. However, the program (bigThing,h bigThing) does not have a single-threaded use of bigThing, so h *must* be implemented using copying, because we have access to both values. The upshot of all of this is that a program that restricts itself to single-threaded use of a (large) structure can use a desctructive implementation, so if we can ensure that our patterns of I/O access are single-threaded, then we can: - implement I/O as we must, i.e with destructive update - yet still maintain the "illusion" that our program is pure (copying). What's the catch? Well, in general, the question of wether or not a given structure's use is single-threaded, is undecidable. So what we have are two (partial) solutions: Clean's uniqueness types, and Haskell's monads. Let us assume that the entire I/O state is captured by a variable world :: World "Invent-and-Verify": Clean allows you to write a program that explicity mentions world, and the uses the type-system to check that accesses to world are single-threaded. Essentially the destructive functions have type annotations that insist their World arguments and results are singly-threaded (a.k.a. "unique"). So program writefile "a.dat" "Text A" (writefile "b.dat" "Text B" world) typechecks, but program (world,writefile "b.dat" "Text B" world) doesn't. Because of undecidability, the type-checker is not totally accurate, but behaves conservatively, so may report a program as ill-typed, even if it is actually single-threaded, but will always spot a program that is truly bad - not single-threaded. "Correctness-by-Construction": Haskell approaches the problem by hiding the world inside an abstract data-type called a monad. Haskell programs do not mention the world explicitly at all. The monad, with its return, bind and basic monadic I/O operations is setup so that the hidden world state is always accessed in a single-threaded fashion,so the underlying implementation is free to use desctructive update. So we can write a monadic form of the first program above, as do writefile "b.dat" "Text B" writefile "a.dat" "Text A" We cannot begin to express the second (ill-typed) program at all ! (2) Leaving aside the fact that the monad concept is more general than just I/O (Maybe monad, List monad, etc..), we can state categorically that as far as I/O is concerned, that Clean's uniqueness type approach is more general than Haskell's monads, i.e.: - any Haskell monad-IO program can be re-written as a correctly typed Clean IO program (simply "implement" the IO monad as a state monad over a state world :: World). - not all Clean IO programs can be directly written in monadic style. The issue has to do with the fact that the IO monad "over-sequences" IO actions, because the monad encapsulates the entire world in one lump. (see slides 37/38 of http://research.microsoft.com/~simonpj/papers/haskell-retrospective/HaskellR...). So if we have two functions, one, f1 :: IO (), reading from file "f1.in" and writing to "f1.out", and the other, f2 :: IO () reading from "f2.in" and writing to "f2.out", we must decide as programmers what order to use - either do{ f1 ; f2 } or do { f2; f1 }. If we generalise to f1 .. fn, we have to sequence these, which is why the function in Haskell of type [IO a] -> IO [a], is called "sequence". In Clean, we not only have explicit access to the world, but we can partition it. Simplifying somewhat, we could open up pairs of file-handle (f1.in,f1.out), (f2.in,f2,out) ... (fn.in,fn.out), which does have to be done sequentially, since each file opening modifies the (global) filesystem. However, once this is done, we could, in principle, execute the fn in any order, and indeed in such a way that the implementation could choose to do them in parallel - this potential for (admittedly limited) deterministic parallel execution of I/O actions is possible with uniqueness types, but not epxressible in the monadic world as currently formulated. (3) Shameless plug : a semantics for I/O that covers both Clean and Haskell and which scopes out the "deterministic parallelism" alluded to above was described in Malcolm Dowse, Andrew Butterfield: Modelling deterministic concurrent I/O. ICFP 2006: 148-159 http://doi.acm.org/10.1145/1159803.1159823 -- -------------------------------------------------------------------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Foundations and Methods Research Group Director. Department of Computer Science, Room F.13, O'Reilly Institute, Trinity College, University of Dublin, Ireland. http://www.cs.tcd.ie/Andrew.Butterfield/ --------------------------------------------------------------------

Stefan O'Rear wrote:

On Wed, Feb 06, 2008 at 08:57:43PM +0000, Andrew Butterfield wrote:

...

In Clean, we not only have explicit access to the world, but we can partition it. Simplifying somewhat, we could open up pairs of file-handle (f1.in,f1.out), (f2.in,f2,out) ... (fn.in,fn.out), which does have to be done sequentially, since each file opening modifies the (global) filesystem. However, once this is done, we could, in principle, execute the fn in any order, and indeed in such a way that the implementation could choose to do them in parallel - this potential for (admittedly limited) deterministic parallel execution of I/O actions is possible with uniqueness types, but not epxressible in the monadic world as currently formulated.

What if f1.out is a symlink to f2.out? I don't think Clean satisfies the evaluation order independance that is so treasured here.

Sorry for lateness in getting back - it's been one of those fortnights.. The case you mention won't arise simply because during the process of opening these file-handles (which cannot be done in parallel, because they all modify the filesystem), the write conflict will be detected, and the opening of the second one will fail. Once the file-handle pairs are all opened we have a guarantee that all writes are to distinct files. -- -------------------------------------------------------------------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Foundations and Methods Research Group Director. Course Director, B.A. (Mod.) in CS and ICT degrees, Year 4. Department of Computer Science, Room F.13, O'Reilly Institute, Trinity College, University of Dublin, Ireland. http://www.cs.tcd.ie/Andrew.Butterfield/ --------------------------------------------------------------------