tag:blogger.com,1999:blog-1777990983847811806.post572071035785262951..comments2017-12-06T14:41:09.139-08:00Comments on Haskell for all: Purify code using free monadsGabriel Gonzaleznoreply@blogger.comBlogger13125tag:blogger.com,1999:blog-1777990983847811806.post-11768621242450866732016-08-21T12:00:12.043-07:002016-08-21T12:00:12.043-07:00I think Coq is what a lot of people reach for when...I think Coq is what a lot of people reach for when they want automatic theorem proving although I'm not an expert on it myselfGabriel Gonzalezhttps://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-41354520027061907952016-07-15T08:08:48.267-07:002016-07-15T08:08:48.267-07:00Instead of quickcheck, is there some automated-rea...Instead of quickcheck, is there some automated-reasoning tool that would attempt to actually find the proof of the equational property automatically? I suppose it wouldn't work in the general case, but proving simple examples as the one presented here should be possible somehow, I think. Are there some theorethical issues or is it too difficult to implement or has simply nobody done it yet?jachymhttps://www.blogger.com/profile/12487644433402463364noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-69231351032136561282015-12-06T21:09:50.549-08:002015-12-06T21:09:50.549-08:00Perfect. Thanks for pointing me in the right direc...Perfect. Thanks for pointing me in the right direction. Zanghttps://www.blogger.com/profile/10166319578442197145noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-40447525521430560292015-12-06T19:54:24.112-08:002015-12-06T19:54:24.112-08:00I think it's probably easier to do this using ...I think it's probably easier to do this using the `operational` package's encoding of free monads:<br /><br />https://hackage.haskell.org/package/operationalGabriel Gonzalezhttps://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-34413524762714410592015-12-06T17:11:15.371-08:002015-12-06T17:11:15.371-08:00Excellent post - great examples. Thanks a lot!
A ...Excellent post - great examples. Thanks a lot!<br /><br />A quick question for you: How you would represent a function of the type `IO a -> IO (Double, a)` (say, System.TimeIt.timeItT) as a constructor of your TeletypeF type?<br /><br />Thanks again for the excellent post!Unknownhttps://www.blogger.com/profile/09640737754874754373noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-21112815045520546182014-04-23T16:49:05.254-07:002014-04-23T16:49:05.254-07:00Yes, the `free` library recently added a Template ...Yes, the `free` library recently added a Template Haskell function to autogenerate all of these wrapped functions:<br /><br />http://hackage.haskell.org/package/free-4.7.1/docs/Control-Monad-Free-TH.htmlGabriel Gonzalezhttps://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-78585979943467423172014-04-23T01:47:48.531-07:002014-04-23T01:47:48.531-07:00Thanks for your article!
However, I wonder how you...Thanks for your article!<br />However, I wonder how you would do this practically for a program which requires maybe tens or hundreds of IO operations. Wrapping all those functions into a free monad would be quite a burden.<br />Is there a good approach to this?jrkhttps://www.blogger.com/profile/17998161877646447052noreply@blogger.comtag: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 Gonzalezhttps://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 Rogerhttps://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 Gonzalezhttps://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.Sawadyhttps://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.Sawadyhttps://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.Unknownhttps://www.blogger.com/profile/15527851328314513476noreply@blogger.com