[Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe
Timon Gehr wrote: I am not sure that the two statements are equivalent. Above you say that the context distinguishes x == y from y == x and below you say that it distinguishes them in one possible run. I guess this is a terminological problem. The phrase `context distinguishes e1 and e2' is the standard phrase in theory of contextual equivalence. Here are the nice slides http://www.cl.cam.ac.uk/teaching/0910/L16/semhl-15-ann.pdf Please see adequacy on slide 17. An expression relation between two boolean expressions M1 and M2 is adequate if for all program runs (for all initial states of the program s), M1 evaluates to true just in case M2 does. If in some circumstances M1 evaluates to true but M2 (with the same initial state) evaluates to false, the expressions are not related or the expression relation is inadequate. See also the classic http://www.ccs.neu.edu/racket/pubs/scp91-felleisen.ps.gz (p11 for definition and Theorem 3.8 for an example of a distinguishing, or witnessing context). In essence, lazy IO provides unsafe constructs that are not named accordingly. (But IO is problematic in any case, partly because it depends on an ideal program being run on a real machine which is based on a less general model of computation.) I'd agree with the first sentence. As for the second sentence, all real programs are real programs executing on real machines. We may equationally prove (at time Integer) that 1 + 2^10 == 2^10 + 1 but we may have trouble verifying it in Haskell (or any other language). That does not mean equational reasoning is useless: we just have to precisely specify the abstraction boundaries. BTW, the equality above is still useful even in Haskell: it says that if the program managed to compute 1 + 2^10 and it also managed to compute 2^10 + 1, the results must be the same. (Of course in the above example, the program will probably crash in both cases). What is not adequate is when equational theory predicts one finite result, and the program gives another finite result -- even if the conditions of abstractions are satisfied (e.g., there is no IO, the expression in question has a pure type, etc). I think this context cannot be used to reliably distinguish x == y and y == x. Rather, the outcomes would be arbitrary/implementation defined/undefined in both cases. My example uses the ST monad for a reason: there is a formal semantics of ST (denotational in Launchbury and Peyton-Jones and operational in Moggi and Sabry). Please look up ``State in Haskell'' by Launchbury and Peyton-Jones. The semantics is explained in Sec 6. Please see Sec 10.2 Unique supply trees -- you might see some familiar code. Although my example was derived independently, it has the same kernel of badness as the example in Launchbury and Peyton-Jones. The authors point out a subtlety in the code, admitting that they fell into the trap themselves. So, unsafeInterleaveST is really bad -- and the people who introduced it know that, all too well. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]
Lazy I/O *sounds* safe. And most of the alternatives (like conduits) hurt my head, so it is really *really* tempting to stay with lazy I/O and think I'm doing something safe. Well, conduit was created for the sake of a web framework. I think all web frameworks, in whatever language, are quite complex, with a steep learning curve. As to alternatives -- this is may be the issue of familiarity or the availability of a nice library of combinators. Here is the example from my FLOPS talk: count the number of words the in a file. Lazy IO: run_countTHEL fname = readFile fname = print . length . filter (==the) . words Iteratee IO: run_countTHEI fname = print = fileL fname $ wordsL $ filterL (==the) $ count_i The same structure of computation and the same size (and the same incrementality). But there is even a simple way (when it applies): generators. All languages that tried generators so far (starying from CLU and Icon) have used them to great success. Derek Lowe has a list of Things I Won't Work With. http://pipeline.corante.com/archives/things_i_wont_work_with/ This is a really fun site indeed. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Set monad
One problem with such monad implementations is efficiency. Let's define
step :: (MonadPlus m) = Int - m Int
step i = choose [i, i + 1]
-- repeated application of step on 0:
stepN :: (Monad m) = Int - m (S.Set Int)
stepN = runSet . f
where
f 0 = return 0
f n = f (n-1) = step
Then `stepN`'s time complexity is exponential in its argument. This is
because `ContT` reorders the chain of computations to right-associative,
which is correct, but changes the time complexity in this unfortunate way.
If we used Set directly, constructing a left-associative chain, it produces
the result immediately:
The example is excellent. And yet, the efficient genuine Set monad is
possible.
BTW, a simpler example to see the problem with the original CPS monad is to
repeat
choose [1,1] choose [1,1] choose [1,1] return 1
and observe exponential behavior. But your example is much more
subtle.
Enclosed is the efficient genuine Set monad. I wrote it in direct
style (it seems to be faster, anyway). The key is to use the optimized
choose function when we can.
{-# LANGUAGE GADTs, TypeSynonymInstances, FlexibleInstances #-}
module SetMonadOpt where
import qualified Data.Set as S
import Control.Monad
data SetMonad a where
SMOrd :: Ord a = S.Set a - SetMonad a
SMAny :: [a] - SetMonad a
instance Monad SetMonad where
return x = SMAny [x]
m = f = collect . map f $ toList m
toList :: SetMonad a - [a]
toList (SMOrd x) = S.toList x
toList (SMAny x) = x
collect :: [SetMonad a] - SetMonad a
collect [] = SMAny []
collect [x] = x
collect ((SMOrd x):t) = case collect t of
SMOrd y - SMOrd (S.union x y)
SMAny y - SMOrd (S.union x (S.fromList y))
collect ((SMAny x):t) = case collect t of
SMOrd y - SMOrd (S.union y (S.fromList x))
SMAny y - SMAny (x ++ y)
runSet :: Ord a = SetMonad a - S.Set a
runSet (SMOrd x) = x
runSet (SMAny x) = S.fromList x
instance MonadPlus SetMonad where
mzero = SMAny []
mplus (SMAny x) (SMAny y) = SMAny (x ++ y)
mplus (SMAny x) (SMOrd y) = SMOrd (S.union y (S.fromList x))
mplus (SMOrd x) (SMAny y) = SMOrd (S.union x (S.fromList y))
mplus (SMOrd x) (SMOrd y) = SMOrd (S.union x y)
choose :: MonadPlus m = [a] - m a
choose = msum . map return
test1 = runSet (do
n1 - choose [1..5]
n2 - choose [1..5]
let n = n1 + n2
guard $ n 7
return n)
-- fromList [2,3,4,5,6]
-- Values to choose from might be higher-order or actions
test1' = runSet (do
n1 - choose . map return $ [1..5]
n2 - choose . map return $ [1..5]
n - liftM2 (+) n1 n2
guard $ n 7
return n)
-- fromList [2,3,4,5,6]
test2 = runSet (do
i - choose [1..10]
j - choose [1..10]
k - choose [1..10]
guard $ i*i + j*j == k * k
return (i,j,k))
-- fromList [(3,4,5),(4,3,5),(6,8,10),(8,6,10)]
test3 = runSet (do
i - choose [1..10]
j - choose [1..10]
k - choose [1..10]
guard $ i*i + j*j == k * k
return k)
-- fromList [5,10]
-- Test by Petr Pudlak
-- First, general, unoptimal case
step :: (MonadPlus m) = Int - m Int
step i = choose [i, i + 1]
-- repeated application of step on 0:
stepN :: Int - S.Set Int
stepN = runSet . f
where
f 0 = return 0
f n = f (n-1) = step
-- it works, but clearly exponential
{-
*SetMonad stepN 14
fromList [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14]
(0.09 secs, 31465384 bytes)
*SetMonad stepN 15
fromList [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15]
(0.18 secs, 62421208 bytes)
*SetMonad stepN 16
fromList [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]
(0.35 secs, 124876704 bytes)
-}
-- And now the optimization
chooseOrd :: Ord a = [a] - SetMonad a
chooseOrd x = SMOrd (S.fromList x)
stepOpt :: Int - SetMonad Int
stepOpt i = chooseOrd [i, i + 1]
-- repeated application of step on 0:
stepNOpt :: Int - S.Set Int
stepNOpt = runSet . f
where
f 0 = return 0
f n = f (n-1) = stepOpt
{-
stepNOpt 14
fromList [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14]
(0.00 secs, 515792 bytes)
stepNOpt 15
fromList [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15]
(0.00 secs, 515680 bytes)
stepNOpt 16
fromList [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]
(0.00 secs, 515656 bytes)
stepNOpt 30
fromList
[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30]
(0.00 secs, 1068856 bytes)
-}
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] I would like to know how to use the following events handlers : dropTargetOnData, dropTargetOnDrop, dropTargetOnEnter,
If you have figured it all out, I hope you want to write a HaskellWiki page about it. If I pass the gating, I ll publish a kind some HowTo on the differente techniques I dig out already started with this one, where I published my finding in the answer: http://stackoverflow.com/questions/15867654/wx-haskell-drag-and-drop-example As no one else has responded so far, I think you are in uncharted territory; wxHaskell is huge and there are not many applications using it. good point. ! do we have some kind of census of application that wrok or still work with wxhaskell ? any interest in (me) doing this ? (who know some toosl to do this, a la doodle ?) and by extension : btw how many people are really active and resonably knowleadeable these day ? (e.g. senior) Are Eric ? Jeremy ? atzedijkstra ? yourself ? still active on wx. and are you using it yourself HenkJan ? is :https://github.com/atzedijkstra/wxHaskell the head dev for these day ? i.e. who is the maintainer ? ( Sorry for all these questions, but I am just discovering the field :-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]
On Fri, Apr 12, 2013 at 1:44 AM, o...@okmij.org wrote: As to alternatives -- this is may be the issue of familiarity or the availability of a nice library of combinators. It is certainly not just a matter of familiarity, nor availability. Rather, it's a matter of the number of names that are required in a working set. Any Haskell programmer, regardless of whether they use lazy I/O, will already know the meanings of (.), length, and filter. On the other hand, ($), count_i, and filterL are new names that must be learned from yet another library -- and much harder than learned, also kept in a mental working set of fluency. This ends up being a rather strong argument for lazy I/O. Not that the code is shorter, but that it (surprisingly) unifies ideas that would otherwise have required separate vocabulary. I'm not saying it's a sufficient argument, just that it's a much stronger one than familiarity, and that it's untrue that some better library might achieve the same thing without the negative consequences. (If you're curious, I do believe that it often is a sufficient argument in certain environments; I just don't think that's the kind of question that gets resolved in mailing list threads.) -- Chris Smith ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: psqueue-benchmarks - benchmarks of priority queue implementations
I actually found a (potential) problem with the GHC implementation. See here: https://github.com/nh2/psqueue-benchmarks/blob/db89731c5b4bdd2ff2ef81022a65f894036d8453/QueueBenchmark.hs#L44 If I fromList 100 entries into the queue, it stack space overflows. I got the same problem with the fingertree implementation, so maybe I just construct the test case wrong and cause the stack space overflow myself, but it works with the other two implementations. Also, looking at the updated graph: http://htmlpreview.github.com/?https://raw.github.com/nh2/psqueue-benchmarks/master/report.html we can see that GHC's queue is 3 times slower than queuelike for findmin sequential. Where could the stack overflows come from? Niklas On 30/03/13 09:07, Kazu Yamamoto (山本和彦) wrote: Hi Niklas, No, it does not stack overflow, and it seems to perform slightly better than the other implementations; it also doesn't suffer from the toList slowness problem as does listlike. Thanks. It's nice. However, it is probably not as generally usable as it hardcodes the priorities to be Doubles. I think that you can import the tips of GHC PSQ to original PSQ. P.S. If you need test cases, you can find some properties for Heap (priority queue) here: https://github.com/kazu-yamamoto/llrbtree/blob/master/test/Heap.hs You can add some properties relating dilatation to them. --Kazu ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Warsaw Haskell Group
Hello! We are organizing a group of Haskell fans from Warsaw, Poland. So far we have set up a community on G+ (https://plus.google.com/u/0/communities/103183708602453146804), a mailing list is on the way. We would like to meet regularly someplace in the capital (we still decide where), and hack on Haskell together as much as we can :) Should there be more people involved, we could arrange regular lectures. Hope to see you there! Warsaw Haskell Group ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: psqueue-benchmarks - benchmarks of priority queue implementations
Does not compiles under ghc 7.6.2 Date: Sat, 13 Apr 2013 11:09:13 +0800 From: m...@nh2.me To: k...@iij.ad.jp CC: haskell-cafe@haskell.org Subject: Re: [Haskell-cafe] ANN: psqueue-benchmarks - benchmarks of priority queue implementations I actually found a (potential) problem with the GHC implementation. See here: https://github.com/nh2/psqueue-benchmarks/blob/db89731c5b4bdd2ff2ef81022a65f894036d8453/QueueBenchmark.hs#L44 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] GSoC proposal: Data Visualization
Dear Haskell Community, During the last months I used Haskell for machine learning, particularly in the field of Echo State Neural Networks. The main drawback I encountered is that its difficult to visualize and plot data in Haskell in spite the fact there are a couple of plotting libraries. Data visualization is very important in the field of machine learning research (not so much in machine learning implementation) since humans are very efficient to analyze graphical input to figure out what is going on in order to determine possible adjustments. I was wondering if other members of the community have experienced this drawback and would be interested in improved data visualization for Haskell, especially if there is interest to use Haskell for machine learning research. I collected my ideas in the following page: https://github.com/netogallo/Visualizer . Please provide me with feedback because if the proposal is interesting for the community I would start working with it, even if it doesn't make it to this GSoC, but a project like this will need a lot of collaboration for it to be successful. Thank you very much, Best Regards, Ernesto -- Ernesto Rodriguez Bachelor of Computer Science - Class of 2013 Jacobs University Bremen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Will Haskell Platform 2012.4.0.0 uninstall cleanly for the installation of 2013.2.0.0
On Fri, 12 Apr 2013 00:42:15 +0200, KC kc1...@gmail.com wrote: :) You don't really need to uninstall the platform, unless your disk is running out of space; just change your search path (that's actually done automatically at installation time). If you keep the old platform, you can test your latest (versions of) packages with a previous compiler. Note, that re-installing an old platform may cause a lot of trouble, because cabal-install might select incompatible versions of packages. Regards, Henk-Jan van Tuyl -- http://Van.Tuyl.eu/ http://members.chello.nl/hjgtuyl/tourdemonad.html Haskell programming -- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GSoC proposal: Data Visualization
Hello Ernesto, There are a number of efforts underway to provide better data vis libraries for haskell. Likewise, there was some recent discussion on the Diagrams mailing list about data vis tooling, and there should be a few interesting tools surfacing over the coming few months. My immediate concern is that this project is too broad and undefined in scope to be a successful Haskell GSOC. A successful GSOC project should have a) a clear notion of what project's goal is b) clear evidence that the planned work can reasonably be done over the summer c) the result of a successful project would be valuable to the general haskell community It sounds like the core of what you want to do is write a small lib that transforms a data set from some initial schema into the schema thats suitable for some underlying choice in plotting tool. This is a useful thing to do, but not large enough in scope for a GSOC project. On the flip side, interactive data vis tools are *hard* to do well, and a GSOC that proposed to work on that from scratch would be very very risky unless you've spent a lot of time working on building such tools. You're definitely pointing at region of library space where more nice tools for haskell would be very valuable, and which a number of folks are trying to address. But, for GSOC, unless its a very very clearly laid out proposal, it will be deemed too risky. I warmly recommend you look at prior years' Haskell GSOC projects to get a feel for what strong successful projects/proposals look like. cheers -Carter On Fri, Apr 12, 2013 at 5:10 PM, Ernesto Rodriguez n...@netowork.me wrote: Dear Haskell Community, During the last months I used Haskell for machine learning, particularly in the field of Echo State Neural Networks. The main drawback I encountered is that its difficult to visualize and plot data in Haskell in spite the fact there are a couple of plotting libraries. Data visualization is very important in the field of machine learning research (not so much in machine learning implementation) since humans are very efficient to analyze graphical input to figure out what is going on in order to determine possible adjustments. I was wondering if other members of the community have experienced this drawback and would be interested in improved data visualization for Haskell, especially if there is interest to use Haskell for machine learning research. I collected my ideas in the following page: https://github.com/netogallo/Visualizerhttps://github.com/netogallo/Visualizer . Please provide me with feedback because if the proposal is interesting for the community I would start working with it, even if it doesn't make it to this GSoC, but a project like this will need a lot of collaboration for it to be successful. Thank you very much, Best Regards, Ernesto -- Ernesto Rodriguez Bachelor of Computer Science - Class of 2013 Jacobs University Bremen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe
On 04/12/2013 10:24 AM, o...@okmij.org wrote: Timon Gehr wrote: I am not sure that the two statements are equivalent. Above you say that the context distinguishes x == y from y == x and below you say that it distinguishes them in one possible run. I guess this is a terminological problem. It likely is. The phrase `context distinguishes e1 and e2' is the standard phrase in theory of contextual equivalence. Here are the nice slides http://www.cl.cam.ac.uk/teaching/0910/L16/semhl-15-ann.pdf The only occurrence of 'distinguish' is in the Leibniz citation. Please see adequacy on slide 17. An expression relation between two boolean expressions M1 and M2 is adequate if for all program runs (for all initial states of the program s), M1 evaluates to true just in case M2 does. If in some circumstances M1 evaluates to true but M2 (with the same initial state) evaluates to false, the expressions are not related or the expression relation is inadequate. In my mind, 'evaluates-to' is an existential statement. The adequacy notion given there is inadequate if the program execution is indeterministic, as I would have expected it to be in this case. (They quickly note this on slide 18, giving concurrency features as an example.) See also the classic http://www.ccs.neu.edu/racket/pubs/scp91-felleisen.ps.gz (p11 for definition and Theorem 3.8 for an example of a distinguishing, or witnessing context). Thanks for the pointer, I will have a look. However, it seems that the semantics the definition and the proof rely on are deterministic? In essence, lazy IO provides unsafe constructs that are not named accordingly. (But IO is problematic in any case, partly because it depends on an ideal program being run on a real machine which is based on a less general model of computation.) I'd agree with the first sentence. As for the second sentence, all real programs are real programs executing on real machines. We may equationally prove (at time Integer) that 1 + 2^10 == 2^10 + 1 but we may have trouble verifying it in Haskell (or any other language). That does not mean equational reasoning is useless: we just have to precisely specify the abstraction boundaries. Which is really hard. I think equational reasoning is helpful because it is valid for ideal programs and it seems therefore to be a good heuristic for real ones. BTW, the equality above is still useful even in Haskell: it says that if the program managed to compute 1 + 2^10 and it also managed to compute 2^10 + 1, the results must be the same. (Of course in the above example, the program will probably crash in both cases). What is not adequate is when equational theory predicts one finite result, and the program gives another finite result -- even if the conditions of abstractions are satisfied (e.g., there is no IO, the expression in question has a pure type, etc). The abstraction bound is where exact reasoning necessarily stops. I think this context cannot be used to reliably distinguish x == y and y == x. Rather, the outcomes would be arbitrary/implementation defined/undefined in both cases. My example uses the ST monad for a reason: there is a formal semantics of ST (denotational in Launchbury and Peyton-Jones and operational in Moggi and Sabry). Please look up ``State in Haskell'' by Launchbury and Peyton-Jones. The semantics is explained in Sec 6. InterleaveST is first referred to in chapter 10. As far as I can tell, the construct does not have specified a formal semantics. Please see Sec 10.2 Unique supply trees -- you might see some familiar code. Although my example was derived independently, it has the same kernel of badness as the example in Launchbury and Peyton-Jones. The authors point out a subtlety in the code, admitting that they fell into the trap themselves. They informally note that the final result depends on the order of evaluation and is therefore not always uniquely determined. (because the order of evaluation is only loosely specified.) So, unsafeInterleaveST is really bad -- and the people who introduced it know that, all too well. I certainly do not disagree that it is bad. However, I am still not convinced that the example actually shows a violation of equational reasoning. The valid outputs, according to the informal specification in chapter 10, are the same for both expressions. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Building the Haskell Platform in Linux
Hi cafe! Probably you all know how to do this, but I myself found confused when building the Haskell Platform in Linux for my first time. I was using Linux for my first time too! The first problem I encountered was to decide what linux packages install to make the ./configure successful in both GHC binary distribution and the Haskell Platform. So I collected the names of the minimum set of packages that you need to have installed before starting with GHC and the Platform in a small blog post: http://deltadiaz.blogspot.com/2013/04/haskell-platform-from-source-in-linux.html If I would have to start all over again, forgetting what I have learned so far, I would fine this list very useful! This thought is what brought me here to make it public. Who knows, maybe I am saving somebody of some google searches and trials and errors. With my best intentions, Daniel Díaz. -- E-mail sent by Daniel Díaz Casanueva let f x = x in x ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: psqueue-benchmarks - benchmarks of priority queue implementations
Hi, See here: https://github.com/nh2/psqueue-benchmarks/blob/db89731c5b4bdd2ff2ef81022a65f894036d8453/QueueBenchmark.hs#L44 If I fromList 100 entries into the queue, it stack space overflows. Are you sure that this is a bug of GHC PSQ? I think that replicateM _GHC_CRASH_N causes Stack space overflow. If you compile it with -rtsopts and run it +RTS -K100M, I guess you don't see the problem. --Kazu ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
