tag:blogger.com,1999:blog-1777990983847811806.post572071035785262951..comments2014-04-19T12:35:02.893-07:00Comments on Haskell for all: Purify code using free monadsGabriel Gonzaleznoreply@blogger.comBlogger6125tag:blogger.com,1999:blog-1777990983847811806.post-55107600362257455292014-01-18T00:44:58.238-08:002014-01-18T00:44:58.238-08:00To answer your first question, the free monad is n...To answer your first question, the free monad is not the only way to add a useful semantics to `IO`. The approach you describe (moving some shared logic up into the free monad and making it non-free) is better.<br /><br />The main reason I use the free monad as the running example is because it is the most extreme and most instructive example: if you understand how the free monad trick works then you typically also understand how the non-free derivatives work as well.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-78930476028366677612014-01-13T12:44:08.115-08:002014-01-13T12:44:08.115-08:00Is the "free monad" the key to adding pu...Is the "free monad" the key to adding purity/semantics to IO?<br /><br />It seems like what you are doing is splitting IO into to two monads: a pure monad and an impure monad. This lets us swap out the impure "implementation" monad with alternate backends, while still maintaining some semantic guarantees.<br /><br />The "free monad" is the *least* you can do, so it's a good starting point.<br /><br />But it would be even nicer to use a non-free monad, one that lets the type-system encode *even more* semantics about the expected behaviors of the IO functions.<br /><br />When you say that we can reason about `runPure` to show that `runPure echo === take `, that shows you that the impure `run echo` *might* be ismorphic/adjoint/equivalent to `take 1`, but there's no guarantee, because the list-management code is inside `runPure`, not in the common (free) monad.<br /><br />Basically, the free monad and `runPure` provides a test case that `run` "isn't definitely wrong"<br /><br />Now (and here's where I start hand-waving frantically), if you boost the list-management code from `runPure` up to the pure monad (no longer a free monad), but carrying some additional semantics that says that `putStrLn` consumes content from `getLine` (and any intermediate pure transformations), then you have IO "laws". You still can't statically *guarantee* that impure IO follows those laws (same is with the monad laws in general), but you can encode them, and you can write specific test cases to (quick)check those laws on sample data/programs.<br /><br />(Disclosure: I don't really know what I am talking about. I'm not sure that using a more interesting pure monad actually carries tangible improvements)Michael Rogerhttp://www.blogger.com/profile/08729150476888743293noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-89770722051784466792012-07-19T10:47:01.720-07:002012-07-19T10:47:01.720-07:00I completely agree. Usually you know you implemen...I completely agree. Usually you know you implemented something correctly when it has all sorts of nice succinct equational properties.<br /><br />Also, like you said, you can use all the equational properties as rewrite rules so that GHC can optimize your program automatically, as I hinted at in the post.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-81028054166017864712012-07-19T10:40:42.229-07:002012-07-19T10:40:42.229-07:00We can do program derivation also! It's not ea...We can do program derivation also! It's not easy but works nice. In this fashion one can make a program more efficient while it's sure that is correct.<br /><br />And there is another good point to equational reasioning. People often think that demonstrations only serve to confirm correctness, but they also serve to deduce answers too. And this is a very good point to have in programming, choosing an answer because it's guided by some properties instead of trying to guess it thinking in a human manner the way that the program should behave.Sawadyhttp://www.blogger.com/profile/15647975101406450223noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-5862906606653692482012-07-19T10:37:41.592-07:002012-07-19T10:37:41.592-07:00This comment has been removed by the author.Sawadyhttp://www.blogger.com/profile/15647975101406450223noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-73092791147552053022012-07-19T10:29:57.270-07:002012-07-19T10:29:57.270-07:00Thanks for the walk through of how to prove someth...Thanks for the walk through of how to prove something with equational reasoning. The term is thrown around a lot, but there are few examples of the actual steps. <br /><br />I have been thinking that it might be good to have a wiki for showing the proofs of instances for common type classes (Monad, Applicative, etc). This would be a good resource to show users how to prove their own instances.Unknownhttp://www.blogger.com/profile/15527851328314513476noreply@blogger.com