Quiet Nights and Quiet Stars

Quiet chords on my guitar … and quiet from Rick for the past few months.

Quiet on the Phaneron means there will be much to say. As advertised, the first six months of 2011 have been about thinking small. Yes, I’ve been in the woodshed again and truly enjoy the solitude. Much like an earlier period in my life when internalizing fingerings, modes and inversions required the quiet to allow careful concentration, so have these past six months allowed for examining nightly releases of the Glasgow Haskell Compiler, its Regular Shape Polymorphic Parallel Array (REPA) library and dependent types in a AGDA.

After having taken a pretty close look at topics in software development and information technology architecture over the past few decades I’m very excited to get under the hood with GHC and its back-ends. I hope to share some experiences by year end on optimizing GHC back-end selection and configuration management on my 4-core i7 using genetic algorithms as described by Don Stewart in Evolving Faster Haskell Programs (now with LLVM). I also hope to get access to some cooler hardware, possibly through some academic connections.

Closely examining REPA seems a good fit for my development in Haskell. Converting Paul Tarau’s list-based implementation of this bijective mapping between Godel numberings and Term Algebras in REPA is a valuable exercise in both learning this library and the tacit knowledge I need to become a journeyman on GHC. The next stage of this exercise will include verification with Quickcheck. I’ve also taken the opportunity to do a retrospective on REPA by examining some of the early work on parallel list notation [:e:] and state transformer monads.  There’s no shortage of great papers out there on Haskell. See my del.icio.us bookmarks. This retrospective will provide the right foundation for later investigation in Data Parallel Haskell. Seems there’s time before the next release.

It looks like I’ll drop my plans to build expertise in Isabelle/HOL in favor of Agda. I just don’t have the bandwidth to internalize that much. Agda allows me to leverage my Haskell investment.

If you read A Winter of Philosophy and Logic, you’ll also be interested to know Valdimir Voevodsky recently announced a special program to develop the Univalent Foundations of Mathematics along with Steve Awodey and Thierry Coquand. Voevodsky has taken an interest in Martin-Lof type theory. He’s demoed some proofs in Coq, but he’s also active on the Agda listserv. And Coquand & Co seem to be pro-Agda. Voevodsky’s stature in math circles could do a lot for this subject. I’ll be tracking this all pretty closely.