Rash thoughts about .NET, C#, F# and Dynamics NAV.

As programmers we often want to express that a special property holds for a method, e.g. we want to say that the associativity law holds for list concatenation. In F# we could define a concat method like this:

As programmers we could write a couple of unit tests which try to check the associativity law. With NUnit enabled we could write this:

But the question is: did we cover all interesting cases? In computer science we have a method to prove that the property holds for all lists. This methods is called structural induction (see also this video lecture by Martin Odersky) and would look like this:

1) Rewrite the code as equations

concat ([],ys)    = ys                  [CON1]
concat (x::xs,ys) = x :: concat(xs,ys)  [CON2]

2) Rewrite the property as an equation

concat(concat(xs,ys),zs) = concat(xs,concat(ys,zs))

3) Check the base case

concat(concat([],ys),zs) 
= concat ([],zs)                 // using CON1
= []                             // using CON1

concat([],concat(ys,zs))

= concat (ys,zs)                 // using CON1
= []                             // using CON1

3) Show the inductive step

concat(concat(x::xs,ys),zs) 

= concat (x::concat(xs,ys),zs))  // using CON2
= x :: concat(concat(xs,ys),zs)  // using CON2 
= x :: concat(xs,concat(ys,zs))  // induction hypothesis
= concat(x::xs,concat(ys,zs))    // using CON2

This math is very clean and shows that the associativity law holds for all lists. Unfortunately even with a slightly more complicated sample this gets at least tricky. Try to prove that reverse(reverse(xs)) = xs with reversed defined as:

As you will see the naïve approach with structural induction will fail (for a nice solution see this video lecture).

There is even a bigger problem with the proof: one assumption of induction is referential transparency of the given functions. We can’t always assume this.

So we can’t always (easily) proof code properties and we don’t want to write too many unit tests – then what can we do?

One compromise solution is to use a tool which systematically generates instances for our tests. There are a couple of tools out there, e.g. there is QuickCheck for Haskell or PEX for .NET. In F# we can use a tool called FsCheck:

Of course a test like this doesn’t prove that the property holds for all lists, but at least it verifies all bases cases and probably a lot more cases than one would manually do.

If you introduce a bug you get a nice report, which even shows a counterexample:

It’s even possible to add these tests to your test suite and to run them during the CI build. So don’t stop at classical unit test – check code properties!

“Footloose is a fast and scalable asynchronous distributed computing and service library that was designed to be secure, simple to use, unobtrusive and without the need of client side code generation or proxy classes.

It was developed to connect or build distributed applications on the .NET/Mono platform with enterprise features like load-balancing, clustering, encryption, service discovery and single-sign on.

Footloose enables you to easily transmit any kind of data between the components of your application over thread-, process- or physical boundaries. Depending on your needs Footloose uses one if its transport channels, e.g. a Named Pipe or a Unix Socket for Inter Process Communication (IPC), AMQP with one of the available Message Broker implementations (like RabbitMQ) in the local network or even XMPP as a secure and fast realtime messaging protocol that enables you to build cloud services.”

http://www.footloose-project.de

If you don’t like WCF then you should really check out Footloose.
Today I want to show you how to use Footloose in a very simple sample with F#.

As a first step we create a F# project for the service contracts. Inside this project we need a service definition like this:

This is just a definition of the remote service and the data. Now we create a F# console project for such a service and reference the service contracts project. We start by implementing the service like this:

Now we use nuget to retrieve the latest version of Footloose. At the time of writing we need to install the pre-release of version 3.0 by "install-package Footloose -pre". In the Program.fs we add the service configuration. Here Footloose wants us to specify the endpoint name, transport channel and a serializer. In order to get Footloose working we also have to retrieve a trial license from the website.

Footloose wants us to provide a ServiceLocator in order to resolve the service. Normally you would use a DI container for this, but here it’s sufficient to fake a IServiceLocator like this:

In the next step we create another F# console project for the client, reference the service contracts and install Footloose ("install-package Footloose -pre"). We also need to install FSharpx ("install-package FSharpx.Core") in order to use the "Quotation to Linq Expression" stuff and the new task monad. Now we are ready to build the client:

As you can see we set up the connection and wrap our service call inside a task monad. The most interesting part is calling the service. Footloose wants to us to provide a LINQ expression:

In order to make the client code compile we also need an active pattern which transforms the service result into something we can pattern match:

As the last step we configure the solution to start both projects and run the sample:

The result should look like this:

The sample code is now part of the FootlooseExamples project on github.