Generic programming in F# - another take

Playing a bit more with generics, I stumbled upon some fairly compact combinators that can derive n-ary conjunctions from a binary conjunction. Here is a self-explanatory F# example (disregard the ugliness involved in F#'s lack of higher kinds, Haskell or OCaml code would not need this):



In case you are wondering about the Coq file in the gist: a good objection to this approach is efficiency. Instances computed in this way are not efficient at all. Just think of all the allocated tuples! It turns out, we can remedy the situation with automated program transformation. In F# it would involve computing over quotations or similar quoted forms. It is hard to get started since little support for optimizing those is available out of the box. In Coq there is more batteries. As you can see in the gist, Coq seems to tackle the above example trivially with the "compute" tactic, and derive an instance equivalent to a hand-written one.

Introducing FAKE boot workflow

FAKE is a tool to automate your builds with F# scripts. Use the newly available FAKE boot workflow to get started quickly, automatically reference packages, and plug in your own build logic from NuGet.

FAKE with NuGet support

UPDATE: the proposal made it into pre-release FAKE, see the more recent article: http://t0yv0.blogspot.com/2013/04/introducing-fake-boot-workflow.html

Intended F# build workflow: start from an empty folder, write build.fsx, and run fake - and get anything building with software from NuGet.

Draft Implementation  Discussion

Generalizing records combinators a bit

Towards generic programming in F#: thoughts on generalizing the earlier combinators over records and unions...

WebSharper, PhoneGap, and Ripple: easier native HTML5 apps

We are experimenting with PhoneGap, PhoneGap Build, Ripple emulator and WebSharper. If successful, this will let you write truly cross-platform native mobile apps in F#, quickly pre-testing them in Chrome, and then generating various installers (Android, Windows, iOS - yes, iOS!) without even having to install the SDK.

TypeScript: initial impressions

There are several things under the TypeScript umbrella: a type system, language spec, JavaScript-targeting compiler and tooling that provides interactive code completion. I have tried TypeScript on a few small projects, the latest one being TypedPhoneGap. I also worked extensively with the language spec, wrote a parser and analyzer for the `.d.ts` contract specification fragment, pondered the semantics, and engaged in little flamewars on the language forum. My conclusion, in short, is this: the type system and language design are terrible, the compiler is OK, and tooling is excellent. Overall, it is an improvement over writing bare JavaScript, and the definition fragment is helpful (though not ideal) for communicating JavaScript API formally.

Using Coq as a program optimization tool

Update: - a slightly more compelling example of where program computation shines is at Another take on F# generics.

I tend to complain a lot about the programming tools I work with. In one sentence, the world of software is just not a sane place. If left unchecked, this complaining attitude can grow into despair - so I enjoy a little escape from time to time. I need to dream of a better world, where programming is meaningful, fun, beautiful, efficient, mostly automated, and where programs are verified. This is why my escape activity is playing with Coq.

One fascinating trick that Coq does really well is computing and manipulating programs. Have you ever found yourself writing beautiful, general functional code and then wondering how to make it run faster? Spending lots of time inlining definitions, special-casing, performing simplifications and hoping you do not introduce bugs in the process?

This activity can be automated in a way that verifies meaning preservation.

Here is a rather silly example (I will try to think of a better and more convincing one):



Lines 20-24 should in theory be expressible as a single-word tactic. This is where program simplification happens.

Imagine a better world.. You write functional code, focus on clarity of specification, then drop into interactive theorem proving to compute (!) the equivalent huge, ugly, optimized, specialized program that runs a lot faster but is guaranteed to produce the same result.

EDIT: a reader has asked how manipulating programs in Coq is different from using an optimizing compiler such as GHC. The short answer (and I again realize just how lame my example is since it does not demonstrate it) is control.

With GHC, you get a black-box optimizer that does some transformations and gives you a result. The resulting program is usually better (faster, uses less space), but once in a while worse. It also may or may not do the essential optimization for your domain. I am not using GHC on a daily basis - so feel free to correct me, but I believe the amount of control you exert is fairly limited, even with REWRITE pragmas. In Coq, on the other hand, you get "proof mode" - an interactive environment where you can inspect and explore the intermediate versions of your program as it is being optimized, and guide the process. There is a spectrum of possibilities from fully manual to fully automated transformations, programmable in the Ltac tactic language.

Another advantage (which makes this attractive to me) is that if you are targeting ML (OCaml, F#), you are working with a compiler that refuses to do too much optimization. So GHC-like magic is simply not available. Here extracting from Coq may come handy.

Yet another advantage is that you are working in a more expressive logic. This opens the door to writing more general programs than your target compiler would admit. I have not yet explored this too much, but it seems to be an easy way to bypass the lack of, say, higher kind polymorphism in F#.

Finally, I should also mention that as a proof assistant, Coq makes it practical to construct proofs that your programs (and transformations) are correct with respect to a given semantics. I find this appealing, even though this is a bit beside the point. As a beginner my experience has been that proving any non-trivial lemma takes unbelievably more time than constructing a program, so for now I am just exploring the possibility of using Coq as a programming language without doing much proof development.