Fear of releasing code

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.

Debugging & Refactoring, a mid-mortum

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

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

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

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

So two quick notes:

1. 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.
2. 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

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.

Some first steps with Data.Reactive

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

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

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

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

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.

Thoughts on Haskell & Performance

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.

A couple of silly examples

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

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.

Dependent types & security

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

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?