# Getting started with using SublimeHaskell and Cabal

I recently started using Sublime Text 2 as my main editor for non .net related languages – and I really enjoy it (I think I will pay Mr. Skinner soon – well deserved!).

If you are working with Haskell, then there is a rather good plugin named SublimeHaskell you can use to get automatic compile-error reporting (on save) and an integrated type query and type insert mechanism I quite like.

But in order to get this you have to set up your Haskell project with cabal and install the plugin first.

The installation itself is very simple once you installed the “Package Control” for Sublime Text 2 (see the link – it’s basically nothing more than running the following snippet inside the Sublime Text 2 console).

import urllib2,os;
pf='Package Control.sublime-package';
ipp=sublime.installed_packages_path();
os.makedirs(ipp) if not os.path.exists(ipp) else None;
urllib2.install_opener(urllib2.build_opener(urllib2.ProxyHandler()));
print 'Please restart Sublime Text to finish installation'



With the Package Control ready you just have to use the package-install, search for SublimeHaskell and hit return – done.

# Setup a basic Haskell Cabal project

Create a folder for your project and create your Haskell source file(s) – here I’m using a very basic one:

-- Greetings.hs
-- Copyright (c) 2012 Carsten König
--

module Greetings where
import System.Environment

main :: IO ()
main = getArgs >>= print . greetings . head

greetings s = "Hello! " ++ s



Next create a .cabal file for your project – this is where you tell Cabal how to build/install your files and what dependencies it has, etc.(see the Cabal user guide for additional information):

Name:                greetings
Version:             0.0
Description:         say Hi
Author:              Carsten König
Maintainer:          Carsten@gettingsharper.de
Build-Type:          Simple
Cabal-Version:       >=1.2

Executable greetings
Main-is:           greetings.hs
Build-Depends:     base >= 3 && < 5



Important are the name (which names your package), Executable <name> (the –o(utput) name) and Main-is entry.

Finally you will need a (very basic) Setup.hs script for cabal:

import Distribution.Simple
main = defaultMain



That’s it – now you can install/build your project with Cabal like this:

cabal install --prefix=$HOME--user  Please note:$HOME is where cabal should write your binary output to – it will create/use a “bin”-folder right below \$HOME.

That’s it – now whenever you save your file in SublimeText it ghc will run it and possible errors will show like this:

And even better: if you mapped your keybindings in the “Preferences/Key Bindings – User” settings of Sublime Text like this:

    {
"keys": ["ctrl+k", "ctrl+h", "ctrl+t"]
},
{
"keys": ["ctrl+k", "ctrl+h", "ctrl+i"]
}



You can put the cursor on a method, use the sequence <Ctrl>-<K>, <Ctrl>-<H>, <Ctrl>-<T> to see the type of the expression:

Or hit <Ctrl>-<K>, <Ctrl>-<H>, <Ctrl>-<I> to add the type above your method:

Neat isn’t it (aside from not noticing String = [Char])

# enjoying Racket

I’m lately trying to get (back) into Lisp/Scheme/Clojure-Space.

While trying to get a reasonable Windows-environment for Clojure set-up (a pain… a PAIN – suggestions welcome) a stumpled upon Racket and I have to say I really like this (at least for some toying around with the languague).

Here is a sample using the nice DrRacket GUI:

# Lambda Calculus: What about “if”

In the last article we talked about subtraction. But of course there is more to “programming” than just arithmetic. One of the most basic things we need is a way to decide an output based on some value. You all know this as “if” and we will talk in this part about representing Booleans and implementing a “if” function like this:

$$If(condition, then, else) = \begin{cases} then & \text{if } condition=true \\ else & \text{else} \end{cases}$$

## Representing Booleans

Just like with the natural numbers we introduced in the first article we are going to represent $$T$$ (short for true) and $$F$$ (short for false) in the form of abstractions – to be more precise: we will just reuse the tuple-selectors from the previous article:

$$T := \lambda xy.x$$ $$F := \lambda xy.y$$

## And, Or, Not

The next step is to get the usual logical operators into our calculus. Let’s start with $$And$$. It should operate on two Booleans $$a$$ and $$b$$ and return another Boolean, that is an abstraction with two parameters. Now if both arguments are $$T$$ the resulting function has to return the first argument you can pass to it, if not the second. Of course $$a$$ will behave similar: if it is true it will return the first argument given, if it is false the second. As we have to chain two true’s you can see that the following abstraction does the trick (you might observe that this uses “currying”).

$$And := \lambda ab.abF$$

Here is a sample session from my interpreter to verify that this is indeed a AND:

LAMBDA CALCULUS INTERPRETER
===========================
>>> T := \xy.x
\xy.x
== [T]
>>> F := \xy.y
\xy.y
== [F]
>>> And := \ab.abF
\ab.(ab\xy.y)
== [And]
>>> And T T
\xy.x
== [T]
>>> And T F
\xy.y
== [F]
>>> And F T
\xy.y
== [F]
>>> And F F
\xy.y
== [F]



Of course you can also work this out with a pencil and the lambda-calculus rules.

OR is similar: if the first argument is true than we can return true, if not the answer is just the second argument (remember: $$true || b = true$$ and $$false || b = b ). This translates directly into  Or := \lambda ab.a T b  >>> Or := \ab.a T b \ab.(a\xy.xb) == [Or] >>> Or T T \xy.x == [T] >>> Or T F \xy.x == [T] >>> Or F T \xy.x == [T] >>> Or F F \xy.y == [F]  Having seen all this NOT should not be a problem for you (right? – you might want to try it before reading on – I will give you the answer at the end ) ## Finally: IF After all of this IF is just a piece of cake – remember: if the condition is true we want to return the first argument that follows (the \(then$$-branch); and if the condition is false we want to return the second argument (the $$else$$-branch).

You should know by now that this is just the behavior that $$True$$ and $$False$$ already have! So the “condition” already does the work and our IF is just the identity-function – neat isn’t it?

In case you don’t believe:

>>> If := \x.x
\x.x
== [If]
>>> If T a b
a
>>> If F a b
b



So here is the NOT – in case you did not find yourself (there are many right definitions) – the easiest one is just to use the same trick as with the IF – use the argument to invert:

$$Not := \lambda a.a F T$$

>>> Not := \a.a F T
\a.(a\xy.y\xy.x)
== [Not]
>>> Not T
\xy.y
== [F]
>>> Not F
\xy.x
== [T]



## Conclusion

So this is it – the first control-structure you need for a general-purpose programming language – and it was rather easy.

BTW: we have already seen how to do a kind of FOR loops – you can just use the natural number representation for that.

It’s much harder to get something similar to a WHILE loop, or – as we are in functional land, a recursive function. And in the next article we will see how to implement this using one of the infamous fixpoint operators – so stay tuned

# Lambda Calculus: Subtraction is hard

In the last article I defined the Succ operation on numbers and showed how this can be used to implement addition in untyped lambda calculus.

Because of the number representation I choose this was rather easy so Subtraction should be not that hard right?

Well … wrong.

You might want to stop here and try to define a Pred operation yourself that takes a number and returns the predecessor (-1) of that number or zero if there is none (because 0 is not the successor of any natural number there should be no predecessor to 0, ever other number has one).

Let’s have a look at our numbers again and try to find out what the problem is: We represented a natural number $$n$$ by $$\lambda fx.f^{n}x == \lambda fx.f(f(..f(x )..))$$ and so to get the predecessor of $$n$$ we must “remove” one of the $$f$$ if there are any.

## Why is this hard?

Have a look at our reduction-rule – it will only replace some variables by something different and there is no way to substitute it with an empty term (as there are no empty terms in lambda calculus).

So you might be tempted to think that this is not possible, It is said that Church himself believed for some time that this is not possible but his student Kleene came to the solution while visiting his dentist – that’s why the trick is called “wisdom tooth trick”.

## The Trick

So what is the “trick”?

If you know it it’s indeed rather easy: You cannot remove a $$f$$ so you don’t. Instead you start by zero and count up to the number you want the predecessor of BUT by doing this you remember the last number you saw just before. Having reached the desired number you return the memorized last number … doh you might think – that is exactly how I find the predecessor of an character in the alphabet. Well ok – that is my way for most characters and that is because I – like every other person – do remember the ABC…Z series very well but seem not to have the mental capacity to remember the reversed series as well, so to find the predecessor of Q (I remember in triples so T would be to easy) I count up to Q: ABC…MNOPQ and having this still in cache I present you with P”

### The More technical points

So first we have to find some way to remember a value and treat a state through our terms. This is where intuition from functional programming comes in handy.

Instead of globally remembering some values we use a tuple as the object we want to manipulate. The first item of this tuple shall be the last number and the second one the current number: $$(lastNumber, currentNumber)$$ and a step in our algorithm is just $$(lN, cN) \Rightarrow (cN, Succ cN)$$.

Of course now we have to find a way to create pairs and from a pair get the first and second item.

## Making and using Pairs

Just as with the numbers a nice way to do this is using passed functions in a clever way. To create a pair we will use this lambda-calculus term: $$MkPair := \lambda ab. \lambda s.(s a b)$$. Where $$a$$ is the first item in the pair and $$b$$ is the second item. Of $$s$$ you should think as a “selector” function.

Now defining a selector-function for “first” and “second” is a piece of cake: $$Fst := \lambda ab.a$$ and $$Snd := \lambda ab.b$$.

To test this let’s say we have a pair $$P := MkPair\ a b == \lambda s.(s a b)$$ then using the second-selector we have $$P\ Snd == \left( \lambda s.(s a b) \right) Snd == Snd\ a b$$ $$== \left( \lambda xy.y \right) a b == \left( \lambda y.y \right) b == b$$

## The transition function

Now we go on and define a term that can transform our $$(lastNumber, currentNumber)$$ pairs: given such a pair we have to create a new one, that has the old second item as first item and puts the incremented second item in second place. Using the functions we got so far this is not difficult: $$Trans := \lambda p.MkPair\ (p\ Snd) \ (Succ(p\ Snd))$$

## Putting it all together

So now if we only use this function $$n$$-times on $$(Zero, Zero)$$ we can use the first item of the result to define the Pred operation. Luckily our number representation is more or less just a for loop so the final operation is $$Pred := \lambda n.\left( n\ Trans\ (MkPair \ N0\ N0)\right) Fst$$

## Testing this with the console interpreter

LAMBDA CALCULUS INTERPRETER
===========================
\fx.x
== [N0]

\nfx.(f(nfx))
== [Succ]

\fx.(fx)
== [N1]

\fx.(f^{2} x)
== [N2]

\fx.(f^{3} x)
== [N3]

\fx.(f^{4} x)
== [N4]

\fx.(f^{5} x)
== [N5]

\fx.(f^{6} x)
== [N6]

\fx.(f^{7} x)
== [N7]

\fx.(f^{8} x)
== [N8]

\fx.(f^{9} x)
== [N9]

\fx.(f^{10} x)
== [N10]

\abf.(fab)
== [MkPair]

\ab.a
== [Fst]

\ab.b
== [N0, Snd]

\pf.(f(p\ab.b)\fx.(f(p\ab.bfx)))
== [Trans]

\n.(n\pf.(f(p\ab.b)\fx.(f(p\ab.bfx)))\f.(f\fx.x\fx.x)\ab.a)
== [Pred]

>>> Pred N8
\f_x.(f^{7} _x)
== [N7]

>>> Pred N10
\f_x.(f^{9} _x)
== [N9]

>>> Pred N1
\fx.x
== [N0, Snd]

>>> Pred N0
\fx.x
== [N0, Snd]



And there it is!

## Defining the subtraction

This should be trivial by now: subtracting $$m$$ from any number $$n$$ is the same as finding the $$m$$-th predecessor of this number, and as our numbers are for-loops in disguise this is easy: $$Subt := \lambda nm.m\ Pred\ n$$.

(Do be precise: this is not indeed subtraction because we have no predecessors of zero, but to be even more pedantic: the natural numbers do not really have a meaningful subtraction – those numbers are not even a group under addition)

>>> Subt := \nm.m Pred n
\nm.(m\n.(n\pf.(f(p\ab.b)\fx.(f(p\ab.bfx)))\f.(f\fx.x\fx.x)\ab.a)n)
== [Subt]

>>> Subt N2 N0
\fx.(f^{2} x)
== [N2]

>>> Subt N4 N2
\fx.(f^{2} x)
== [N2]

>>> Subt N2 N4
\fx.x
== [N0, Snd]



## Conclusion

So as always this hard problem proved to be quite simple as soon as you know how. Maybe you even tried to find the solution yourself – if you did and did indeed mange to find it: congratulations – you might be a genius (for myself I have to confess: after trying for half an hour or so I went the easy way and asked google/wiki – what a shame, it looks like I might have found it … or not – will never know now)

I hope you enjoyed this one – I surely did – stay tuned for the next part.

# Introduction to Lambda Calculus

You might have heard that functional programming is based on Lambda Calculus – and indeed this is true (LISP was greatly influenced by Alonzo Church’s Lambda Calculus and you might have heard of “lambda”s in other functional languages as well) but originally Church tried to reason about mathematics not based on sets but on functions – and created Lambda Calculus as a tool for this.

For now this series is going to explain only the so-called untyped lambda calculus and I will not try to give you every single technical aspect (as this is rather involved and might look rather boring for people new to the ideas) – for example I will give you some of the definitions but will not go into the nastier technicalities concerning beta-reduction that can easily arise if accidentially bind a variable in the process.

I did write a small lambda-calculus interpreter you can download and play with, that does handle those problems (or so I hope – in case you find a bug with this please leave me a comment or a mail).

So let’s get started by giving you basic

## Definitions

Lambda Calculus deals with Terms so we should start by saying what a Term is. Well this is indeed rather simple – a term can be:

• just an Atom or Variable with a given name – that’s the basic blocks we won’t change
• an so called Abstraction that gives the hole thing it’s name: if $$x$$ is a variable and $$T$$ a term (so you see the definition is of course recursive) then $$\lambda x . T$$ is called an abstraction – will will think of this as a function taking a parameter $$x$$ with body $$T$$ but it’s important to understand that lambda calculus works by simply following rules without using any semantic meanings to the symbols!
• a construct called an Application: if $$A$$ and $$B$$ are terms than we will write this as $$(A B)$$ – we will think of this as applying the argument $$B$$ to the function $$B$$ but again: this is not important for the system but gives us a good intuition about what is happening behind the scenes.

That’s it – you don’t need any more syntax. But to make thinks a bit more readable I will allow to introduce names or identifiers for terms like this $$Id := \lambda x.x$$ and we will use a form of currying: Instead of having to write something like $$\lambda x . \left( \lambda y . (y x) \right)$$ I will allow to write $$\lambda xy. (y x)$$. And we will think of the application to be left assoziative, so instead of $$(A B)C$$ we will simply write $$A B C$$ – my interpreter allows you to do the same. By the way: as there is no $$\lambda$$ on your common keyboard the interpreter expects you to insert the abstractions as

Id := \x.x



## Magic calculations or the $$\beta$$-reduction

This is where things gets interesting. Look at a application $$A B$$ – if $$A$$ is an abstraction $$\lambda x.F$$ then we can use our intuition and think of this as the argument $$B$$ beeing applied to the function $$F$$ and the $$\beta$$-reduction rule does just this: it will substitute every “free” occurrence of $$x$$ in $$F$$ by $$B$$.

Here “free” is a bit of technical term – do make thinks not more complicated as they have to be: every $$x$$ in the body $$B$$ of a abstraction $$\lambda x.B$$ is said to be bound and the free variables are just those not bound – so this rule makes sure that we only apply the arguments to those places where we don’t “override” the meaning of $$x$$. There are other things you have to take care if you substitute terms (for example if you substitute $$y$$ by $$x$$ in $$\lambda x.y$$ you end up getting $$\lambda x.x$$ but the substitution should not change the meaning of the construct so you have to rename $$x$$ in there to make sure not to shoot yourself – take a look at the wiki article or consult a book if you are interested in this things – they are called $$\alpha$$-conversions and substitution rules).

So as an example let’s look use this rule on $$(\lambda x.x) a$$: the rule tells us to substitute every occurrence of $$x$$ with $$a$$ so of course the result is just $$a$$ (and your intuition that this is just a form of identity is surely right).

The “magic” here is that this rule is basically all you need to do computations!

Don’t believe it? Well let’s see how we can get lambda-calculus to add natural number…

## Natural numbers: representation and simple operations

You might remember from school that we can represent the numbers just by defining zero and a successor function that yields the next natural number after it’s argument. We will use this as well so we first have to say what zero should be in our calculus.

There are a couple of good definitions and you could start by saying that zero should be just an variable but as we deal with functions and as it will prove to be ingenious we will say that zero is a function of two arguments: $$Z0 := \lambda fx.x$$ (Hint: you can think of $$f$$ as a function and of our number representation as doing something like $$n \rightarrow x \rightarrow f^{n}( x )$$).

Now we need the Succ operator still and as the hint suggests this should just prepend one more $$f$$ in front of the argument number: $$Succ := \lambda n . \left( \lambda fx.f(nfx) \right)$$ – as you see this takes a number $$n$$ and “returns” (using our intuition) a function that “calls” $$n$$ with it’s arguments ($$f$$ and $$x$$) and passes the result of this once again into $$f$$.

So now that we have the representation of the natural numbers (for example $$3 == Succ (Succ (Succ Z0)))$$) we can look for something like an addition-operator – that is a function taking two numbers $$n$$ and $$m$$ (represented by our abstraction) and returning the representation of $$n+m$$.

This is not too complicated: $$Add := \lambda nm . \left( \lambda fx.nf(mfx) \right)$$.

So let’s try this to double $$1 == Succ Z0 == \lambda fx.fx$$:

$$Add 1 1 == \left( \lambda nm . \left( \lambda fx.nf(mfx) \right) \right) \left(\lambda fx.fx\right) \left(\lambda fx.fx\right)$$

$$=\beta= \left( \lambda m . \left( \lambda fx.\left(\lambda fx.fx\right)f(mfx) \right) \right) \left(\lambda fx.fx\right)$$

$$=\beta= \left( \lambda fx.\left(\lambda fx.fx\right)f\left(\left(\lambda fx.fx\right)fx\right) \right)$$

$$=\beta= \left( \lambda fx.\left(\lambda fx.fx\right)f\left(\left(\lambda fx.fx\right)fx\right) \right)$$

$$=\beta= \left( \lambda fx.\left(\lambda fx.fx\right)ffx \right)$$

$$=\beta= \lambda fx.ffx == 2$$

Or using my little interpreter:

LAMBDA CALCULUS INTERPRETER
===========================
>>> Z0 := \fx.x
\fx.x
== [Z0]

>>> Succ := \nfx.f(nfx)
\nfx.(f(nfx))
== [Succ]

\nmfx.(nf(mfx))

>>> Z1 := Succ Z0
\fx.(fx)
== [Z1]

>>> Z2 := Succ Z1
\fx.(f^{2} x)
== [Z2]

\fx.(f^{2} x)
== [Z2]



## Something similar using F#

Just to emphasize that F# as a functional programming can handle the same stuff: here is a simple F# script that demonstrates the same kind of defintions and operations for natural numbers – maybe you will find this more readable than the lambda-calculus stuff.

module NaturalNumber =
let Z0 = fun f x -> x
let Succ n = fun f x -> f (n f x)
let Add n m = fun f x -> n f (m f x)
let Z1 = fun f x -> Succ Z0 f x

let interprete n = n (fun i -> i+1) 0
do
printfn "1 + 1 = %d" (interprete (Add Z1 Z1))



As you can see this is more or less exactly the same we did with our lambda-calculus terms (we have to use the “fun f x –>” part for the compiler to be happy) and the “interprete” function is just to translate our intuition about the symbols like Z0 and Succ into F# representation for numbers.

That’s it for today – I hope you enjoyed this first overview on lambda-calculus – make sure to let me know what you think!

# now using DISQUS

I just installed DISQUS on this blog – I hope this will help me hold the spam down and you to a better user experience.

As always feel free to give me your thoughts…

# Testing MathJax

I am trying to include MathJax support in my Blog to make the math look nicer and use the great capabilites it provides.

So I hope you can all see this:

$\sum_{i=1}^n i = \frac{n(n+1)}{2}$

as a LaTeX rendered formula – if not please leave me a comment.

# upcoming series: Lambda Calculus

Long time since my last post – sorry for this but I’m gonna be more active in the future.

This post will start a series of entries dealing with Lambda Calculus so be prepared for some major geeky-fun.

With some very basic definitions you can see how you can do amazing stuff like adding numbers by just applying some simple rules.

If you got curious: you can find a simple lambda-calculus interpreter I plugged together to have some pain-free testing-tool for examples and exercises on my lcalcinterpreter codeplex page.