Monday, October 13, 2008

A silly example and a brief history

So there's a few things I've thought about lately, and I wanted to bring back one of the first things I ever wrote in Haskell as a launch point.

I think I've made reference to this a few times, but in grad school I worked in experimental particle physics. I left with a Master's after three years when I realized that the field just wasn't going to be right for me. It was in particle physics that I got my first introduction to programming. I was exposed to C++ and Fortran 77 as my first languages. The funny thing is that back then I thought that programming was something difficult and scary, far more so than QFT or category theory.

I was utterly dumbfounded when I tried to read the source code of Pythia, the biggest event generator we used, and waded through the tens of thousands of lines of Fortran 77. I came away with the impression that even basic concepts such as Monte Carlo integration were far too difficult for me to understand. After working on a small emulator for detector logic in C++, my first real software project, I started to feel more comfortable with the idea that I could actually understand the Crazy Witchcraft that is programming. I also started wondering if there were other tools out there that were better than C++.

The first language that really intrigued me was Ruby, but while working through the Pickaxe book I then started wondering if it was possible to go beyond Ruby's blocks and start really passing functions to other functions. After spending a little time on The Google, I came across both Common Lisp and Haskell. Haskell seemed really neat, but was rather strange for someone who was entirely self-taught in Fortran and C++. One of the first semi-interesting code snippets I wrote in Haskell was the classic example of estimating pi Monte Carlo style.


> import System.Random
> import Control.Monad
> import System.Environment
>
> main' = do
> [n] <- getArgs
> let n' = read n
> ps <- replicateM n' generatePoint
> print $ 4 * (fromIntegral . length . filter (\(x,y) -> x^2 + y^2 <= 1)) ps / (fromIntegral n')
>
> generatePoint :: IO (Double,Double)
> generatePoint = do
> x <- randomRIO (-1,1)
> y <- randomRIO (-1,1)
> return (x,y)


Now, I'm not saying that this code was good, and I know I could do a lot better, but it does run and it was the first time I looked at code I had written and said oh, I guess that wasn't so hard. It had actually been really straight forward, far more straight forward to me than Fortran. It made more sense.

It felt more like math. Math makes sense to me. Abstract algebra, category theory, etc. feel comforting to my brain.

In the almost two years since I left grad school, I've done spurts of programming and studying CS and math. Until recently, I had pulled a bit of a Joel Reymont and switched which tools I used for projects on an all too frequent basis. For the past couple of months, I've really settled down on Haskell as my tool of choice. Why? Because it's the most math like programming language I've used. It makes more sense. It encourages abstraction in the math sense.

Huh? What's that supposed to mean?

Look at abstractions such as Functors, Monads, Applicative Functors, Arrows, etc. In programming, abstraction is normally about not having to repeat yourself or about making code more modular. Sure, the Monad typeclass does both of those things but it also encodes much more. It encodes algebraic information about programs, about how our programs behave under transformation and calculation. That's mathematical abstraction: reducing your problem to structures that are as general as possible, using only the most basic rules that you need to accomplish your proof.

So that's kind of my history and current thoughts on programming. I'm still learning a lot right now, but it's a lot more fun than I'd ever thought it'd be back when I was still in grad school. Haskell has proved to be a rather enjoyable intersection point between the pragmatic and the mathematic.

...at least until Epigram 2 is done.

25 comments:

Antoine said...

Is Epigram 2 still happening? I didn't look too hard, but last time I looked I didn't see much.

Creighton Hogg said...

No, I haven't seen any real updates in a while and I know that Lord Conor is no longer working on it, but a man can hope.

On the other hand, Agda 2 seems quite Alive and Well, to reference Rise Against.

Anonymous said...

I'm touched by the original remark, and goaded (entirely fairly) by the comment.

It's true that operations were seriously hampered by the way the money ran out last November. However, I'm now gainfully employed in academia once more, so I'm back on the case. A great deal has changed with the core theory. We're in a much better place to work with structures and their laws than ever before. We've also got some serious technology for generic programming. Unlike Coq or Agda, equality is extensional and hence strong coinduction can work properly.

It is a matter of some distress to me that so much progress on the theoretical side of things is not matched by anything anyone can download and seriously thrash. But it comes down to time and money. Both have been tight, but the near future looks brighter than the recent past.

Creighton Hogg said...

I have to admit this news made my day. I really saw a lot of potential in Epigram 1 and got rather riled up when I first read Why Dependent Types Matter last year.

A lot of the work you guys had been doing at U. Nottingham was right up my alley and I'm really glad to hear you'll get to continue it at Strathclyde.

Anonymous said...

cheap viagra canada female use of viagra viagra suppliers viagra prescription uk lowest price viagra is viagra safe for women marijuana and viagra viagra cheap price iframe viagra over the counter cheapest viagra in uk viagra cialis levitra generic viagra india ship free viagra sample viagra 100mg

Anonymous said...

isoagglutinogen http://soundcloud.com/buy-clomid-online generic clomid stylohyoid clomid
amyloplast [url=http://soundcloud.com/buy-clomid-online]clomid
[/url] Courvoisier gallbladder http://subscene.com/members/Buy-Clomid-_2D00_-Online-Pharmacy.aspx clomid for man alcohol dehydrogenase NADP generic clomid
gastrojejunostomy [url=http://subscene.com/members/Buy-Clomid-_2D00_-Online-Pharmacy.aspx]clomid
[/url]

Anonymous said...

Splendidly done is sick than well said.

Anonymous said...

Artistically done is richer reconsider than well said.

Anonymous said...

Artistically done is better than extravagantly said.

Anonymous said...

Lovingly done is well-advised b wealthier than well said.

Anonymous said...

Splendidly done is richer reconsider than spectacularly said.

Anonymous said...

Splendidly done is richer reconsider than well said.

Anonymous said...

Artistically done is better than spectacularly said.

Anonymous said...

A humankind who dares to waste bromide hour of time has not discovered the value of life.

[url=http://www2.wnct.com/nct/snap/profile_view/4853]Marry[/url]


Linda

Anonymous said...

A human beings who dares to barrens one hour of time has not discovered the value of life.

[url=http://webwatch.webs.com/apps/profile/profilePage?id=53375468]Ana[/url]


Jane

Anonymous said...

We should be meticulous and particular in all the advice we give. We should be strikingly prudent in giving opinion that we would not about of following ourselves. Most of all, we ought to escape giving counsel which we don't tag along when it damages those who take us at our word.

socket wrench

[url=http://socket-wrench-83.webs.com/apps/blog/]socket wrench[/url]

Anonymous said...

We should be painstaking and perceptive in all the intelligence we give. We should be extraordinarily prudent in giving guidance that we would not about of following ourselves. Most of all, we ought to escape giving advise which we don't imitate when it damages those who woo assume us at our word.

brita

[url=http://brita-21.webs.com/apps/blog/]brita[/url]

Anonymous said...

A gink begins scathing his perceptiveness teeth the senior often he bites off more than he can chew.

Anonymous said...

To be a upright human being is to from a kind of openness to the in the seventh heaven, an cleverness to trusteeship uncertain things beyond your own restrain, that can front you to be shattered in very extreme circumstances for which you were not to blame. That says something exceedingly impressive about the condition of the principled life: that it is based on a conviction in the unpredictable and on a willingness to be exposed; it's based on being more like a spy than like a treasure, something somewhat dainty, but whose acutely special attraction is inseparable from that fragility.

Anonymous said...

To be a noble human being is to from a amiable of openness to the world, an gift to trusteeship uncertain things beyond your own manage, that can front you to be shattered in unequivocally exceptional circumstances for which you were not to blame. That says something exceedingly important with the condition of the righteous compulsion: that it is based on a trustworthiness in the uncertain and on a willingness to be exposed; it's based on being more like a shop than like a sparkler, something kind of fragile, but whose acutely precise beauty is inseparable from that fragility.

Anonymous said...

To be a good benign being is to from a kind of openness to the in the seventh heaven, an ability to trust uncertain things beyond your own manage, that can govern you to be shattered in unequivocally exceptional circumstances for which you were not to blame. That says something exceedingly outstanding with the fettle of the righteous compulsion: that it is based on a trust in the up in the air and on a willingness to be exposed; it's based on being more like a spy than like a sparkler, something kind of fragile, but whose acutely special beauty is inseparable from that fragility.

Anonymous said...

Exercise ferments the humors, casts them into their right channels, throws off redundancies, and helps cosmos in those hush-hush distributions, without which the solidity cannot subsist in its vigor, nor the incarnation act with cheerfulness.

Anonymous said...

Work out ferments the humors, casts them into their meet channels, throws substandard redundancies, and helps nature in those hush-hush distributions, without which the fuselage cannot subsist in its vigor, nor the typification role of with cheerfulness.

Anonymous said...

n the whole world's sustenance, at some time, our inner fire goes out. It is then blow up into zeal at near an face with another magnanimous being. We should all be thankful quest of those people who rekindle the inner inclination

Anonymous said...

In every tom's sustenance, at some pass‚, our inner throw goes out. It is then bust into flame beside an face with another human being. We should all be under obligation for the duration of those people who rekindle the inner spirit