This is kind of an open-ended question.
I'm trying to figure out if this proof of Löb's theorem can be translated into Haskell step by step. The idea was inspired by sigfpe's post. Unfortunately he used the Functor type class, whose law (a→b)→(□a→□b) isn't valid in modal logic. I'm trying to fix that drawback and use the correct law □(a→b)→(□a→□b) instead.
Here's a tentative type signature for what I want:class Prov p f where mp :: p (a -> b) -> p a -> p b dup :: p a -> p (p a) fix :: p (f a -> a (f a)) unfix :: p (a (f a) -> f a) loeb :: Prov p f => p (p a -> a) -> p a loeb = ???
The idea is to use p as the provability predicate, and f as the fixpoint operator. Note that there's no method with type a -> p a, because not all true sentences are provable. If we had such a method, the problem would be much easier.
Trying to implement that, I ran into a few difficulties:
1) Haskell doesn't have type-level lambdas, so fix and unfix can only be used with newtypes. That requires adding more methods to Prov, for packing and unpacking every single newtype. I wish there was a better way.
2) The methods of Prov don't seem to be enough. It looks like I need versions of dup and mp that work inside p as well. Is there a workaround?
3) Using f seems like a hacky approximation to the diagonal lemma. Can we do better?
I guess I'm just confused overall. Is it even feasible to use such a direct encoding for modal logics, like provability logic? Or should I go lower level and define explicit types for sentences, proofs, etc.?submitted by want_to_want
The original message contains some interesting tidbits. I am not sure how the discussion on emacs-devel will develop. But speculating about things such as Guile elisp is, of course, our bailiwick.
Are hackage packages signed? Does cabal download packages via http or https?submitted by MintyGrindy
[link] [6 comments]
LPNMR 2015 - Preliminary Call for Papers - 13th International Conference on Logic Programming and Non-monotonic Reasoning
We are happy to announce a stable persistent 2 release candidate.
We previously announced an unstable release of persistent 2. It was a good idea to call it unstable because some commenters pointed out that we were not exposing the full power of the new flexible Key type. This lead to a couple of breaking releases that organizied the internal types of persistent. All of these are on the unstable 2.0.x series.
persistent-2.0.3.* is on hackage now. We consider this a release candidate that will be promoted to persistent-2.1. We may wait until the haddocks build on hackage before releasing.Ongoing persistent maintainership
Persistent is of huge importance to the Hasekll community, playing the role of default ORM. The project has benefited immensely from the community involvement. We get a lot of prompt bug reports that often include fixes. And there have been many great new features added by contributors.
However, persistent it is lacking in dedicated maintainers for each backend. We would like for Michael to keep doing a great job stewarding the project, but for others to step up and help own a SQL backend.
An extreme example of a lack of backend maitenance is when we received a pull request for a CouchDB backend. It was great to share the code as a starting point, but it was already using an older version of persistent and is now sitting in the experimental folder in a bit-rotted state.
In general a persistent backend can only be first class and in our tree with a dedicated maintainer. Michael and I maintain persistent and persistent-template. I maintain the persitent-mongoDB backend. The issue now is more with the SQL backends, where the maitenance and development for them is being pushed on Michael. For example, I implemented custom Key types in persistent, persistent-template, and persistent-mongoDB. Michael and myself implemented them for persistent-sqlite, but it still needs to be implement for persistent-postgressql and persistent-mysql.
Maintaining persitent and persitent-template has had a questionable cost/benefit ratio for me. But I have personally found that maintaing the persistent-mongoDB backend has paid off well for me. I need to have a good understanding of what is happening with my code that deals with the database. Rather than treating it as a black box I make continous incremental improvements to the library that I rely on, and I can smoothly get code onto hackage rather than having local modifications.
Let us know if you are interested in helping to maintain a backend.
Summary: I've just released a new version of Shake, with a --demo feature and an underlying continuation monad. I want to release v1.0 in the near future.
I've just released a new version of the Shake build system, version 0.13.3. While the version number is only 0.0.1 higher, the changelog lists a large number of improvements. In particular, two changes are:
- The Action monad is now based on continuations, which allows Shake to suspend threads without requiring a GHC RTS thread. The result is significantly less memory used on thread stacks. I still find it quite amazing that Haskell has such powerful and robust abstraction mechanisms that a huge change doesn't even break the API.
- The shake binary now features a --demo mode, invoked by running shake --demo. This mode generates a Shake project, compiles it, and shows off some of the features of Shake. You can the output of --demo here.
With the two features above, I'm now looking towards Shake version 1.0. I'm not looking to make any significant backwards-incompatible change, or necessarily any code/API changes at all. However, if you have anything you think should be addressed before reaching such a milestone, please comment on the issue tracker or email the mailing list.
The one thing I still want to finish before releasing version 1.0 is to have a proper website for Shake. I've registered shakebuild.com which will host the content, and have set up GitHub pages to serve it up. I have some rough content in the docs directory and a prototype generator in the website directory - as an example it currently generates something a bit like this for the user manual, but with a table of contents when run through the latest generator. I'd appreciate any help with the content, the generator, or the styling - just email the mailing list.
Did you know that all ACM-sponsored conferences have an anti-harassment policy? I didn’t, until I chaired the Haskell Symposium last year. The concise policy says, among other things, that people shouldn’t use my family constitution to interfere with my professional participation. And the policy has teeth. That’s great.
My not knowing the policy and not seeing it publicized didn’t make me go out of my way to harass anyone. But it did make me less sure and less comfortable that I belonged at ICFP. Briefly, it’s because I didn’t know if it would be common ground at the conference that my actual self was fully human. That’s not something I can take for granted in general society. Also, it’s because I didn’t know whether my fellow conference attendees were aware of the policy. We could all use a reminder, and a public signal that we mean it.
For these reasons, I’m very happy that ICFP will start to publicize ACM’s existing anti-harassment policy and make sure everyone registered knows it. All ACM conferences should do it. That’s why Tim Chevalier, Clement Delafargue, Adam Foltzer, Eric Merritt, and I are doing two things. We ask you to join us:
- Donate to the Ada Initiative. Our goal is for the functional programming community to raise $4096 by the end of Friday (Sept 19) UTC. To count toward this goal, please use this link: http://supportada.org/?campaign=lambda
- Call on the ACM and tell your friends. For example, I tweeted
I donate to @AdaInitiative because I want @TheOfficialACM events to announce their anti-harassment policy http://supportada.org/?campaign=lambda #lambda4ada
Thanks for improving our professional homes!