Abstract Absurdities

Weight Loss: When Hungry, Eat

2010-01-27T18:35:00.000-08:00

I'm still plugging away at a number of technical topics, so I wanted to share a bit more of my experience with food and weight loss.

There's a rule that I didn't mention last time, and it's possibly the most important of all of them: when you're hungry, eat something. I discovered that in order to keep losing weight over a long period, I couldn't starve myself. I had to eat whenever I felt like my body needed food and I had to eat until I wasn't hungry. Sometimes that's meant eating four or five small meals in a day.

Eating when you're hungry is a little scary when you've had problems with your weight. It's easier to have rigid rules for what and when you eat. There is, and probably always will be, a little voice that's scared of putting it all back on again. That's a reasonable concern, after all! To deal with this voice, you simply have to listen carefully to your body's signals of what it needs and trust that countless ages of evolution have - in fact - provided you with the tools you need.

Weight Loss: My Success

2010-01-18T14:34:00.001-08:00

I've spent most of my post-teenage life struggling with my weight. About 16 months ago, I made a fairly radical change to my eating habits and I've now lost 103 lbs.

There's two major things I changed about my diet. First, I ate less sugar. Second, I ate slower. Before I get into the details, I want to clarify something. I am a vegetarian now, but that's a decision unrelated to my attempt to lose weight. I lost over 60 lbs before I became a vegetarian. Vegetarianism wasn't a prerequisite.

Eat less sugar. That sounds pretty simple, doesn't it? Unfortunately, it was a lot harder than I thought it would be. A lot of preprocessed foods, including most bread you'll find in the super market, include superfluous high-fructose corn syrup. Even foods that market themselves as healthy will include copious amounts of sugar; they just cut out the fat instead. Unfortunately, that's the opposite of what my experience has taught me. I choose fat over sugar. My body can actually break down fat and do something useful it.

I found that once I reduced the amount of sugar I consumed drastically, my appetite became more regular and manageable. I get hungry again quickly when I have sugary food and it's usually accompanied by headaches, not by an empty stomach. I also have a harder time telling just how hungry I am when I've had much sugar. It scrambles my sense of what I need. I'm really vigilant now to check the labels of food I buy in the store. I also cook more of my own meals than I used to.

Fresh fruit is my one exception to the above rule. Fruit doesn't cause me any of the problems that, say, corn syrup laden bread does. I don't entirely understand why, but it seems to be broken down differently.

Eating slow was the other key change to my life style. If I wolf down my food, I can very easily eat more than I actually need without realizing it. I discovered that if I just slow down, take breaks, and take the radical step of chewing that I can actually tell when I've had enough food. I was never aware of the whole spectrum of sensations in my stomach until I slowed down and paid attention. I was amazed to discover that there's more than just "starving" and "stuffed".

Just these two things, I think, were the most important parts of my experience losing weight.

How to teach Category Theory?

2009-10-10T17:06:00.003-07:00

So I'm teaching an intro to category theory course this fall at Portland State, my new place of employment.

Now, I think it's going alright. I have only 6 people in on this class, including one professor, but I imagine that if I teach it again in the future and advertise it a bit harder that there will be more.

It's been an interesting experience, though, because I've realized one of the big problems with trying to explain category theory: it's too young a field. We have all the definitions, but none of the metaphors. There's no coherent narrative to give you intuition. "Categories for the Working Mathematician", one of my all time favorite books, cheats pretty seriously on this front. It never gives a basic vocabulary to use to describe any of these structures, it just gives so many examples from other areas of math that you start to build an intuition; however, you have almost no words with which to explain this intuition.

I was inspired to write more about this because of a thread on reddit. I strongly disagree with the sentiment that one should be able to explain the concepts of category theory in terms of functional programming. Some ideas in category theory- such as representable functors, adjoints, hom-sets, topoi - are general enough that any attempts to squash them into Haskell code is simplifying to the point of confusion. An example of this is Dan Piponi's old post on the Yoneda lemma. While it's good and gives intuition, it's also a bit of a lie- the Haskell arrow (->) is not actually a hom-set and Yoneda is all about the relation between hom-sets and natural transformations that allows you to embed any category C into the category of functors from C to Set, a category with much richer logical structure. As much as the analogy to Haskell helps, I think it hurts by making the big, general, picture harder to see.

So is the solution to suck it up and just bang your head against Mac Lane, never thinking about how it relates to code? Of course not! Let's take a slight detour, first, before talking about what to do.

So Paul Graham has this famous essay - famous enough I don't even see a point to linking it - about "Blub programmers" and how they're blind to the powers of better tools because they only know Blub. It probably wasn't Graham's intent, but this essay is usually referenced by language evangelists to explain why some programmer they talk to isn't instantly willing to adopt their favorite language despite how awesome it is. It's a seductive explanation. The people who disagree with them don't "get it" or just aren't trying.

The more likely reason? They're terrible at explaining why their language is good.

When I was a grad student in physics, most of the grad students (myself included, much to my shame) joked about how dumb all the pre-med students were and how they never wanted to do any work, because that was the most convenient explanation for why there were so many complaints about how hard & confusing the labs, lectures, etc. were.

The more likely reason? We were terrible at explaining physics.

That brings me back to the course I'm teaching. I'm spending the majority of my time trying to figure out real metaphors for explaining category theory, especially with respect to its uses in Computer Science.

So far, the basic story I'm going with is that category theory is about "modeling structures". Functors are about instances of models in a target category. Natural transformations are ways to move between two models in a "coherent" fashion. I'm still fleshing out this language, and I don't know how terribly helpful it will be at the end of the day, but I'll be cleaning up and releasing my notes at the end of the term as one long pdf. The point is that there's still a lot of programmers, computer scientists, and even mathematicians that don't see category theory for the beautiful foundational math I see. Now, it's possible that they're all stupid or don't want to work.

The more likely reason?

Fear of releasing code

2009-01-24T21:33:00.004-08:00

Alright, so this post is going to be all Captain Emo. I wanted to write about something I've realized I do, with the hope that if someone else is unfortunate enough to have the same habit that maybe they'll realize it as well.

I sometimes have a ridiculously irrational fear of actually finishing up & releasing my personal projects.

Of course, it doesn't manifest itself as transparently as "oh, crap, people might see my code & think I punch puppies". It's much more of a "gosh, I just don't know if it's really tested enough yet" or "why don't I add a few more features first" or "I'll just tweak the API a bit" or even the insidious "I'll work on that tomorrow". Oh yes, "tomorrow" being that wonderful code word for "maybe around the time I start laying golden eggs". Sometimes I've even thrown out a good chunk of work I had finished because I thought of a "better way" which mysteriously never gets coded up.

Here's the important point I've been thinking about: something is only perfect if it doesn't exist. If you want to actually accomplish anything, you're going to release stuff that is buggy, non-optimal, & might not even compile on anyone else's machine. That's okay. It can get fixed!

I've never lost respect for someone because of a bug in a library. I've only gained respect for them when they fix it. I'm probably not the only one who feels that way.

An almost religious experience

2008-10-30T05:05:00.004-07:00

Alright, so this is a bit off topic for this blog but I had to talk about something that amazed and astounded me.

Last night, after the Obammercial, I was flipping through the channels and I came across a sitcom called "Under One Roof" starring, not joking, Flavor Flav and a cast of people designed to make Mr. Flav not look like the craziest person on the set.

This show was so strange & surreal that at any minute I expected the real credits to roll and for it to be some extended sketch of another comedy show. For God's sake, it actually featured a wacky-Asian-stereotype cook who uttered the phrase "me so horny". The strange gesticulations, the bizarre dialog, the constant mugging & posturing for the camera all made it impossible for the brain to accept that it was watching something non-ironically meant for entertainment. Yet sure enough the credits rolled after a half-hour.

Then it hit me.

I had just witnessed the first Dadaist Sitcom. This wasn't just not funny, it was true anti-art. It wasn't that the show failed at entertaining. It succeeded at destroying the very concepts of entertainment & humor, leaving only a void. A void that challenged my fundamental assumptions about the place of entertainment in society. It made me question not why this show existed but why no other could be so profound and challenging.

Debugging & Refactoring, a mid-mortum

2008-10-28T15:15:00.001-07:00

So I haven't touched my Bluetooth bindings in the past week, having been a bit intimidated by the prospect of sitting down and making the necessary network interfaces to actually handle doing real communication & not just simple queries. I can tell it's not going to be too hard once I get started, but it doesn't look like the most exciting thing in the world.

To get my motivation up, I worked instead on some of the small physics games into which I wanted to eventually integrate wiimote controls. Making a small game engine in Haskell hasn't been entirely easy, but that's more a function of my inexperience & that I don't think I've been using language features to their best advantage.

I lost a bit of my time wrestling with trying to make the engine interface feel "object oriented", which is where my mini-rant about type class abuse last week came from.

At this point, though, I have a good percentage of the code I need to make a few of my game ideas; however, the percentage of code that's working in all the cases it needs to is much smaller, particularly the generic collision detection & handling for polygons. There's a number of cases in my testing that keep coming up with unexpected results.

I've spent some time in the GHCi debugger, which is actually a lot more easy to use than I expected. If you haven't used the debugger yet I recommend that you read issue 10 of The Monad Reader and the rather nice tutorial provided therein. One minor thing I want to emphasize about using the debugger is that if you force a value that's returned by a function before you start stepping through the function, you won't actually step through the function by doing :step. GHCi will just continue with whatever compuation is done with the value you forced. Again, it's a minor thing but it took me a few seconds to realize why I skipped over the step-thru of one of the functions I was trying to diagnose.

Even though the debugger is actually fairly nice, my real problem is that I've made a number of small logical mistakes & built upon those mistakes without realizing I had made them in the first place. I think a good next step for this project would be to start pulling in the old QuickCheck machinery, trying to define the algebraic properties the functions in the physics engine should obey, refactoring the whole mess, and making sure it passes all of my tests from the get-go. This should prevent the "Oh, I think everything is fixed now so let's just start bouncing some squares around the screen...looks good...great...@#%*!" loop.

More on OS design

2008-10-27T15:00:00.002-07:00

I've been thinking a bit again about modern type systems with respect to operating system design and I think I can describe heuristically some of my old ideas and the open questions I still have. If there are comments or ideas, I'd love to hear them.

I like modern type systems. I also like capabilities. How can we combine them together? I used to think I had more solid leads on this question, but now I feel a little shaky. What I wanted to do was have a set of capabilities, essentially just indexes into some resource mapping in the kernel, be attached to each process. The actual access rights for each resource would be encoded as a phantom type in the capability. So for each resource type you'd have some set of operations that would have preconditions about the phantom types they would find acceptable. If you wanted to pass a capability to another process you can use provided functions for making a copy securely, giving any level of permissions less than or equivalent to your own.

Now there are some things that I think make sense here: the more we can shove questions of safety into the type system, the less we have to do at runtime and the better scalability you can have. Also, I think it encourages a very different UI experience. To see a resource you need to have a capability to it, but if you're dispatching over the type of capability then presumably you could do something like have the only shell commands available for that resource be the ones that match the type signature of the resource. I'm not sure how to actually implement a feature like that, but it seems like it should be feasible on a moral level.

I feel like there's three questions I have to answer in order to take the idea from "oh that's kinda cute" to something real. The first problem is bootstrapping and snapshotting of the OS. I haven't even begun to think about this, honestly.

Another issue is how the process and system call model would have to work. We'd want the system calls to be somehow typechecked for proper capability use. Again, I'm not sure of a good scheme for this that doesn't restrict execution to just the host language. Perhaps the bullet that has to be bitten involves making some form of FFI for each compiler that should target this system so that the system calls are made in the host language and then type checked at compilation.

The last issue that's still fuzzy in my head involves storing capabilities for a process. Now, it's all fine and dandy to say 'it's a set', but most data structures in a language such as Haskell are homogenous. What I need is a heterogenous container that doesn't completly lose type information, which means that using type classes and existentials is right out. I know Oleg Kiselyov has done work with thing like HList, but that's something I don't know much about.

Revisiting old concepts

2008-10-23T15:00:00.001-07:00

In an old post I threw out the perspective that typeclasses & exokernels are similar ideas, but I explained it so pithily I think it was more or less incomprehensible. Honestly, even I had to sit & think for a minute to figure out what I meant over a year ago.

The idea wasn't really that profound, but did amuse me a little.

Let's say that you design a type class called Hardware, maybe even require that it be a monad or at least applicative, that includes all of the functionality you'd want from an exokernel, i.e. protection & raw handling of resources. You should also define a set of algebraic properties that you want all of these operations to satisfy in practice.

Any actual instance of this type class that satisfies all of our conditions is an implementation of an exokernel.

Then your libOS, the part that does all the nasty work of management of resources, can be polymorphic over the implementation and only work with the basic protection interface defined by the type class.

This whole business occurred to me a long time ago because of reading the original House paper and their discussion of the H monad. They don't quite take it in this direction, but I think that it seems feasible.

I'm being a little hand-wavy, though, because this isn't something I've
actually tried to make. It just seems like a compelling bit of imagery & possibly a good idea for organizing a kernel.

A serious problem

2008-10-22T11:50:00.000-07:00

Hello,
I'm Creighton Hogg and I want to talk to you about typeclass abuse.

Like any form of substance abuse it may seem harmless at first, a way
to recapture the old feelings of modularity you had during your
object-oriented youth; however, you'll quickly find yourself twisting
and obfuscating your code to design the signatures of your typeclass
methods so that they can cover a wide swath of cases that are
fundamentally dissimilar.

Have you noticed signs of:
1. Obsession over reuse of the names of functions?
2. Attempts to use typeclasses to try and treat collections of
dissimilar objects as though they were the same?
3. A frequent need for typeclasses with two or more type
variables?

If so, you may be in grips of typeclass abuse. Please keep the
following in mind as you attempt to deal with your problem.

First, if you want to have a collection of objects that are treated
differently by functions, please consider using an Algebraic Data Type
instead. For more fine grained control over your data types, you may
want to look into GADTs.

Second, if you are needing a number of classes with two or more type
variables, consider that you may be attempting to use a language feature
designed to enable polymorphism to handle extremely specific and
dissimilar cases. You are working against the grain of the language,
and should probably simply accept that you can't overload a function
name to be 20 different functions that each do different things.

Lastly, if you're not actually sure if a typeclass would make your code
more convenient, why not just try writing your code without it? When
you've got a number of use cases down, then maybe you can decide on what
the proper abstraction is.

This message paid for by the Foundation To Get Creighton To Stop Abusing
His Code, a non-profit organization.

Brief updates

2008-10-13T16:13:00.002-07:00

So two quick notes:

I've been working on my Haskell bindings to BlueZ and I can now detect my wiimote. I can't read anything from it or tell it to do anything, but I know it's there. I'm hoping to have some kind of actual release done next week.
Any political candidate who starts talking about how "great" our country is should be poked in the eyes, 3 Stooges style. We know you like the place or you wouldn't be running for office and if you keep talking about how great things are you look like you don't have ideas to make it better. Seriously.

A silly example and a brief history

2008-10-13T09:08:00.002-07:00

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.

Working through Genetic Programming

2008-10-07T17:41:00.005-07:00



> import Random
> import Control.Monad
> import Control.Monad.Random
> import Data.Ratio
> import Data.List (sortBy)

So I really did accomplish my reading of the first three chapters of Koza's first book on Genetic Programming the week I said I would, but I sat on this post for a good bit afterwards. There wasn't a lot of meat in those initial chapters except for a few salient points:

Genetic programming can give you good answer if you're willing to accept that the answer is not 'correct', merely accurate and if you're willing to lay aside preconceived notions of beauty in your solutions.
Due to the schema theorem, a genetic recombination/fitness based search can effectively cover a large swath of the solution space with a small population.

The majority of Ch. 3 of the book is devoted to Old School genetic algorithms and the schema theorem. I'm not going to bother going through fully fledged examples of the schema theorem, but I think the point can be understood fairly intuitively: when you proportionally select the fittest specimen to be in the mating pool of each generation, you are making judgements about the fitness of patterns of genes and thus gather information about not just the specimen you have but all the possible specimen that have overlapping genetic structure.

What I want to do in the rest of this post is just write my own tiny, not terribly well-featured, genetic algorithm implementation. I'm hoping that this will provide not only more practice for me, but also be instructive to others. I base the implementation more upon the heuristic description that Koza gives than on anything else and make no claim that this is any kind of optimal construction.

First, since I hope to express my code at least somewhat generically between genetic algorithms and genetic programs, I'm going to define a typeclass to capture the basic behavior required of a "genetic" structure. Also, it is worth noting that in this post I'm going to make gratuitious use of the Control.Monad.Random library just because it feels somehow appropriate to be doing these calculations in a monad.



> class Genome a where
>     mutation :: MonadRandom m => a -> m a
>     recombination :: MonadRandom m => a -> a -> m (a,a)
>

Oddly enough, that didn't seem too terrible. We have no notion of how often something like mutation in the typeclass, because that should be controlled at the level of the actual implementation.

Now, though, we'll define an instance of this class for lists as that's probably the easiest thing to do. I do, however, make the implicit assumption that in a given simulation all the specimen are of the same length.



> 
> instance Random a => Genome [a] where
>     mutation xs = do
>                   i <- getRandomR (0,length xs - 1)
>                   x' <- getRandom
>                   return $ replaceAt i xs x'
>     recombination xs xs' = do
>                          i <- getRandomR (1,length xs - 2)
>                          let (xs1,xs2) = splitAt i xs
>                              (xs1',xs2') = splitAt i xs'
>                          return (xs1++xs2',xs1'++xs2)
> replaceAt i xs x = xs1++[x]++(drop 1 xs2)
>               where (xs1,xs2) = splitAt i xs

At this point we can start putting together the real framework for a genetic algorithm run. The first, and relatively easiest function to compute will be the one to choose the mating pool for the next generation given a fitness function and a list of specimen. I assume a constant population size for the course of the simulation, so the outgoing list will have just as many members as the in going list. We also do our selection based entirely upon the relative fitness between the specimen of the population, an idiom captured quite well in the fromList function in the Control.Monad.Random library.



> chooseMatingPool :: MonadRandom m => (a -> Integer) -> [a] -> m [a]
> chooseMatingPool eval pop = replicateM l $ fromList weighted
>     where weighted = map (\p -> (p, eval p % 1)) pop
>           l = length pop

Now I'll admit that I'm limiting the fitness function a little by requiring it to return Integer values, but I honestly feel like that's a generality that I'm willing to lose for the purposes of this post and for the convenience of using fromList.

Next will be the handler that sexually recombines the mating pool. I cheat a little here and presume that since the order of the mating pool was selected randomly that I don't need to shuffle them any more when I perform the selection and thus I can just take pairs of specimen, breed them, then put them back in the list. If there's an odd man out, or as I like to call him "Creighton in High School", then we don't breed him with anyone and just put him back in the pool.

The function to implement mutation in the population is also extremely trivial so I'll throw it in below without much ado.



> breed :: (MonadRandom m, Genome a) => [a] -> m [a]
> breed [] = return []
> breed (x:[]) = return [x]
> breed (x:y:xs) = do
>   (x',y') <- recombination x y
>   xs' <- breed xs
>   return $ x':y':xs'
>
> mutate :: (MonadRandom m, Genome a) => Double -> [a] -> m [a]
> mutate chance pop = mapM (mutate' chance) pop
>     where mutate' c a = do
>             result <- getRandomR (0,1)
>             if result < c then mutation a else return a

Alright, so the next minor hurdle is going to be generating the initial population we need. Now, my cheating with lists has painted us into a slight corner where we can't be as generic as we'd like. The problem is that there are two conflicting imperatives at work here. First, that lists are a very convenient way to deal with sets of genes. Second, that the lists in a single simulation must all be of the same size. The result is that I can't write any generic instance such as



  instance (Random a) => Random [a] where
    ...

useful in all instances, since I want to be able to use different size lists, or arrays for that matter, for different simulations. What would be the slickest solution? Depedently typed arrays with the size as a part of the type. However, in a world without dependent types we can still write something that works even if the lack of clean semantics annoys me.

In any case we can now start wrapping the whole thing up a bit more into larger control structures. I think these are fairly straight forward, but the main function is runSimulation. It takes in the number of runs to execute, the performance threshold for declaring an early end, the probability of mutation, the evaluation function, and the initial population. That's a lot of parameters!



> randomList :: (Random a,MonadRandom m) => Int -> m [a]
> randomList i = liftM (take i) getRandoms
>
> initialListPopulation :: (Random a, MonadRandom m) => Int -> Int -> m [[a]]
> initialListPopulation s l = sequence $ replicate s $ randomList l
> 
> simulationStep :: (MonadRandom m, Genome a) => Double -> (a -> Integer) -> [a] -> m [a]
> simulationStep mut_chance eval pop = chooseMatingPool eval pop >>= breed >>= mutate mut_chance 
>   
> maxInPopulation :: (a -> Integer) -> [a] -> (a,Integer)
> maxInPopulation f = head . reverse . sortBy (\(_,w) (_,w') -> compare w w') . map (\p -> (p,f p))
>
> runSimulation :: (MonadRandom m, Genome a) => Int -> Integer -> Double -> (a -> Integer) -> [a] -> m a
> runSimulation 0 _ _ eval pop = return $ fst $ maxInPopulation eval pop
> runSimulation runs threshold mut_chance eval pop = do                               
>                    if snd (maxInPopulation eval pop) >= threshold 
>                       then return $ fst (maxInPopulation eval pop)
>                       else do
>                            newpop <- simulationStep mut_chance eval pop
>                            let finalpop = takeBest eval pop newpop
>                            runSimulation (runs-1) threshold mut_chance eval finalpop
>
> takeBest :: (a -> Integer) -> [a] -> [a] -> [a]
> takeBest eval xs xs' = take (length xs) . reverse . sortBy (\p p' -> compare (eval p) (eval p')) $ xs++xs'

Now we have enough framework in place that we can introduce an actual, executable, example. In accordance with a tutorial I saw once, we'll evolve the string of all 'True's as a quick test.



> evalOnes :: [Bool] -> Integer
> evalOnes = foldr (\b s -> let v=if b then 1 else 0 in v+s) 0
>
> main = do
>   p <- initialListPopulation 50 20
>   final <- runSimulation 200 20 0.01 evalOnes p
>   print final

I've done some preliminary testing and found that for this size of problem it still quite often finds the list of 20 Trues within the 200 generations. I'm sure if I played a bit more with how the population was chosen I could get it to be much more optimal, but I plan to worry more about that when I tweak my code to accommodate monotypic genetic programming instead of just fixed length genetic algorithms.

Random Thoughts and Idle Speculation

So first off, I found this code extremely easy to write. Now that I'm pretty much using Haskell for all of my personal projects and toys, I've come to appreciate just how effortless writing code starts to feel. It's just a language that stays out of my way when I'm trying to figure out a problem, and that's about the best compliment I think I can give a tool.

Also, as I've continued reading Koza's book I'm starting to wonder about what exactly makes genetic programming so much more powerful than straight up genetic algorithsm. I'm guessing it really comes down to the richness and varying size of the structure being evolved rather than the fact that you're evolving a parse tree. There's some ideas tickling at the back of my head about what about qualities a data structure, a functor, needs to satisify to be "evolvable". Hopefully I'll be able to clarify some thoughts about that as I continue reading the book.

Some first steps with Data.Reactive

2008-09-30T19:50:00.001-07:00

I've had a pretty busy last week and I began to go down the path of neglecting my poor, tiny blog. Don't die on me, tiny blog! I will grant you the content you desire to make you happy!

Alright, so a friend of mine asked me about Data.Reactive a few days ago and I wanted to share a couple of small examples and even questions about the proper use of this library.

For those who haven't seen it, Conal Elliot has made a slightly brain-twisty new library for doing functional reactive programming, i.e. a way to make interactive programs with clean semantics. What follows is my attempt to make a simple chat server that uses Data.Reactive to handle logins and echoing text. I'm partly cribbing from a good example on haskell cafe and unabashedly borrow some of Mr. Stephen's function definitions. I'm not claiming this is a good example of using Data.Reactive, only that it merely works and this was my way of learning about the library. If anyone with more experience can comment as to my use/misuse of the Conal's work, it would be most appreciated.


> module Main where
>
> import Control.Concurrent
> import Control.Concurrent.STM
> import Control.Applicative
> import Control.Monad
> import Data.Reactive
> import Network
> import System.IO
>

The function socketServer is going to be our introduction to using Events in Data.Reactive. It returns an event source that we can use to grab handles as they are created by the acceptConnection function. An important point that I found embarrassingly confusing is that you don't need to do any plumbing between the event and sink. The sink is just a function of type a -> IO () that populates the event whenever it is called. acceptConnection is just a simple function that accepts the the connection then passes that into the sink that we created with mkEvent.


> socketServer :: IO (Event Handle)
> socketServer = withSocketsDo $ do
>                  (event,sink) <- mkEvent 
>                  socket <- listenOn (PortNumber 5000) 
>                  forkIO $ forever $ acceptConnection socket sink
>                  return event
>
> acceptConnection :: Socket -> (Handle -> IO ()) -> IO ThreadId
> acceptConnection s sink = do
>   (h,_,_) <- accept s 
>   hSetBuffering h NoBuffering
>   forkIO $ sink h

Now seeing these functions, you might be wondering what you need to do to get at the data in the event that's returned by this function. Well, we only have to take a look at the documentation for Data.Reactive on hackage to see that Event is an instance of Functor and that this functor instance allows us to lift a function of type a -> IO b to a function Event a -> Event (IO b). Looking at the documentation again, we find a wonderful little function called runE that has type Event (IO b) -> IO a so lets put these together into one tiny program.


> main' = do
>   e <- socketServer 
>   runE $ fmap (\h -> print h >> hClose h) e

This is a pretty braindead example, but it will print a line to stdout every time that a new connection is made to the server. Now lets go ahead and make it so that as new events occur we launch a connection handler that allows us to turn this into a real chat room. We'll also, just to be gratuitous, also use events to manage the incoming messages and their distribution.


> main = do
>        e <- socketServer 
>        (msgEvent,sink) <- mkEvent 
>        runE $ fmap (forkIO . (handleCloser $ handler msgEvent sink)) e
> handler :: Event String -> (String -> IO ())-> Handle -> IO ()
> handler e sink h = do
>   subscribe e (hPutStrLn h)
>   forever $ hGetLine h >>= sink
>
> handleCloser ::  (Handle -> IO ()) -> Handle -> IO ()
> handleCloser action h = catch (action h) (const $ hClose h)

Okay, so not really that much changed in this version. The big change is that we now have two sets of events, one that for the handles and one for the messages. We also use the subscribe function to launch the threads that display messages to everyone logged in, subscribe being a slightly misleadingly typed function that takes in an event and a consumer and spawns a new thread feeding the event data into the consumer. Now, all you boys and girls following along at home will probably notice a major oversight: at the moment, there's no real way to close down the chat server cleanly. Also, I cheat and don't properly handle logouts except for closing the handle when it hits an error.

I'm also working on another use of Data.Reactive with some of the SDL toys I've written. Maybe I should port my pong clone over to it, if I have copious free time.

One last thought on laziness

2008-09-30T11:45:00.003-07:00

So while I'm working on a couple of other posts I want to put up over the next couple of days, I did want to throw out some last words on this whole lazy evaluation business & advice for learning Haskell.

I'm of the opinion that laziness is the single hardest thing to get used to in Haskell: not warm fuzzy things, not higher order functions, not syntax. The reason why it's taken me awhile, having used Haskell more off than on for small toys over the past couple of years, to really grasp how to use lazy evaluation is that it forces you to think about the combination of your functions and data much more carefully.

Let's take a really silly example such as

head . map (+1)

because it's something that is easy & obvious. If you apply this function to a list of numbers the evaluation can proceed something like the following:

head . map (+1) [1,2,..]
head $ ((+1) 1):(map (+1) [2,...])
((+1) 1)
2

To anyone remotely familiar with the concept of laziness I'm sure this seems somewhat intuitive. You only need the first element of the list, so only the first element has the argument to map applied to it. It's a simple consequence of the structure of lists and the definition of map, the kind of example that you can feel comfortable with after just a minute with a pencil and paper. So what's my point?

My point is that if you're learning Haskell and you're running into problems with laziness, you should break out the pencil & paper and try to calculate what will happen when your function is called. It's something you don't really have to do with other languages, but I think it's the best way to see how your functions and data structures interact during evaluation until you have better intuition.

Laziness redux

2008-09-22T16:32:00.003-07:00

Okay, so last time around I made reference to a little program to generate subscriber profiles for an e-mail system I'm testing and how it was blowing up when trying to generate over 10k profiles. Well, like a big kid I actually managed to figure this one out for myself. I'll include a simplified version of the problem code to illustrate the point.

So the problem is that I wanted to randomly generate these user profiles, so I ended up making this data type an instance of Random which is entirely uninteresting & boilerplate code.

Now, essentially the logic for generating the list of profiles looked like, exaggerated for full effect,


import Control.Monad
import Random
filepath = "crud.csv"
generateProfiles :: Int -> IO [Int]
generateProfiles i = foldM aux [] [1..i]
                   where aux is i = do
                                sub <- randomIO                                              
                                return (sub:is) 
main = generateProfiles 10000000 >>= (writeFile filepath . unlines . map show)

Run this! Run this and weep for your feeble RAM as it is withers under the gaze of my space leak!

Alright, so this is pretty awful isn't it? It came from trying to think about the problem as "well, I want to generate 'i' many subscribers so I'm going to iterate over a list of i length, generating a subscriber each time". Bzzt, wrong. That's trying to (badly) emulate a C style for-loop in Haskell, not writing Haskell, and is a very bad idea.

Well, I took a look at this code with a fresh eye, was terrified, and then realized what would probably be a more idiomatic Haskell program: generate an infinite list of subscribers, and just write the first 'i' to a file. After all, if I'm truly being lazy then only as many as I need to write should be created. So the new approach looks something like


betterGenerate :: (RandomGen g) => g -> [Int]
betterGenerate = randoms

main = do
       std <- newStdGen  
       let subs = betterGenerate std  
       (writeFile filepath . unlines . map show . take 10000000) subs

which takes a few seconds, but doesn't eat RAM all to Hell. The main point here, for me, was to stop trying to write C# in Haskell and just write Haskell. There's probably still ways I could improve the logic of my little utility, but I can now generate 1 million subscribers, or about 120 MB of data, in roughly 2 minutes which is the upper limit of what I need.

Haskell Cafe or: How I learned to stop worrying & love laziness

2008-09-19T19:07:00.003-07:00

So as a part of my efforts to not just be so isolationist I'm starting to get code critiques on Haskell Cafe. It makes me proud, though, to be able to make grown men weep with the power of my unintentional obfuscation. Did I say proud? I meant mildly mortified.

Indeed though, the feedback was actually rather helpful and it made me realize something: I still naturally avoid laziness. I mean, I take advantage of the ability to define control structures via laziness, but relying on laziness to give you incremental processing of a file? I still find that a little scary & unintuitive. I feel like an ape trying to understand the proper uses of fire: not entirely cognizant of the proper outcome but instinctively aware that I could bring everything down in flames.

How do I overcome this? Experience I suppose. That and perhaps judiciously looking at the ghc-core output to understand what the compiler is really doing.

I actually have a slightly less trivial utility for generating fake subscriber profiles for testing an e-mail system I'm working on that, despite working in ~2 seconds for 10k profiles, exhausts its available memory after about 10 minutes when I try to generate 100k profiles. Yikes! So I'm guessing I'm misusing laziness somehow and building up a massive amount of thunks, and as Cee-Lo Green almost said "I ain't got no time to be thunkin' around". I want to try digging into the generated core, doing some profiling, and finding out what is really what before I ask h-cafe again. It'll put hair on my chest.

Predictability in APIs

2008-09-17T11:30:00.000-07:00

So this is a minor rant about something that bothers me in C# that I felt like sharing over lunch. First, I'd like to make the obligatory disclaimer that I actually like C# quite a bit. It's a close third behind Common Lisp on my list of language love.

The problem I have, though, is that functions that return objects may actually return null and that this is not reflected in the type system. I find this especially frustrating because they're so close to the right track with the nullable types.

If you ever play with LINQ to SQL you'll undoubtably come across nullable types. If your database has a column of type INT, but nulls are allowed, LINQ doesn't give you a type int for that column: it gives you type int?, which is really just the .NET equivalent of Maybe Int. You can't just willy nilly pretend you have an int when you may not because this gets caught as a type error.

Functions that return objects, on the other hand, don't do this because null is a valid assignment to any variable of an object type. This bugs the hell out of me because you can't tell just by looking at type of a function whether or not there are circumstances where it will return null instead of a 'real' object. This means that I'll either get bitten on the patootie at some point when a function I thought never returned null actually does, or I need to preemptively wrap try's around all over the place as some form of voodoo to ward off bad spirits.

My basic point is predictability. I want to be able to use a library in the most naive & dumb way as possible and still not have it blow up in my face. This is one thing I thing Haskell definitely gets right with functors such as Maybe or Either.

Reading List #1

2008-09-17T08:37:00.002-07:00

So I'm starting a weekly reading list that I'm hoping will be useful to my compadres. The first two things I'm recommending are

Chapters 1 & 2 of the awesome "What Every Programmer Should Know About Memory" though this makes for rather dense reading, at least for me, I think even just gleaning the low level picture is instructive.
The old classic "Why Functional Programming Matters" by John Hughes. It's well written, still feels relevant, & is worth reading just for the comparison of functional programmers to ascetic monks.

For my own extra reading, I'm going through the first three chapters of Koza I and the paper "Typed Contracts for Functional Programming". I'll have at least a paragraph or two to throw out there about each of these on Sunday.

Events that have occurred

2008-09-16T16:55:00.003-07:00

So a lot has happened over the past few months.

I left one job and started a new job as a programmer/data center admin at a company called Clarity Technology Group. It's a much smaller company than what I had been at & is a work environment better suited to me.
I've discovered that fresh vegetables are very helpful when you're trying to go on a diet.
I've decided to improve my >2:1 ratio of blog drafts to blog posts.
I've started writing bindings to VMWare's VIX API in Haskell.

Now as for the VIX bindings, I haven't gotten very far yet but I have to give a shout out to the writers of Real World Haskell for writing a rather excellent introductory chapter on Haskell's FFI. It's a lot less scary than I thought it would be and that's a credit to the authors. I consider teaching to be the art of making things seem as simple as they truly are, and their explanation certainly succeeds there.

Also, as a general question to the Haskellers out there: does anyone have experience calling WMI from Haskell? Are there bindings that are useful for this task?

Intro to SDL with Haskell

2008-04-01T19:37:00.003-07:00

So for awhile now I've been working on the lazyfoo tutorials using Haskell's SDL bindings.

I thought it might not be a bad idea to throw up some of the final code. Now one caveat is that I'm going to assume that if you're playing along at home that you have downloaded any materials needed for the tutorial and have it in the same directory as the executable that you're running.

I'll skip tutorial 1 because it's a little too trivial, but below is the code for the second tutorial.


> import Prelude
> import Graphics.UI.SDL as SDL

> background = "background.bmp"
> hello = "hello_world.bmp"

> main = do

The first thing we have to do is initialize the SDL subsystems. For simplicity,
I always just do init [InitEverything].


>   SDL.init [InitEverything]

Next, we create a small, vanilla, window using setVideoMode


>   setVideoMode 640 480 32 []

Since the images are just bitmaps, we can just use the straight up loadBMP functions.
loadBMP returns a surface, which is the fundamental unit for drawing in SDL.


>   image <- loadBMP hello
>   back <- loadBMP background

Next we need to grab the surface that we want to draw to.


>   screen <- getVideoSurface

And the two blitSurface commands to actually paint the contents of one surface
onto another. The arguments are the source surface, the clipping rectangle of
this surface, the target surface, and the rectangle to which you want to paint.
In both cases, Nothing represents the entire surface. That's why when painting
the background both rectangles are Nothing.


>   blitSurface back Nothing screen Nothing
>   blitSurface image Nothing screen (Just (Rect 180 140 0 0))

Finally, we need to actually draw the surface on the screen using flip.


>   SDL.flip screen

The following function uses events to make sure that the window will stay open
until you choose to close it.


>   quitHandler

> quitHandler :: IO ()
> quitHandler = do
>   e <- waitEvent
>   case e of
>     Quit -> return ()
>     otherwise -> quitHandler

Thoughts on Haskell & Performance

2008-02-05T03:40:00.000-08:00

So I'm trying to ease my way back into blogging and I thought I'd start with some thoughts I had that came from this.

Now, my current job involves analyzing performance bottlenecks for a decent sized software company & then working with the individual R&D teams to make improvements.

My point is that from my own experiences, the quality of your compiler isn't the bottleneck. It's your design.

I'm not even making the obvious point that "you choose stupid algorithms you get stupid performance". I mean that when I have found application level issues they generally have either been bugs or they have been cases where the semantics for that feature of the app aren't compatible with high performace, e.g. some screen will too eagerly load request data from the database, too aggressively do calculations that could be delayed till later in the UI, etc. I've worked this job for about a year and I haven't yet had a time when I've found that our choice of language, VB6, has been the major problem.

My conclusion is that for things that aren't numerical analysis or video games, for applications that are real "pay the bills" software, the fact that something like Haskell is slower than C just doesn't seem that relevant.

Although, now that I think about it I'm not sure if it matters for those other things either.

Exokernels & Typeclasses

2007-06-01T15:42:00.000-07:00

Blahblah sick blahblah tired blahblah giant antibiotic pills blah

Okay, so one thing that I was thinking about a long time ago when I reread the House paper was that the whole notion of the H monad, a restricted version of the IO monad meant for interacting with the OS, was really a lot like a specification of an exokernel.

I don't think the analogy is perfect, but I do think that something like the H monad combined with a plug-ins system for Haskell could actually be used to make something very similar to an exokernel with external libraries providing the real meat of normal OS abstractions to processes.

I need to think about this a bit more.

I also would like to do chunks of the book Computational Category Theory in Haskell, just to make myself sit down and really get comfortable with the way that book approaches the subject. Different takes on familiar subjects are always nice.

A couple of silly examples

2007-05-10T10:17:00.000-07:00

So having being mostly stumped on a few other ideas, I was rereading a textbook on OS design and saw that one of the exercises was to create an echo server. I thought I'd clean up one I had written in the past to learn the Network library and post it up here.


>port :: PortID
>port = PortNumber 6000

>main = withSocketsDo $ do
> sock <- listenOn port 
> handler sock

>handler :: Socket -> IO ()
>handler s = do
>  (h,_,_) <- accept s 
>  hSetBuffering h NoBuffering
>  forkIO $ echo h
>  handler s

>echo :: Handle -> IO ()
>echo h= do
>  text <- liftM (filter (/='\r')) $ hGetLine h 
>  if text=="exit"
>     then hClose h
>     else do
>          hPutStrLn h text
>          echo h
>

If you run this and telnet to localhost 6000 you should be able to see it work. Actually writing this code was very simple and felt very intuitive.

Now, that's pretty simple and a nice start: now let's say we wanted a simple server that can handle connections, creating logins, and validating logins. The problem is that now the threads need to share some kind of information, and that makes things a lot more messy; however, Software Transactional Memory makes it a bit easier.

We'll take a very silly way to store usernames and passwords, as tuples in some list.


>type Login = (String,String)

Now our actual "database" of logins will be a STM TVar of a list of logins. For those unfamiliar with STM, I really do recommend reading some of the original papers. They're rather well written and clear in motivating how one would use STM. For now, all that matters is that a TVar is a mutable object that can be accessed and modified atomically.


>type DB = TVar [Login]

>main = do
> db <- newTVarIO [] 
> sock <- listenOn port 
> handler sock db

>handler :: Socket -> DB -> IO ()
>handler s db = do
>  (h,_,_) <- accept s 
>  hSetBuffering h NoBuffering
>  forkIO $ loginServer h db
>  handler s db

>loginServer :: Handle -> DB -> IO ()
>loginServer h db = do
>  hPutStrLn h "Welcome to my server, log in or create an account:  "
>  hPutStrLn h "[0]:log in\n[1]:create account\n[2]:exit"
>  choice <- liftM (filter (/='\r')) $  hGetLine h 
>  case choice of
>    "0" -> validate h db
>    "1" -> create h db
>    "2" -> hClose h
>    _ -> loginServer h db
>
>validate :: Handle -> DB -> IO ()
>validate h db = do
>  hPutStr h "username:  "
>  name <- liftM (filter (/='\r')) $ hGetLine h 
>  hPutStr h "password:  "
>  pass <- liftM (filter (/='\r')) $ hGetLine h
>  (found,pass') <- atomically $ loginLookup name db
>  if found && (pass'==pass)
>    then hPutStrLn h "You can log in!"
>    else hPutStrLn h "Not valid."
>  loginServer h db
>             
>create :: Handle -> DB -> IO ()
>create h db = do
>  hPutStr h "username:  "
>  name <- liftM (filter (/='\r')) $ hGetLine h 
>  (found,_) <- atomically $ loginLookup name db 
>  if found
>    then hPutStrLn h "Name already in use!"
>    else do
>         hPutStr h "Choose a password:  "
>         pass <- liftM (filter (/='\r')) $ hGetLine h 
>         atomically $ pushDB name pass db
>         hPutStrLn h "Account created"
>  loginServer h db
>
>loginLookup :: String -> DB -> STM (Bool,String)
>loginLookup name db = do
>    db' <- readTVar db 
>    case lookup name db' of
>      Nothing -> return (False,"")
>      Just p -> return (True,p)
>
>pushDB :: String -> String -> DB -> STM ()
>pushDB name pass db = do
>  db' <- readTVar db 
>  writeTVar db ((name,pass):db')

Now this isn't the cleanest code, and I'm worried I may have missed some edge cases that can make it fail, but for the most part I think this is a pretty decent example of shared transactional memory combined with the Network library. The main point is that STM allows us to mostly ignore issues of how to keep everything synched together.

Arrows & Security

2007-04-19T11:14:00.000-07:00

I've been rereading an interesting paper from last year: Encoding Information Flow in Haskell.

In a nutshell, the paper is about encoding security lattices in Haskell via arrows.
To start with, I should say a few words about lattices. A lattice is, fundamentally, a set with a partial order, a least upper bound binary operator, and a greatest lower bound binary operator. I'm just going to be simple here and consider only bounded lattices where there is an actual least and greatest element for the entire lattice.

Now how does a lattice tie in with security? Well, I found that the original paper on the subject is a very good introduction, but the basic idea is that any sane arrangement of security labels that can be assigned should form a lattice. For example, if you have two security labels then you have privileges greater than or equal to either of them.

Matrioshka, our planned OS kernel, uses three lattices along with type-level capabilities to completely describe any information policy. In case it's not immediately clear why one cannot include lattice information in the capabilities, the reason is that Haskell doesn't have true dependent types so comparisons on the type level are boolean in nature. The types match or they do not. You can't examine the types and decide whether one is "greater" than the other in some sense.

Now this paper advocates using arrows as an interface to describe protected computations. Essentially, you wrap up functions with the extra data describing the lattice information and then use the standard arrows typeclasses to handle control flow and composition. I actually think it's a rather neat approach.

So the basic data structure involved is the FlowArrow

data FlowArrow l a b c = FA {
  computation :: a b c,
  flow :: Flow l,
  constraints :: [Constraint l]}

A FlowArrow is a wrapper around any other arrow type that also includes the change in lattice point for the computation and a list of constraints on the lattice generated by the composition of FlowArrows. This list of constraints is then matched against the lattice and if everything checks out the computation is unwrapped and can be executed. Pretty slick.

Of course, we can add phantom types to the FlowArrow pretty easily and thus get some representation of actual capabilities.

data CapArrow caps l a b c = CA (FlowArrow l a b c)

So now we require that for arrows to be composed together, the capabilities must be of the same type. This is where Haskell's polymorphism pays off as we can then compose arrows that have capability requirements such as

readArrow :: CapArrow (Read,d) l a b c

and

writeArrow :: CapArrow (d,Write) l a b c

if the user had possession of a resource with the proper permissions attached to it

initArrow :: Resource caps b -> CapArrow caps l a b b

Now, a lot of this is still speculation because I have no hard prototype. In terms of a system built on top of House, the underlying arrow instance would probably be Kleisli arrows for the H monad.

Science of Structure

2007-04-09T06:03:00.000-07:00

In an effort to get back in the habit of writing here, I thought I'd throw out something less technical.

One of my main interests is mathematics. Like a lot of people who love math, I end up getting the typical "oh I'm not good at math" or "I never liked math" responses when I tell people this. I try to clarify the situation by pointing out that it's not math they dislike, it's arithmetic. Arithmetic is all the algebra, long division, how-do-I-multiply-fractions business that most people associate as Math with a scary capitol M. That's not math, it's mechanism. To me, mathematics is the science of structure. It's the science that at a fundamental level tries to both abstract away phenomenon to their core essentials and illustrate the deep connections between the seemingly disparate.

Given this characterization, it probably is no surprise that my favorite branch of mathematics is category theory. I find this "abstract nonsense" to be rather inspiring in it's ability to connect ideas and concepts together, to serve as a framework for abstraction. What's more are the apparently rich ties to computer science. Haskell's monads may seem like the proverbial dead horse here, but they really are an excellent example.

I have been studying category in my spare time for several months now. My main book is MacLane's "Categories for the Working Mathematician". I think it's a very dense, but very good, book. My recommendation for study from it is to spread it out over short periods. Don't try and sit down and absorb fifty pages of this book at once, it won't work. Just read a single section, do a couple of the proofs, and then go back to something else for the rest of the day. I find it's a pretty good book to work on during lunch breaks, if your company is nice enough to give you hour long ones.

There are a few mathematical ideas that I've been kicking around lately: first, how does one generalize the notion of continuous function & homotopy to categories instead of topologic spaces. Now, I did some skimming around and found that continuous functors are defined as ones that preserve limits in a category but I realized that I'm not sure if this is just a meaningless pun or if limits in a category really do have the same meaning as limits in a topologic space. Second, is a general interest of mine in mathematical foundations of genetic programming and genetic algorithms. Not in terms of convergence and all that, but more in terms of what structure you need to have on the genotype and the transformation to phenotype in order to have a system able to evolve. For example, it seems like you need to have some sort of zipper-like structure on the genotype in order to do crossover. I haven't thought about it too much though.

Ball of MUD

2007-03-07T09:16:00.000-08:00

How would one write a MUD codebase in a functional language like Haskell, or even in a multi-paradigm language such as Common Lisp? That's something I really want to figure out, and so I'm beginning. Four-five hours per week of hacking on it should be feasible, yet allow there to be some modicum of progress each week.

I have 40-50 pages of design notes I wrote up over the fall, but haven't had time to implement any of it until now. The very first thing to do is understand how to set up some kind of very simple server that let's a user make an account and log in.

Dependent types & security

2007-02-21T12:45:00.000-08:00

During my last semester in grad school, before I left physics with a Master's, I took the graduate course on OS design. That was probably the second most fun class I ever took, second only because the professor was not an awesome old man we could call Yoda.

In any case, in this OS class I worked on a design project for a kernel written in Haskell that employs higher order types to create a static capability system. Beyond simply being a capability system, however, we wanted to encode actual secrecy and integrity levels into the type system as well and attach that data to all system resources. Of course, we ran into the limitations of even Haskell's Sexy Types(tm) and found that what we really wanted were true dependent types. Not having the time to examine the feasibility of a kernel design in Epigram, though what a kernel it would be, we ended up tagging system resources with phantom types to represent the capabilities themselves and stored the secrecy and integrity levels as actual data. We called it Matrioshka and I would love to build a real prototype on top of House in the not too distant future.

Now, the fun part is what happens when you try to express something like a capability in a dependently typed language. It turns out to be rather simple.

Let's take, as a simple example, capabilities for an arbitrary resource with only a secrecy level. This is going to be a bit of a half-baked example, because I'm still trying to digest Epigram, but hopefully it will be somewhat illustrative anyway.

So let's consider a process as just some type with an attached secrecy level. Then we should be able to evaluate whether or not we can use a read capability to a resource, and the bit of epigram code that follows allows just that.


data Nat : *  where zero : Nat ;  succ : Nat -> Nat
-------------------------------------------------
data Bool : *  where false : Bool ;  true : Bool
-------------------------------------------------
     (  x, y : Nat   !                     
let  !---------------!                     
     ! le x y : Bool )                     
                                           
     le x y <= rec x                       
     { le x y <= case x                    
       { le zero y => true                 
         le (succ x) y <= case y           
         { le (succ x) zero => false       
           le (succ x') (succ x) => le x' x
         }                                 
       }                                   
     }                                     
---------------------------------------------------
inspect le (succ zero) zero => false : Bool
---------------------------------------------------
data Read : *  where read : Read ;  illit : Read
---------------------------------------------------
     ( n : Nat ;  X : * !        (      x : X      !
data !------------------!  where !-----------------!
     !   Cap n X : *    )        ! cap x : Cap n X )
---------------------------------------------------
     (  n : Nat   !                         
data !------------!  where (---------------!
     ! Proc n : * )        ! proc : Proc n )
----------------------------------------------------
     ( p : Proc n ;  c : Cap m Read !          
let  !------------------------------!          
     !   canRead _n _m p c : Bool   )          
                                               
     canRead _ n _ m p c <= case c             
     { canRead _ n _ m p (cap c) <= case c     
       { canRead _ n _ m p (cap read) => le m n
         canRead _ n _ m p (cap illit) => false
       }                                       
     }                                         
---------------------------------------------------

Now there might be a serious question as to why one would ever want to do this. After all, if you're just analyzing the secrecy & integrity levels at runtime anyway then why not just store everything as data and forget all these fancy-pants type systems?

There are two major reasons, in my opinion, of why you would want to handle all security at the type level: first, so that you can use the type system to help prove that the system is working correctly. Second, to improve performance!

Performance is important in an OS, and by using the type system we can save quite a bit of work. First, analysis of types should be in principle faster than actually accessing data stored in the capability itself. Second, it should be possible to designate a working set of capabilities that a process can name and access securely in accordance with the secrecy and integrity lattices. After this set has been calculated once, then the kernel will no longer have to interpose itself for security checks until the working set changes again.

Hopefully, with this potential performance gain we can have our cake and eat it too when it comes to using a functional language for the kernel design. Of course, these claims remain just that until a prototype is completed. As I already alluded, House is probably going to be the most feasible system in which to implement a prototype but it will likely be quite a bit of work.

Sussman, Robustness, & Quickcheck

2007-02-19T17:38:00.000-08:00

Today on reddit there was a link to a paper by Gerald Sussman about how to construct robust systems.
If I understood correctly, his thesis is that one can only gain the robustness of biological systems by emulating their development: evolution and exploratory development. Not only that, but an emphasis on runtime tests and checks can help catch problems and further improve the strength of the system.

The idea makes a lot of sense when I think about it, but I have a feeling a lot of people who read it are going to take it as an argument for dynamically typed tools. It may have even been intended as such, but I do not presume to know the mind of Prof. Sussman.

On the other hand, I think a truly powerful type system may in fact help with exploratory programming and test-driven programming. When reading the paper I couldn't help but think of the beautiful Haskell system, QuickCheck. QuickCheck actually comes with GHC, so if you're using that compiler then you don't have to worry about installing anything else.

I actually think it'd be nice to have another example than the intro to the wiki, so I'm including my own stupid one: attempting to verify that a breadth-first search doesn't suck given that I already have some search that I know works.


>import Test.QuickCheck

>data Tree a = Node a | Branch (Tree a) a (Tree a)
>       deriving Show

So here we've defined a very simple binary tree, yay!


>dfs :: Eq a => a -> Tree a -> Bool
>dfs a (Node x) = a==x
>dfs a (Branch t x t') | x==a = True
>                      | otherwise = dfs a t || (dfs a t')

>bfs :: Eq a => a -> Tree a -> Bool
>bfs a tree = bfh tree []
>    where bfh (Node x) [] = x==a
>          bfh (Node x) (l:ls) = if x==a then True else bfh l ls
>          bfh (Branch t x t') l = if x==a 
>                                   then True 
>                                   else bfh (head l') (tail l')
>            where l' = l++[t,t']

Now we have two very simple forms of search. Let's now assume that God himself has descended and told us that our depth first search is The Awesome but we are worried that the breadth first search doesn't work. QuickCheck to the rescue!


>instance (Arbitrary a) => Arbitrary (Tree a) where
>    arbitrary = oneof [do
>                         x <- arbitrary                   
>                         return (Node x),
>                       do
>                         t <- arbitrary   
>                         t' <- arbitrary   
>                         x <- arbitrary   
>                         return (Branch t x t')]

>prop_Search t x = dfs x t ==> bfs x t

So here we've defined an instance of the Arbitrary type for our binary tree, and the property we check is that if the depth first search for a random element in a randomly generated tree is true then the breadth first search for that same element in that same tree must be true.

Of course I think we can go a lot further than this when it comes to exploratory programming and testing. I personally believe that a very strong static type system can help create a very tidy embedded language for genetic programming, but all I have are some very old toy examples on that front. Who knows how well we can do if we invoke Conor's Law?