I have seen many articles expounding on how software is not like bridge building. They attempt to reason about the problem via poorly formed analogies and often miss the actual critical differences between software development and bridge development. You will see things like the number of bolts and rivets compared to the number of lines of code. You will hear about the size of the software problem space vs. the size of the bridge builder's problem space. But none of these articles has ever hit the nail on the head for me, so I thought I would draw an apt analogy that can help both software programmers and bridge engineers understand each other.
Imagine you are a bridge engineer and have been teleported to an alternate universe to build the Golden Gate Bridge. You have things that look like beams, bolts, and welding torches. You set out to build the bridge and one day your crew finally finishes it. The first traveler gets on the bridge and drives across it, but he winds up in Des Moines, Iowa.
"What happened?" you exclaim! Your crew laughs at the traveler's predicament. "It must be a bork," they say. One of the crew goes out half way on the bridge, turns a bolt 90 degrees clockwise, and shouts back to send another driver across. Another brave traveler, dubbed "beta-tester" for some reason, sets off across the bridge and finds herself in China. The crew laughs heartily and shouts back, "Give it another spin!" With another 90 degree turn, and another brave traveler later, someone actually drives across the bridge into San Francisco as intended! There is much cheering and the sound of the popping of the Champaign floats across the ocean.
Just then, you notice a Volvo trying to drive across. You stare in awe at this strange universe wondering if the Volvo ever managed to get across. You tap one of your crew in the back and ask, "Do you think the Volvo will get to the right place?" He drops both his Champaign glass and his jaw. "VOLVO!!!!" he screams! "No, No, NO!" a crew member exclaims. "Didn't you know your world had Volvo's?" you ask. "Of course," he replies, "but we didn't think anyone would be foolish enough to try to drive it across the bridge!"
Flabbergasted, you wait for the inevitable. Half way across, the poor Volvo starts to float off the ground. It starts to spin over and over again. Horrified, you ask, "Can we make it so we can allow Volvos to drive across after we rescue that poor soul?" "Certainly," comes the reply of the crew chief, "but we'll have to raise the entire bridge by another 4 feet. We could either lift it from the bottom or just put an extra 4 feet of concrete on the surface of the bridge." You choose the latter option, saddened by the fact that your beautiful bridge now has a thick white coat of concrete to accommodate the simple Volvo.
Thinking your task has finished, you look forward to running far, far away from this universe and back into ours. You then notice 2 cars starting to drive across the bridge in tandem. A familiar feeling of dread fills you as you stammer out, "What happens if the bridge is used in parallel?" "RUN!" comes the screaming reply. No longer questioning the logic of this world, you take off. Looking back, you see a single bolt fall from the top of the bridge. As it falls, it begins to absorb the bridge itself. More and more of the bridge falls INTO the bolt. The cars, bolt, and bridge are lost forever. That is until the crew chief comes over to where the bridge was and pushes a button at the edge of the road. The bridge instantly reappears. He also posts a sign, "No driving on the bridge in parallel."
Before finally finishing with this world, you turn to ask your crew how this universe works. "It's quite simple," comes the reply. "Any bolt, beam, or other bridge part can be a bridge to any other part of the universe. It is even possible for a part to become a black hole leading to nowhere, as you saw." "Why do you build bridges then?" you ask. "We build bridges for the same reason you build bridges, because they are useful. We cannot help the fact that our universe is very strange. We envy your bridges that always lead to the same place and your parts that do not become black holes. From what you told us of your world, your software builders are in the same situation as us. Give them our sympathy and our camaraderie." With that, you return home with a far greater appreciation of what your programmer friends have to go through.
Thus ends our journey to the alternate dimension. Unfortunately for software developers, this place actually exists for us. The Halting Problem shows that we can never be certain of any result about any computation. It may run properly, it may become an endless loop, or it may give the completely wrong result. Adding concurrency adds on even more uncertainty into the situation. And we can PROVE this logically. There is no escape from the Halting Problem weirdness. Every single line of code added may blow up the bridge, dump you in China, or create a black hole.
THAT is the real bridge to programmer metaphor. And it is why software development will always be hard.
Now to help you all remember allow me to coin Gleason's Law:
"Any sufficiently complex software is indistinguishable from magic."
It is hard to even begin to learn the cutting edge of functional language theory these days without talking about monads. In languages running in a purely functional manner, monads offer a way of dealing with the outside environment in a safe and controlled manner. In a pure environment, monads provide us a way to carry data computations via pure functional composition and still have computations that happen "on the side." A lot of research into functional languages requires a solid understanding of monads and thus to apply their results to the Qi programming language, I'll define a few monad operations here and define a type theory that can handle the list monad
Since you can find a wide variety of monads for the language Haskell, I will start by describing monads in Haskell and use that to define representations inside of the Qi language. Basically, a monad is a type that defines two operations. The operations are "lift" and "pipe". In Haskell, they are often called "return" and "bind" respectively. As long at the two functions hold the following identities, we can consider the type to be a monad.
Here is a definition of the rules a monad must follow in a pure version of scheme.
(pipe (lift x) f) = (f x)
(pipe m lift) = m
(pipe (pipe m f) g) = (pipe m (lambda (x) (pipe (f x) g)))
In Haskell, the Monad m class is defined by
class Monad m where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
We can see that return "lifts" a value of type a into the monad class m a. Bind takes in a monad of type "a" and a function that takes in a value of type "a" and gives a monad of type "b". Bind then returns to us a monad of type "b" where the monad "a" has been transformed by the function into a monad of type "b". Once we have these two functions working as defined, we have a monad. Notice that we have not defined these functions yet. Haskell allows us to define a higher order type that we promise that all implementations of the type will have the listed functions and they will match the given type signatures. These sorts of definitions are not as easy in Qi, yet.
One of the basic monad types in Haskell is the list monad. We define list monads as having type Monad [] and we can make a set of functions that follow the monad laws over Monad []'s.
instance Monad [ ] where
(x:xs) >>= f = f x ++ (xs >>= f)
[] >>= f = []
return x = [x]
Let us rewrite these rules in Qi.
(define bind
[] _ -> []
[X | Xs] F -> (append (F X) (bind Xs F)))
(define return
X -> [X] )
Well that was easy! Let us try out this new monad... We'll take a list of [10 20 30] and a function that takes an X and returns [X X+1] and give it to bind to see what it does with it.
(2-) (bind [10 20 30] (/. X [ X (+ X 1) ] ) )
[10 11 20 21 30 31]
So far, so good. Let us check the monad laws to see if this version follows those laws. Law 1 says that (bind (return X) F) == (F X)
(5-) (define f X -> [ X (+ X 1) ] )
f
(6-) (bind (return 2) f)
[2 3]
(7-) (f 2)
[2 3]
Law 2 says (bind Monad return) == Monad
(8-) (bind [ 4 5 6] return)
[4 5 6]
Law 3 says that (bind (bind Monad F) G) = (bind Monad (/. X (pipe (F X) G)))
(9-) (define g X -> [ (+ X 33) (+ X 44) ] )
g
(10-) (bind (bind [10 20 30] f) g)
[43 54 44 55 53 64 54 65 63 74 64 75]
(11-) (bind [10 20 30] (/. X (bind (f X) g)))
[43 54 44 55 53 64 54 65 63 74 64 75]
So we have proven that our monad list does in fact honor the monad laws. However, we are not running the type checker in Qi on this problem, so the monad we get is the same one that we can get in any functional language. We have to wait until runtime to see the error of the following attempt at using a monad.
(14-) (bind [10 20 a] (/. X (bind (f X) g)))
1+: a is not a NUMBER
So now the question becomes, can we get a monad into the TYPED version of Qi. Firstly, we must note that Qi has no notion of polymorphic type overloading. Hence we cannot easily make a general purpose "bind" operator that all monads can use. We also should note that the type checker treats a polymorphic list as a special case, and thus we cannot perform a direct translation like the one from Haskell. In some way, we will have to contain our lists in another type.
Let us take the simplest translation. If something is of type (list A) then we can make a monadic list type of (monad list A) via the following sequent rules.
(datatype monad
X : (list A);
=====
[X] : (monad list A);
)
Monadic lists are simply lists inside of a container list and any list in a container can be a monad list of that type. We should read this as saying, "We can construct monads from lists by adding a list around it and we can construct lists from monads." We note that Qi allows you to go back from a monadic representation to the list based one as long as you properly use the type. Unfortunately, Qi has no notion of modules so we cannot seal off this behaviour from other functions in our code.
Continuing, we will define some helper functions to allow us to manipulate the monad data structure inside the instance functions. Of course, Qi has no notion of either class or instance and allows us to pull lists from monads. But if we ignore these quirks for the moment, we can define a reasonable monad list type that works. I include a constructor function "list_monad" and a few internal data access helpers.
(define list_monad
{ (list A) --> (monad list A) }
X -> [X] )
(define m_head
{ (monad list A) --> A }
X -> (head (get_list X)))
(define m_tail
{ (monad list A) --> (monad list A) }
X -> [ (tail (get_list X))] )
(define m_cons
{ A --> (monad list A) --> (monad list A) }
X [Xs]-> [(cons X Xs)])
(define join
{ (monad list (monad list A)) --> (monad list A)}
Xs -> (join-help [[]] Xs))
(define join-help
{ (monad list A) --> (monad list (monad list A)) --> (monad list A) }
Final [[]] -> [ (reverse (get_list Final)) ]
Final ML -> (let XRest (m_tail (m_head ML))
(if (= XRest [[]])
(join-help (m_cons (m_head (m_head ML)) Final)
(m_tail ML))
(join-help (m_cons (m_head (m_head ML)) Final)
(m_cons (m_tail (m_head ML)) (m_tail ML))) )))
Our m_ functions and join properly deal with getting (list A)'s from their containers and putting them back in. Join has to take the job of flatten and check for the end of a list and if we find it, drop it from the "Final" list. This accounts for the if statement in the function. It obviously makes heavy use of the data manipulation functions which lowers legability. We can read it as saying, "Take the first element head of the list (remember that we have a monad list of a monad lists here) and put it on the final list. Then take the rest of that head list and put it back on the processing queue. The Final output list is built in reverse order so we are forced to reverse the computation at the end of the join. Not pretty, but it works for the purpose of monad construction.
Now we are in a position to define "bind" and "return" as before.
(define bind
{ (monad list A) --> ( A --> (monad list B)) --> (monad list B) }
XS F -> (join [(map F (get_list XS)) ]))
(define return
{ A --> (monad list A) }
X -> [[X]]
)
Note that we basically take the list out of the monad container and apply normal list functions to it, wrapping it up back in the monad container when we return.
Testing it out gives:
(14+) (bind (list_monad [10 20 30]) (/. X (list_monad [X (+ X 1)]) ))
[[10 11 20 21 30 31]] : (monad list number)
And our monad type is certainly not a list
(31+) (head (bind (list_monad [4 5 6]) return))
error: type error
Now let us assure ourselves that our monad list is polymorphic to type A. We now define a fractal symbol function f.
(36+) (define f
{ symbol --> (monad list symbol) }
X -> (list_monad [ x o x]) where (= X x)
_ -> (list_monad [ o o o]))
And let us use it with our monad functions
(37+) (bind (return x) f)
[[x o x]] : (monad list symbol)
(38+) (bind (bind (return x) f) f)
[[x o x o o o x o x]] : (monad list symbol)
(39+) (bind (bind (bind (return x) f) f) f)
[[x o x o o o x o x o o o o o o o o o x o x o o o x o x]] : (monad list symbol)
So there you have it, a very simple, poorly performing basic list monad of polymorphic type A in the Qi Programming Language. Feel free to offer any questions or criticism that you have. Thanks for reading.
