Skip to content
August 23, 2011 / cdsmith

Haskell For Kids: My Project!

Oops!  I almost forgot to do my own homework from my Haskell for Kids class!

Here’s the program I wrote (intentionally using only the features we’d already talked about in class.)

import Graphics.Gloss

picture = pictures [
    color lightGray (rectangleSolid 500 500),
    translate  0 (-75) (color darkGray mouse),
    translate 90 (150) thoughtBubble
    ]

darkGray = light black
lightGray = dark white

thoughtBubble = pictures [
                            (scale 100 50 filledCircle),
    translate ( -85) ( -15) (scale 0.4 0.4 (text "I wonder...")),
    translate ( -85) ( -65) (scale 20 20 filledCircle),
    translate (-120) (-110) (scale 15 15 filledCircle)
    ]

filledCircle = pictures [
    color white (circleSolid 1),
    color black (circle 1)
    ]

mouse = pictures [
    scale 2   1 (circleSolid 50),
    translate (-100) ( 40) mouseHead,
    translate ( 120) (-20) mouseTail,
    translate ( -40) (-55) mouseLegs,
    translate (  20) (-55) mouseLegs
    ]

mouseHead = pictures [
    translate 20 35 (color rose (circleSolid 20)),
    translate 20 35 (thickCircle 5 40),
    rotate (-10) (scale 1.5 1 (circleSolid 40))
    ]

mouseTail = (rotate (-15) (rectangleSolid 100 5))

mouseLegs = pictures [
    rectangleSolid 5 35,
    translate 20 0 (rotate 10 (rectangleSolid 5 35))
    ]

And the result:

August 23, 2011 / cdsmith

Haskell for Kids: Week 2!

It’s time for the second weekly roundup from my Haskell programming class for kids!  (Here’s a link to last week’s.)

Pictures From Last Week

Remember, last week’s assignment was to write a program to draw an involved picture about something of your choosing.  Here are some of the results:

This Week: Organization

The theme for this week is organization.  One problem that’s easy to run into quickly in computer programming is that you write computer programs that are so involved and complicated that you get stuck: the program might even work, but it’s so hard to understand that you dread having to change it!  We spent some time talking about ways to organize your computer programs to make them easier to read.

Parts of a Program

Just to review, a computer program that you wrote on the first day of class might look like this:

import Graphics.Gloss

picture = color red (pictures [ circle 80, translate 50 100 (rectangleSolid 100 50) ])

We looked a little closer at how programs are built during our second class last week.  Here are the parts.

Import Statement

The first line is the import statement: remember that’s where we tell the computer that we will be using the Gloss library.  If it weren’t for that line, then the computer would have no idea what words like color, red, pictures, circle, and so on actually mean!  You only have to import a library once, no matter how many times you use the things that it defines.

Definitions

After the import statement, your program defines some new words, called variables.  The one variable we defined in the program earlier was picture.  For the moment, we always define a variable called picture, because that’s how the computer knows what to draw.  What we didn’t mention in my last post, though, is that you can define other variables besides picture!  And when you do, you can use them in the same way you could use circle or other built-in picture types.

For example, look at this program:

import Graphics.Gloss

picture = snowman

snowman = pictures [
    translate 0 ( 50) top,
    translate 0 (  0) middle,
    translate 0 (-75) bottom
    ]

top    = circleSolid 50
middle = circleSolid 70
bottom = circleSolid 90

This program defines five variables: picture, snowman, top, middle, and bottom.  Again, the computer is only going to draw the thing labeled picture, but the other variables are useful for keeping things organized.  There are two important rules here, which are part of the programming language, Haskell:

  1. Each new definition has to start in the left-hand column.  It should not be indented.
  2. If you start a new line in the same definition, you have to indent it.  It doesn’t matter how far, but you need to indent at least a little.

It came up that I’m defining picture first, and then snowman, and so on… some people thought it would make more sense to do it in the other order.  That’s fine!  The order of your definitions makes no difference at all, so feel free to start with picture and work your way down to the parts (sometimes called “top down”, or to start with the parts and work your way up to the overall picture (sometimes called “bottom up”), in whatever way makes sense to you.  You could even put them in alphabetical order.  The computer doesn’t care.  (I don’t actually recommend alphabetical order… but you could!)

Expressions

The parts after the equal sign (=) in your definitions are called expressions.  This is where you say what the variables actually mean.  Most of what we looked at last week had to do with the different kinds of expressions you can put there: circles, rectangles, and so on, and even some more complicated expressions involving color or translate and so on.

In our second class last week we said a little bit more about what an expression is.  Look at this example:

picture = translate 10 20 (circleSolid 50)

The expression on the right side of the definition of picture has four parts to it, all written next to each other.  When you see something like that, the first part is called a function, and then rest of them are called parameters.  So here we have:

  1. translate – That’s the function
  2. 10 – That’s the first parameter
  3. 20 – That’s the second parameter
  4. (circleSolid 50) – That whole thing is the third parameter

Pay attention to the parentheses!  Parentheses mean “treat this whole part here as just one thing”.

Every function expects a certain number of parameters.  For example, translate always expects three: the first is how far to move horizontally, the second is how far to move vertically.  The third is the picture that you’re moving.  If you tried to give it only 2 parameters, or 5 parameters, it won’t work!  (If you want to, try it and see what happens.)

What about the part inside the parentheses?  It’s just another expression!  Can you identify which part of it is the function, and which are parameters?

There’s one other piece: you might notice that pictures is a bit different.  The piece that comes after pictures has square brackets around it, and you can have as many things in there as you like, with commas between them.  That’s just another kind of expression, called a list.  So far, pictures is the only thing we’ve seen that uses lists, but we’ll see another one soon!

Here’s the whiteboard after we discussed the parts of a program and expressions:

The conversation bubble was a different discussion: we talked about how you can make interesting shapes by drawing in white over the top of another shape.

Some Advice

Most of that was from the second class last week.  This week, we spent some time talking about good advice for writing computer programs.  We came up with the following:

Be Fanatical about Organization

If you don’t stay organized, it’s just not possible to write interesting computer programs.  Your programs should be designed out of pieces, and you should pick those pieces to be meaningful.  Here’s an example of what not to write:

import Graphics.Gloss
pictures = [
    translate 71 123 (rectangleSolid 30 200),
    rotate 45 (translate 10 1 (color green (circle 50))),
    translate 100 100 (scale 2 2 (rectangleWire 10 10)),

… and on, and on, and on …

That’s okay to do when you’re trying things out or playing around.  But eventually, you want to break up your program into manageable pieces!  A long list of 40 different drawing operations isn’t very fun to read, and it definitely isn’t fun to try to make changes to later on.

Instead, try to do something like the snowman example earlier: the pieces of the snowman are broken down into smaller pieces, so you can think about one thing at a time.  Of course, not just any pieces will do!  You don’t want one piece to have the grass and one leg and sun, and then then next piece to have another leg and a tree!  Try to find pieces of your picture that make sense on their own.  Computer programmers even have a fancy word for that: we call those pieces coherent or we say that they have a lot of cohesion.

Earlier, we mentioned the ideas of “top down” and “bottom up” approaches to programming: you can either start by defining picture, and then define its pieces… or you can start by defining the pieces, and then build bigger things out of them.  For now, whichever direction you find easier is okay, but just pay attention to which one you’re doing, and maybe taking the opposite approach once in a while will make certain things easier.

Be a Good Communicator

The second piece of advice we talked about is to be a good communicator.  You’re not just writing a computer program for the computer to run it: you’re also writing something for other people to read.  You might show your programs to other people in the class, or to teachers, or plenty of other people.

A really good way to communicate well is to pick good names for things.  If you’re drawing a flower, your program will be a lot easier to understand when your variables are called leaf, stem, and petal; not picture1, picture2, and picture3!

Another tool you can use that’s helpful for communicating well is called comments.  The computer will ignore any part of your program that’s between a {- and a matching -}.  (That’s an open curly brace following immediately by a dash… and then a dash followed by a closing curly brace.)  For shorter comments, the computer will ignore anything from  (two dashes in a row) to the end of the line.  So you can write something like this:

{-
    Picture of my dog, by Chris Smith

    This is a picture of my dog, Ruby.  She is part border collie.
-}

picture = pictures [
    circleSolid 50,       -- That's her body
    rectangleSolid 20 100 -- That's her tail
    ]

(No, that doesn’t really look much like a dog… gimme a break, it was just a quick example!)

By picking good names and adding comments to explain what you’re doing, you can make your programs a lot easier to read and understand, both for yourself and other people.  That’s what we mean by being a good communicator.

Hide Unimportant Ideas

There’s only so much that one person can remember at a time!  Because of that, another important idea in computer programming is to hide the stuff that isn’t important, so that you can focus on what is.

We talked about a new language feature that helps here, and that is let and where.  Here’s ax example of using where in a program.

import Graphics.Gloss

picture = snowman

snowman = pictures [
    translate 0 ( 50) top,
    translate 0 (  0) middle,
    translate 0 (-75) bottom
    ]
  where
    top    = circleSolid 50
    middle = circleSolid 70
    bottom = circleSolid 90

That is almost the same snowman program as before: but with one difference.  The variables top, middle, and bottom are defined after the word where, and still inside the definition of snowman.  (It might not be obvious here, but the word where is still indented by a few spaces, so it’s still part of the definition of snowman.

What this does is make top and middle and bottom only mean something inside of the definition of snowman.  So you can use them when you’re defining snowman, but if you tried to use them in a different part of your program, it wouldn’t work.  The error message you’d get would say “not in scope”.

The idea of scope is important in computer programming.  The scope of a variable is how much of the program it can be used in.  When you write more involved programs, you don’t want every single variable that you define to be visible everywhere!  As this snowman program gets bigger, maybe we might want the same name, like top, to mean something completely different when we’re drawing a different part of the scene.  That’s okay, because this top is only “in scope” during the definition of snowman.

We talked about an analogy for this: if you’re in England, it makes perfect sense to say “I saw the queen today!”  But, if you’re in the United States, it doesn’t make sense any more, because we don’t have a queen.  The phrase “the queen” means something different depending on where you are!  So if I talked like the Haskell programming language, and you said to me “I saw the queen today!”, I might say in response, “Not in scope: the queen”.

By the way, here’s the way to write that same snowman program but using let instead of where.

import Graphics.Gloss

picture = snowman

snowman =
    let top    = circleSolid 50
        middle = circleSolid 70
        bottom = circleSolid 90
    in  pictures [
            translate 0 ( 50) top,
            translate 0 (  0) middle,
            translate 0 (-75) bottom
            ]

This means exactly the same thing: you just get the choice between defining the pieces first (that’s let) or defining the pieces afterward (that’s where).

Pay Attention To Details

Finally, the last piece of advice we had for computer programming was to pay close attention to details.  There are lots of situations where a normal person might be able to figure out what you want, but your computer program still won’t work if you don’t get all the details right!

We looked at some of these details more closely:

  • Indentation:  You are not allowed to indent the first line of a definition.  You must indent every line after that.  These are rules in the Haskell programming language; if you don’t follow them, your programs won’t work.  Also, if you use let and where, then you have to indent all the definitions there by the same amount.
  • Parentheses: A lot of people have trouble with this when they get started with programming.  (For that matter, most of us still make mistakes with parentheses even when we’ve been programming for years!)  You have to match up your opening and closing parentheses, or your program just won’t work.We talked about a few things that help.  Some programming tools, including the web site we’re using right now, will help you match up parentheses by pointing them out.  Using the web site, try putting your cursor right after a parenthesis: the matching one will have a gray box drawn around it!  This can help a lot… but it’s only there if the tool you’re using happens to do it.We also talked about counting parentheses.  There’s a trick most programmers figure out for checking their parentheses: start out with the number 0 in your head, and then read through part of your program, and add one every time you see an open parenthesis, and subtract one every time you see a close parenthesis.  If everything matches, you’ll end up back at zero at the end!  If not, you may need to figure out where you’re missing a parenthesis.
  • Spelling: If you misspell a word, it won’t work!  So paying attention to spelling is important.
  • Capitalization:  Whether words are capitalized or not matters!  So, for example, red works fine as a color, but Red doesn’t work!  We talked about the convention of capitalizing new words inside a variable name, even through the variable name starts in lower case, like in circleSolid.  That has a name: “camel case”… because it’s sort of like upper-case or lower-case, except it has a hump in the middle.
  • Spaces: Most of the time, you can put spaces in your program however you like: but they often do need to be there!  You can’t run together numbers or variable names and expect it to work.  A lot of programmers like to use spaces to line things up in nice columns, too.

Here’s our whiteboard at the end of this part:

Paying attention to details like this is very important, and will help a lot as you get more experience with writing programs.

Things Other People Said

We finished up today by reading some quotations by famous people about computer programming, talking about, and did some laughing, too.

Any fool can write programs that a computer can understand.  Good programmers write code that humans can understand.

- Martin Fowler

This is talking about the importance of being a good communicator, which was one of the points above.

Controlling complexity is the essence of computer programming.

- Brian Kernighan

Brian Kernighan was one of two people who invented C, one of the most popular programming languages in the world.  He’s talking here about the important of organization, and of hiding unnecessary details, so that you can build programs without being overwhelmed by how complicated everything gets!  In fact, he says that’s the most important thing about computer programming.

Any sufficiently advanced bug is indistinguishable from a feature.

- Rich Kulawiec

Remember a “bug” is a mistake in your program.  A “feature” is something it does, and is supposed to do.  I threw this quotation in for Sophia, because on the first day of class, she found a bug in my web site where you could stretch a solid circle and it would accidentally leave a hole in the middle, and she used it to make a mouth as part of her first program.  But then the next day, I fixed the bug and broke her program!  That’s definitely a bug that turned into a feature.

If you’re about to add a comment, ask yourself, “How can I improve the code so that this comment isn’t needed?”

- Steve McConnell

This is a great concept!  We talked about using comments to explain what’s happening in your programs: but what’s even better than having a comment is organizing your program so that it’s obvious what you’re doing, and you don’t need the comment any more.  This certainly doesn’t mean never write comments: it just means see if you can keep things simple so there’s not as much to explain.

Great software, likewise, requires a fanatical devotion to beauty.  If you look inside good software, you find that the parts no one is ever supposed to see are beautiful, too.  I’m not claiming I write great software, but I know that when it comes to code, I behave in a way that would make me eligible for prescription drugs if I approached everyday life the same way.  It drives me crazy to see code that’s badly indented, or that uses ugly variable names.

- Paul Graham

This is Paul Graham being funny, but also making a very good point.  This touches on the first and last points of advice earlier.

There are two ways of writing computer programs: One way is to make it so simple that there are obviously no mistakes.  The other way is to make it so complicated that there are no obvious mistakes.

- C.A.R. Hoare (sort of)

The last one is actually slightly misquoted.  I didn’t correct it because the original version means nearly the same thing but uses more technical language.

Your Assignment

Your assignment is to clean up your computer program!  Imagine that you’re going to share with other people not just the picture it draws, but the computer program itself.  Get it as clean and nice looking as you can: try to break things down in logical ways, pick really good names, fix all the details, and communicate well to people reading your code.

See you next week!

August 20, 2011 / cdsmith

Animations Added to Web-Based Haskell/Gloss

The Feature

I’ve added animations to the web-based Gloss/Haskell environment at http://dac4.designacourse.com:8000/anim.  You should export a symbol

animation :: Float -> Picture

and you’ll see it in modern web browsers.  By “modern” we mean:

  • Firefox 6.0 or higher (yes, the one released just a couple days ago)
  • Chrome, Safari, or Opera, any recent version
  • The iOS browser should work (untested).
  • Internet Explorer and the built-in Android browser are known not to work.  On both operating systems, Firefox 6 is available and does work.

The feature we need is called “server sent events”, an HTML 5 extension that makes “comet” style web applications work without a whole tool shed of browser-specific kludges.  So, if you are curious about another browser, see if it implements server-sent events.  Or just try it.

Edit: As of Sunday, you can now do “simulations” as well.  The URL for simulations is http://dac4.designacourse.com:8000/sim.  These are a little more involved.  You need to define three symbols sharing a common data type of your choosing:

initial :: StdGen -> a
step :: ViewPort -> Float -> a -> a
draw :: a -> Picture

Here, initial returns the starting value of your chosen data type.  (Its parameter is a pseudo-random number generator, in case you want random numbers.)  The step function is responsible for “advancing” the simulation by some amount of time.  Finally, the draw function is reponsible for converting the current simulation to a picture to draw on the screen.  The difference between simulations and animations is that animations calculate the picture from scratch each time: you give it a time since the start, and get back a picture.  Simulations, on the other hand, play out incrementally: each new state depends only on the most recent state and the amount of time that’s passed since then.  You can always turn an animation into a simulation by defining initial = 0 and step = const (+) where the type “a” is Float.  But not all simulations can be efficiently written as animations.

Under the Hood

The previous version of the application (which still works just fine) displayed only static pictures, and did so by loading some JSON directly into the document and then having JavaScript draw it on a canvas.  This new animation mode is a little different.  The steps are:

  1. You submit your function.
  2. The server compiles your code (using SafeHaskell, of course), and stores your function along with the start time in a lookup table.
  3. The animation page loads, and has a key to that lookup table.
  4. The animation page connects back to the server using the JavaScript EventSource object (that’s the server-sent events feature).
  5. The server then streams newly updated pictures as JSON along that connection.

Incidentally, if you’re thinking of implementing a “comet”-style web application with Snap, you might be interested in the code at https://github.com/cdsmith/gloss-web/blob/master/src/EventStream.hs which implements the server side of the event stream format.  It’s a generic module that you can transplant into your own code.  In the future, I’ll look at the best way to get it packaged either as part of a snap package or as a stand-alone library.  As short as it is, though, I hope to avoid adding that dependency weight.

Anyway, that’s animations for you.  Have fun!

Examples

The following program draws the solar system, representing the distances of all the planets from the sun, their orbital periods, their relative sizes.  The one thing that’s not accurate is the relationship between the sizes of the planets and their distance from the sun… something had to give, since a completely to-scale representation of the solar system would just look empty!  Also, I didn’t bother representing the eccentricities of orbits.

import Graphics.Gloss

animation t = pictures [
    color black (rectangleSolid 500 500),
    sun,
    rotate (60 * t /   0.24) (translate   4 0 mercury),
    rotate (60 * t /   0.62) (translate   7 0 venus),
    rotate (60 * t /   1.00) (translate   9 0 earth),
    rotate (60 * t /   1.88) (translate  14 0 mars),
    rotate (60 * t /  11.86) (translate  48 0 jupiter),
    rotate (60 * t /  29.46) (translate  89 0 saturn),
    rotate (60 * t /  84.32) (translate 178 0 uranus),
    rotate (60 * t / 164.80) (translate 279 0 neptune)
    ]

sun     = color orange         (circle 69)
mercury = color (dark white)   (circle 0.25)
venus   = color (light yellow) (circle 0.6)
earth   = color (light blue)   (circle 0.63)
mars    = color (dark orange)  (circle 0.34)
jupiter = color (light orange) (circle 7.1)
saturn  = color (light yellow) (circle 6.0)
uranus  = color azure          (circle 2.6)
neptune = color blue           (circle 2.5)

Here’s the tree example from the the gloss-examples package.  Unfortunately, it pegs the server’s CPU at 50%… so I’ll have to work on what’s making it run so slowly.

import Graphics.Gloss

animation :: Float -> Picture
animation time
	= Scale 0.8 0.8 $ Translate 0 (-300)
	$ tree 4 time (dim $ dim brown)

-- Basic stump shape
stump :: Color -> Picture
stump color
	= Color color
	$ Polygon [(30,0), (15,300), (-15,300), (-30,0)]

-- Make a tree fractal.
tree 	:: Int 		-- Fractal degree
	-> Float	-- time
	-> Color 	-- Color for the stump
	-> Picture

tree 0 time color = stump color
tree n time color
 = let	smallTree
		= Rotate (sin time)
		$ Scale 0.5 0.5
		$ tree (n-1) (- time) (greener color)
   in	Pictures
		[ stump color
		, Translate 0 300 $ smallTree
		, Translate 0 240 $ Rotate 20	 smallTree
		, Translate 0 180 $ Rotate (-20) smallTree
		, Translate 0 120 $ Rotate 40 	 smallTree
		, Translate 0  60 $ Rotate (-40) smallTree ]

-- A starting colour for the stump
brown :: Color
brown =  makeColor8 139 100 35  255

-- Make this color a little greener
greener :: Color -> Color
greener c = mixColors 1 10 green c
August 16, 2011 / cdsmith

Haskell For Kids: Week 1!

And We’re Off!

Thanks again to everyone that’s supported this project and stepped up to be a part of it.  Today, I taught my first in-person class on Haskell, and it was a blast!  This is my first weekly summary post, containing what we’re doing this week.

First: Introductions

Since there are a number of kids following along with this, let’s all get started with some introductions!

  • Me: My name is Chris Smith, and I’m teaching the in-person programming class at Little School on Vermijo that got all of this started.  I’m a huge fan of Haskell, and am really excited to be able to share that with new people!

  • Sue: Sue Spengler is the “founder, lead teacher, principal, superindendent, custodian, secretary, and lunch lady” for the Little School on Vermijo.  The school is her project, and she’s doing some pretty amazing things.  I had to poke around a bit for a photo, so I hope she likes this one!
  • My local students: The kids in my class today were Grant, Sophia, Marcello, and Evie (I hope I spelled that right!)  I’ll ask them to introduce themselves in comments on this post, so look for them there!
  • Everyone else: Any other kids who are taking the class, please use the comments to introduce yourselves as well!  You can say hello, and if you like, you can even link to a video or  picture.

I hope everyone takes the time to leave comments and say hello to each other.  Learning things is a lot more fun when you talk to other people.

The Plan

We talked about where we’re going, including:

  1. Write computer programs to draw pictures.
  2. Change our computer programs so the pictures move!
  3. Build a game of your own choosing.

This will take the school year!  That’s because this class isn’t just about memorizing some thing about a particular computer program: it’s about being creative, trying things, and doing something you’re proud of.  So there will be a lot of free time to play around and try out different ideas in your programs.  We are learning the Haskell programming language, but in the end, the class is more about being in control of your computer and designing and building something really cool from scratch, not just remembering some stuff about Haskell.

Organization of Computers and Programming

The first thing we talked about was what a computer program is, and how some of the ideas fit together.  Here’s the whiteboard when we were done!

Some of the ideas we talked about:

  • How a computer works.  The main part of a computer is built from a device for following instructions (the “CPU”), and a device for remembering information (“memory”).
  • Machine language.  The computer doesn’t speak English, of course!  It follows instructions in a language called “machine language”.  This language is easy for the computer to understand, but it’s very, very difficult to write programs in.
  • Compilers.  Instead of writing our programs in machine language, we write them in other languages, and then get the computer to translate them for us!  The program that does that is called a compiler.
  •  Some programming languages.  We have a choice what programming language to use when writing computer programs!  We brainstormed some languages kids in the class had heard about: Java, C, C++, Objective C, JavaScript, Java, and Smalltalk.  (Yes, Marcello had heard of Smalltalk!  I’m very impressed.)  The language we’re learning in this class is called Haskell.
  • Libraries.  Libraries are pieces of programs that other people have written for us, so we don’t have to start from scratch.  We spent some time imagining all of the steps involved what we might consider very easy things to do with a computer.  For example, thing of all the little steps in drawing a window… how many circles, rectangles, lines, letters, and so on can you find in a window on your computer?  Libraries let someone describe things once instead of making you repeat all that each time.

We talked about how we’ll be using:

  1. A programming language called Haskell.
  2. A library called Gloss.

Playing Around

At this point, we all used a web site to write some simple computer programs using Haskell and Gloss.  The web site is:

http://dac4.designacourse.com:8000/

We started out with some really simple programs, like these:

Draw a circle!

import Graphics.Gloss
picture = circle 80

Draw a rectangle!

import Graphics.Gloss
picture = rectangleSolid 200 300

Draw some words!

import Graphics.Gloss
picture = text "Hello"

All of these programs have some things in common:

  • The first line of each one is “import Graphics.Gloss”.  This tells the compiler that you want to use the Gloss library to make pictures.  You only need to say it once, and it has to be at the very beginning of your program.
  • They all then go on to say “picture = …”.  That’s because the way our programs work is to make a picture, and call it “picture”.  The web site we’re using then takes that picture, whatever we define it to be, and draws it for us.  We talked about how in the future, we might define other things with other names, but for now, we’re okay with just telling the compiler what “picture” is.
  • After the “=”, they describe the picture that we want to draw.  There are several types of pictures, and we’ve just seen three of them!  All of the kinds of pictures you can create are part of the Gloss library.
  • Except for the last one, they all use some distances.  For example, the 80 in the first example is the radius of the circle (the distance from the middle to the outside).  You can make that number larger to draw a bigger circle, and smaller to draw a smaller circle.  You can do the same with the width and height of the rectangle.

We did have problems with some people using the web site.  If you’re having trouble, you might need to make sure you have a new version of your web browser.  Also, the web site doesn’t work with Internet Explorer… so try with Chrome, Firefox, Opera, or Safari.  Don’t worry too much about the web browser problems: soon enough, you’ll install the Haskell compiler on your own computer, and you won’t need the web site to run your programs any more!  We’re just using the web site to get started quickly.

Drawing more than one thing!

By this time, several kids were asking if they can draw more than one shape at a time.  Yes, you can!  To draw more than one thing, you can use “pictures” (notice the s at the end).  For example,

import Graphics.Gloss
picture = pictures [
    circle 80,
    rectangleWire 200 100 ]

Notice we do this:

  • The word “pictures”
  • An opening square bracket.
  • A list of the pictures we want to draw, separated by commas.
  • A closing square bracket.

We talked about how it helps to make new lines in your program sometimes.  The only think you need to be careful of is that when you make a new line, you have to put a few spaces at the beginning to indent it.  See how the second and third lines of the part where we define “picture” are indented a little?

Changing your pictures

The Gloss library gives you some ways you can change your pictures, too!

You can change the colors with “color”.

import Graphics.Gloss
picture = color red (circleSolid 80)

Notice how you say “color”, then the name of the color you want, and then the picture to draw, in parentheses.  The parentheses are important!  They mean the same thing they do in math: treat that whole part as a single “thing” (in this case, a picture).

We talked about what colors Gloss knows about.  Here’s the list: black, white, red, green, blue, yellow, magenta, cyan, rose, orange, chartreuse, aquamarine, azure, and violet.  We all laughed because Sue picked a weird color name off the top of her head, and asked “Does it know chartreuse?”  Yes, it does.  Lucky guess!

You can also move things around on the screen.

import Graphics.Gloss
picture = translate 100 50 (rectangleSolid 50 50)

When you want to move things around, Gloss calls that “translate”.  Yes, it’s a weird name, but “translate” just means move something left, right, up, or down.  The first number after translate is how far to move it to the side.  Positive numbers mean right, negative numbers mean left, just like a number line!  The second number is how far to move it up or down.  Positive numbers mean up, and negative numbers mean down.

Keep in mind that in Haskell, you have to write negative numbers in parentheses!  If you say “translate -100 …”, then Haskell thinks you want to subtract one hundred from “translate”.  It doesn’t know how to subtract a number from a verb (I don’t either) so it gives up!  You have to write “translate (-100) …” instead, with the parentheses.

You can also turn things.  The verb for that is “rotate”.  Let’s draw a diamond.

import Graphics.Gloss
picture = rotate 45 (rectangleWire 100 100)

You rotate things in degrees.  Remember that 360 degrees means turn it all the way around to where it started, so it won’t do anything!  45 degrees is half of a right angle.  Do you see why that gives you a diamond?

The last thing you can do is stretch the picture.  The verb for that is “scale”.

import Graphics.Gloss
picture = scale 2 1 (circle 100)

That will draw an ellipse, which is like a circle but it’s wider than it is tall!

Don’t worry if this all doesn’t make sense yet!  We’ll be spending a lot of time playing around with how to put these things together!  Here’s the whiteboard after we finished all of this…

Time for Experimentation

We spent a lot of time with everyone making their own shapes and pictures of whatever they want.  The best way to get more comfortable with all of this is to play around.  Make lots of little changes and see what happens!  Try to guess what’s going to happen, then try it and see if you’re right or wrong.

Here are some pictures of the kids with their projects:

Sophia and Evie showing off two circles side by side.  These eventually became the eyes in a face!

That’s Grant with his diamond.  It looked even better after he stretched it a little bit up and down.

This was Marcello’s graphics… centering the word in the circle was a long task!  If you try it, you’ll notice text doesn’t get normally drawn right in the middle like other pictures do, so Marcello put in a lot of trial and error time with “translate” to put the word in the circle.

That’s Sophia being very excited at getting her two eyes in the right places!

Your Assignment

Your mission, if you choose to accept it… is to plan and create a drawing of something you’re interested in!  Maybe it’s a fish, a garden, a space station, or a dragon… just make sure you can draw it by using rectangles and circles of different colors, and moving, turning, or stretching them.  Here at the Little School, we’ll be spending our remaining class this week and our classes next week working on this.  Spend some time and come up with something you’re proud of!

August 15, 2011 / cdsmith

Haskell For Kids: Web-Based Environment Goes Public!

Last time, I described my work on a web-based programming environment for Haskell and Gloss, which is available from github as the gloss-web project.  Now you can try it online without having to install it yourself!  Here’s the URL:

http://dac4.designacourse.com:8000/

It seems to work fine at least with Chrome, Firefox, and Safari on Linux and Windows.  Internet Explorer (even 9) is known NOT to work.

What’s New

I’ve made a few changes to the code and fixed a number of bugs from Sunday’s late-night coding sprint, but the biggest change was to enable use of the SafeHaskell extension.  It’s now impossible to circumvent the type system and run arbitrary code on the server.  Evidence:

Note that there are still no resource or CPU time limits, so there are no protections against writing infinite loops or infinite data structures, so it’s still possible to use the server to run a denial of service attack against itself.  Please don’t do that.  I already know you can, and it’s really just not cool.  I’ve installed the server on a dedicated otherwise-empty machine I set up and installed for this purpose, so the only people you’ll really be hurting are other programmers like yourself who want to try this demo.

Want a non-trivial example to try it with?  Your wish is my command; here’s the simple one I’ve been playing around with as I develop the server:

{- This is my wagon -}

import Graphics.Gloss.Data.Picture
import Graphics.Gloss.Data.Color

picture = pictures [
    blank,
    color brown (translate (-60) (-80) wheel),
    color brown (translate ( 60) (-80) wheel),
    color black (translate (100) ( 75) (rotate 45 handle)),
    color red body
    ]

brown = dark (dark (dark orange))

wheel = pictures [
    rotate   0 spoke,
    rotate  45 spoke,
    rotate  90 spoke,
    rotate 135 spoke,
    rim
    ]

spoke = rectangleSolid 10 70

rim   = thickCircle 35 15

body  = rectangleSolid 200 100

handle = pictures [ rectangleSolid 100 10,
                    translate 50 0 (rectangleSolid 10 30) ]

Edit: Here’s something a little less trivial: a recursive drawing of a Koch snowflake.

import Graphics.Gloss

picture = kochSnowflake 4

kochSnowflake n = pictures [
    rotate   0 (translate 0 (-sqrt 3 * 100 / 6) (kochLine 100 n)),
    rotate 120 (translate 0 (-sqrt 3 * 100 / 6) (kochLine 100 n)),
    rotate 240 (translate 0 (-sqrt 3 * 100 / 6) (kochLine 100 n))
    ]

kochLine k 0 = line [(-k/2, 0), (k/2, 0) ]
kochLine k n = pictures [
    translate ( k/3) 0 (kochLine (k/3) (n-1)),
    translate (-k/3) 0 (kochLine (k/3) (n-1)),
    translate (-k/12) (-sqrt 3 * k/12) (rotate 300 (kochLine (k/3) (n-1))),
    translate ( k/12) (-sqrt 3 * k/12) (rotate  60 (kochLine (k/3) (n-1)))
    ]

You can find complete documentation for the gloss package, of course, at http://hackage.haskell.org/package/gloss.  Note that the server currently only implements the equivalent of displayInWindow, and rather than using the I/O action (which you can’t do, since SafeHaskell won’t let you do anything but purely functional code), you just define a top-level symbol called “picture” in your module.

Thoughts on SafeHaskell

Overall, I’m thrilled to have the SafeHaskell stuff in GHC.  It just has so many potential uses… it’s Java-style sandboxing, but at compile time!

There is one thing that confuses me, though… in order to get this working, I had to patch the gloss library to add “Trustworthy” declarations.  This is not ideal, for two reasons:

  • There are plenty of Haskell modules out there that GHC could easily prove are safe: if nothing else, just try to build them with the Safe extension, and if it fails, try again without it.  The vast, vast majority of Haskell packages would pass this test, and become available for use in safe code.  But that doesn’t seem to be what happens.  A module isn’t considered safe unless it’s explicitly specified to be safe, at compile time.  That greatly reduces the amount of code it’s possible to use from safe code, and sets up a huge obstacle in the way of getting a usable safe code ecosystem.
  • Even worse, in order to make this feasible at all, I had to declare gloss not just safe, but trustworthy.  I really shouldn’t have done that, since I haven’t vetted all of the gloss code to ensure that it doesn’t let you do bad stuff.  I really wanted GHC to assume that proof obligation, but instead I did myself.  Why?  Well, if I’d made it safe, I would have had to declare this for only certain modules (a much more intrusive change) and transitively go modify and rebuild all the pure code that gloss depends on, and so on down the dependency tree.

Perhaps I missed something, but if GHC is missing the opportunity to decide for itself when a module is safe, that’s a real shame, and something that will stand as an obstacle in the way of plenty of much more interesting and grander uses of SafeHaskell.

Anyway, that’s it for now!  Have fun playing…

August 14, 2011 / cdsmith

Haskell For Kids: A Web-Based Environment

In a comment on my last post here, Matthias Felleisen made the comment that it might be possible to make the first week or two of the Haskell for Kids effort go better if there were a web-based environment available.  After some thought, I’ve set out to create such a thing, and I’ve got an afternoon’s worth of proof of concept put together now.  Here, I’ll explain what it is, what the status of it is, and how it works.

WARNING!

Before I say any more, let me point out that you need to be very careful about running the code I’m talking about.  It’s in its very early stages, and the project involves running arbitrary other people’s code on your computers.  Obviously, that’s just a bit dangerous.  In particular,

  • Do not run this code on any system containing sensitive information, like SSL private keys, personal information, etc.
  • Do not run this code on a public network where untrusted people might be connecting.
  • Do not run this code if you have enemies who know you’re doing it, or friends with a malfunctioning sense of humor…

The medium-term plan is to use GHC 7.2’s SafeHaskell extension, along with a reasonable set of resource limits, to run code safely and prevent access to unsafePerformIO and friends.  This is not part of the code yet, so for now it’s very, very unsafe.

Introducing the gloss-web package…

If you look at https://github.com/cdsmith/gloss-web, you’ll find a small amount of initial code toward a web-based environment for Haskell programming in Gloss.  It includes:

  • A web-based editor with syntax highlighting for Haskell, based on Cloud9’s ACE editor.
  • A compilation server that compiles, builds, and runs programs.
  • A JavaScript and JSON-based rendering system for viewing the resulting images.

In short, it’s everything you need to build pictures using Gloss without a local installation of Haskell.

Don’t take this as saying that you can completely skip installing Haskell for the class that’s starting in a few days.  In the end, that’s probably a bad idea.  But in a few situations (particularly in my in-person class, where getting GHC installed on everyone’s computers is likely to take some time), it may help rather a lot to have the ability for students to run their first programs in a web-based system.

Keep in mind that if you’re helping just one kid, as many blog readers are planning on doing, then this is probably a waste of your time.  Just install Haskell on the computer your kid is using instead!

What does it look like?

Good question!

How to Install

I have not released this on Hackage yet, because it’s in very, very early stages.  But you can download it from the github URL above and install it as follows.

  • Download the current code from github
  • Change into the directory and type ‘cabal install’.
  • Type ‘gloss-web’ to run.

You’ll need some relatively recent version of the Haskell Platform to get it working.  If you’re having problems, feel free to ask for help.

Want to Help?

For any experienced Haskell programmers out there who are interested in helping out, patches would be great!  I’ve got plans, and do intend to do them on an as-needed basis as the year-long class proceeds (three cheers for “lazy” evaluation!), but I’m also happy to accept patches from anyone else.

Some of the outstanding challenges include:

  • Test and get it working in more web browsers.  Currently it runs fine in Chrome, and I hope to have no major issues in Firefox or Safari, but I imagine IE will be a whole new ball game.
  • Add a better way to load images, since you can’t use the IO monad.  One thought I have is to let you upload images, and then throw in a built-in module called Images that can be imported that (via unsafePerformIO) defines symbols for each uploaded image.
  • Use SafeHaskell in GHC 7.2, or some other mechanism, to enforce safe execution and prevent use of Template Haskell, unsafePerformIO, the FFI, or any other tricks to get around the type system and run arbitrary code.
  • Implement resource limits and timeouts in case of badly behaved programs.
  • Add support for the animation, simulation, and game interfaces of gloss.  This will involve some kind of streaming from the server via XMLHTTPRequest or some such thing.
  • Better organization of the code.  This will probably use Snap 0.6 extensions, so I’m just keeping it working until that’s released.

I’m particularly interested in getting some of the safety issues handled, as that’s a prerequisite to running this publicly (currently I will be running it locally only for my local class).  The rest of it would be awesome too, though!

Enjoy!

August 13, 2011 / cdsmith

Arrow = Category + Applicative? (Part IIa)

I’m labeling this part (II a), because I haven’t got everything I wanted to finish for this piece, but there are enough interesting ideas that it’s worth posting something, and enough time has passed that I’m getting people asking about the next part!

Summary So Far

In the previous installment of this series, we established a one-way relationship between Applicative and Arrow, while assuming a common Category instance.  In particular, we assumed a data type

data a :~> b = ...

and instances

instance Category (:~>) where
    id    = ...
    (.)   = ...
instance Arrow (:~>) where
    arr   = ...
    first = ...

and satisfying the axioms

[C1] f                            = f . id
                                  = id . f
[C2] f . (g . h)                  = (f . g) . h
[A1] arr   id                     = id
[A2] arr   (f . g)                = arr f   . arr g
[A3] first (f . g)                = first f . first g
[A4] first (arr f)                = arr (f `cross` id)
[A5] first f . arr (id `cross` g) = arr (id `cross g) . first f
[A6] arr fst . first f            = f       . arr fst
[A7] arr assoc . first (first f)  = first f . arr assoc

And we showed that we can always write the following Applicative instance, universally quantified over any domain for the Category:

instance Applicative ((:~>) a) where
    pure x  = arr (const x)
    f <*> x = arr (uncurry (flip ($)))
            . first x
            . arr swap
            . first f
            . arr dup

And, furthermore, that it will automatically satisfy all four of the axioms for Applicative functors.

[F1] v                 = pure id <*> v
[F2] u <*> (v <*> w)   = pure (.) <*> u <*> v <*> w
[F3] pure f <*> pure x = pure (f x)
[F4] u <*> pure y      = pure ($ y) <*> u

This demonstrates that Arrow is at least as specific as the combination of Category and a universally quantified Applicative instance: if you have the first, then you automatically have the second as well.  We now want to explore the opposite direction…

The Inverse Correspondence

We will need a specific Arrow instance now to work with, defined in terms of an arbitrary Applicative instance.  Here’s the one we’ll be using:

instance Arrow (:~>) where
    arr f   = pure f <*> id
    first f = pure (,) <*> f . arr fst <*> arr snd

I’ll again try to convince you that these definitions make logical sense.  Keep in mind the following,

pure f <*> x = f <$> x = fmap f x

So the definition of arr is very general: it doesn’t even really need Applicative — just Functor.  That ought to be comforting, since in a sense all that Functor says is that we can naturally translate from pure Haskell functions to a different context.  It’s not surprising that there would be a strong connection between the lifting of functions given by fmap, and that given by Category and Applicative.  Indeed, arr is that connection.  The Category “id” value on the right of the fmap serves to tie the input from the Category with the input to the function f, giving precisely what we want: a lifting of f into the Category.

Another way to understand arr’s definition is to recall that in the ((->) t) functor, whose objects are just Haskell functions from a fixed domain type, fmap is precisely function composition.  The functor we have here looks very close to that one, and indeed, fmap has a similar meaning.  The difference is that in our applicative functor, fmap composes pure Haskell functions not with other functions, but with morphisms in our Category, giving a morphism as the result.  Lifting a function is done by composing it with the identity morphism.

The definition of first is basically self-evident if you’re familiar with Applicative.  If you’re confused, note that (.) binds more tightly than <*>… we’ll be using that a lot.  So this just unpacks a tuple, applies the given Category element on the left, and packs it back up using the tuple constructor.

Failure

Our stated goal was that by defining the correspondence above, things will just work out and we’ll have established that all of the axioms for Arrow hold.  This should be easy to check!  The Applicative laws give us a really nice tool to reason about equivalence of two expressions.  You may note that I’ve stated them slightly differently here, versus the previous post, by swapping the sides of a few of them.  You should read the four axioms [F1] through [F4] as having a natural left to right direction to them, and by applying each of them as appropriate, we can take any Applicative expression and obtain a normal form:

pure f <*> x_1 <*> x_2 <*> ... <*> x_n

Here, none of x_1 through x_n contain any applicative building blocks (pure or <*>, or any of the constants built from them like fmap, etc.)  Category also has such a normal form, where any expression from a category can be written as either a single identity, or a sequence of composed morphisms, with no other identities or composition occurring in the pieces:

f_1 . f_2 . ... . f_n

What about mixtures of the two?  We have no laws at all that allow us manipulate expressions across the two types, so we’re stuck with the pieces as they are, simplifying within each piece. So to verify the axioms, we simply substitute the definitions of arr and first from the previous section, reduce the Applicative and Category pieces to their respective normal forms, and compare.  Easy, right?

It’s left as an exercise for the reader to try this, but the result is that only the trivial axiom [A1] can be verified in this way.  The remaining Arrow laws do not follow from anything we’ve seen so far. It’s not just that we aren’t clever enough to do it: because both Applicative and Category have normal forms, and there’s no mixing of the two possible, it’s simply not possible that any more of the Arrow laws might be shown to hold all the time from those laws alone!  (This in spite of the fact that numerous source, such as here, explicitly claim otherwise!)

Dodging a Dead End Sign: New Laws!

In a strict sense sense, this is the end of the line: our original goal has conclusively failed.  That said, it’s not so surprising that it failed, and we can still learn a lot by redefining our goal.  We now seek to decide precisely what the difference is.

That is, can we state a (hopefully minimal) set of additional laws we can apply to the Applicative/Category combination, such that we can get all of the Arrow axioms? We’re looking for things that obviously ought to hold for all types that are simultaneously instances of Category and Applicative.  Of course, we’ll also have to go back and show that they follow from the Arrow axioms as well, or we risk losing the bidirectional correspondence.  It’s worth noting that Ross Patterson speculated about such axioms, and that while my axioms look a bit different, if you dig a bit they turn out to very very similar)

Here are the set of axioms I’ll propose:

[G1] u = pure const <*> u <*> id
[G2] u <*> id <*> id = pure join <*> u <*> id
[G3] arr f . u = pure f <*> u
[G4] (u <*> v) . arr f = u . arr f <*> v . arr f

A couple quick notes.  First of all, you might notice that the Arrow term, arr, appears in a couple of them.  That’s okay, though: we don’t mean arr in the Arrow sense.  We mean it in the sense of the definition earlier, as an fmap applied to the identity from the Category.  It turns out that arr plays a unique role in the structure we get from combining Category and Applicative.  It’s a sort of intermediate level of purity between “pure” elements and arbitrary elements.  The elements in the image of arr are pure in the sense of acting like plain functions in the Category, but they depend on the domain type from the Category, making them not quite “pure” in the Applicative sense.  It’s useful to make statements about elements with that half-purity property.

Second, you might notice a use of “join” in [G2], which is of course a Monad term!  Never fear, though, we mean join specialized to the ((->) r) monad, which is just the function:

join f x = f x x

So no worries, we haven’t let monads creep in quite yet!  The connection here is very strong though, and is strengthened by noting that “const” is similarly just “return” specialized to the ((->) r) monad, and together, return and join completely determine the monad structure on a type!  So in a sense, laws [G1] and [G2] are relating the structure we’ve got to monad terms… but the monad is the standard function monad instead of one defined on this type.

Having gained a little insight into [G1] and [G2], we now look at the laws [G3] and [G4].  These laws address the question of what happens when we compose an arr value, either on the left or right.  Essentially, arr composed on the left can be rewritten in terms of application, while on the right it distributes.

Let’s Prove Some Arrow Laws

One of the Arrow laws is so obvious, there’s no point in putting off its proof any longer; it turns out to be exactly equivalent to the first Applicative axiom, and is the one Arrow law that didn’t require our new assumptions:

arr id = pure id <*> id = id

Now, before we set out to methodically prove that Arrow axioms hold, it pays to look around and take stock of the situation with the new laws one at a time.

We can start out by generalizing [G1] and [G2] a bit.  As stated, these laws require identities on the right-hand side, but it turns out they actually only need semi-pure (that is, arr) values.  To see this, we’ll first prove a little lemma, which actually only requires the Applicative laws:

u <*> arr f = u <*> (pure f <*> id)
            = pure (.) <*> u <*> pure f <*> id
            = pure ($ f) <*> (pure (.) <*> u) <*> id
            = pure (.) <*> pure ($ f) <*> pure (.) <*> u <*> id
            = pure (($ f) . (.)) <*> u <*> id
            = pure (. f) <*> u <*> id

With that in our toolkit, we generalize [G1] and [G2] in the obvious way, just by moving arr values from the right to the left, and then moving the parentheses left.  It’s a tad cumbersome, but pretty obvious when you see what’s going on.

pure const <*> u <*> arr f
    = pure (. f) <*> (pure const <*> u) <*> id
    = pure (.) <*> pure (. f) <*> pure const <*> u <*> id
    = pure ((. f) . const) <*> u <*> id 
    = pure const <*> u <*> id
    = u
u <*> arr f <*> arr f
    = pure (. f) <*> (u <*> arr f) <*> id
    = pure (. f) <*> (pure (. f) <*> u <*> id) <*> id
    = pure (.) <*> pure (. f) <*> (pure (. f) <*> u) <*> id <*> id
    = pure ((.) (. f) <*> (pure (. f) <*> u) <*> id <*> id
    = pure (.) <*> pure ((.) (. f)) <*> pure (. f) <*> u <*> id <*> id
    = pure ((.) (. f) . (. f)) <*> u <*> id <*> id
    = pure join <*> (pure ((.) (. f) . (. f)) <*> u) <*> id
    = pure (.) <*> pure join <*> pure ((.) (. f) . (. f)) <*> u <*> id
    = pure (join . (.) (. f) . (. f)) <*> u <*> id
    = pure ((. f) . join) <*> u <*> id
    = pure (.) <*> pure (. f) <*> pure join <*> u <*> id
    = pure (. f) <*> (pure join <*> u) <*> id)
    = pure join <*> u <*> arr f

These identities can be very useful: they avoid the need to explicitly “stash away” semi-pure values on the right when applying the first two laws.  Note that the values on the right obviously need to be semi-pure, since otherwise we could be removing or duplicating effects (where “effects” here has the appropriate meaning for the particular instance you’re looking at).

Another convenient thing to note is that anywhere we use “arr” to indicate a semi-pure value, of course a pure value works too!  The following mini-identity makes this explicit:

pure x = pure const <*> pure x <*> id
       = pure (const x) <*> id
       = arr (const x)

We can now turn to the [G3] law, and see what insights it has to offer.  The first is actually one of the Arrow laws, but it’s also quite useful in reasoning about other things as well:

arr (f . g) = pure (f . g) <*> id
            = pure (.) <*> pure f <*> pure g <*> id
            = pure f <*> (pure g <*> id)
            = pure f <*> arr g
            = arr f . arr g

As an immediate consequence, we can simplify compositions involving pure and semi-pure values.

pure x . arr f = arr (const x) . arr f
               = arr (const x . f)
               = arr (const x)
               = pure x

A more broadly applicable set of identities lets us work with applications between pure values and compositions (of any values at all):

pure f <*> u . v = arr f . (u . v)
                 = (arr f . u) . v
                 = (pure f <*> u) . v
u . v <*> pure f = pure ($ f) <*> u . v
                 = (pure ($ f) <*> u) . v
                 = (u <*> pure f) . v

So applying a pure value to a composition, or a composition to a pure value, is the same as doing the application only to the first of the two values that are composed.

We also have the tools now to easily establish another of the Arrow laws.  Since we’ve done it so many times by now, I’ll start applying the composition law from Applicative and combining the resulting pure expressions on the left in one step.

arr fst . first f
    = pure fst <*> first f
    = pure fst <*> (pure (,) <*> f . arr fst <*> arr snd)
    = pure ((.) fst) <*> (pure (,) <*> f . arr fst) <*> arr snd
    = pure (((.) fst) . (,)) <*> f . arr fst <*> arr snd
    = pure const <*> f . arr fst <*> arr snd
    = f . arr fst

For the next step, it helps to consider what happens when you apply (with <*>) one semi-pure value to another.  The answer is reassuringly logical: Applicative’s <*> combinator can be specialized to functions, and the result goes by several names… Monad’s “ap”, for example, and combinatory logic’s S combinator.  Let’s use “ap” to describe the function we’re looking for:

(f `ap` g) x = f x (g x)

Then we have

arr f <*> arr g = arr f <*> (pure g <*> id)
                = pure (.) <*> arr f <*> pure g <*> id
                = arr (.) . arr f <*> pure g <*> id
                = pure ($ g) <*> arr (.) . arr f <*> id
                = arr ($ g) . arr (.) . arr f <*> id
                = arr (($ g) . (.) . f) <*> id
                = pure (($ g) . (.) . f) <*> id <*> id
                = pure join <*> pure (($ g) . (.) . f) <*> id
                = pure (f `ap` g) <*> id
                = arr (f `ap` g)

That turns out to be the hard work in establish our fourth Arrow law.

first (arr f) = pure (,) <*> arr f . arr fst <*> arr snd
              = arr (,) . arr f . arr fst <*> arr snd
              = arr ((,) . f . fst) <*> arr snd
              = arr (((,) . f . fst) `ap` snd)
              = arr (f `cross` id)

Not bad!  Four Arrow laws down, three to go, and we haven’t even used our shiny new [G4] law yet.  We can fix that, though, and prove a fifth Arrow law in the process:

first f . arr (id `cross` g)
    = (pure (,) <*> f . arr fst <*> arr snd) . arr (id `cross` g)
    = pure (,) . arr (id `cross` g)
      <*> f . arr fst . arr (id `cross` g)
      <*> arr snd . arr (id `cross` g)
    = pure (,) <*> f . arr (fst . (id `cross` g)) <*> arr (snd . (id `cross` g))
    = pure (,) <*> f . arr fst <*> arr (g . snd)
    = pure (,) <*> f . arr fst <*> arr g . arr snd
    = pure (,) <*> f . arr fst <*> (pure g <*> arr snd)
    = pure (.) <*> (pure (,) <*> f . arr fst) <*> pure g <*> arr snd
    = pure ((.) . (,)) <*> f . arr fst <*> pure g <*> arr snd
    = pure ($ g) <*> (pure ((.) . (,)) <*> f . arr fst) <*> arr snd
    = pure (($ g) . (.) . (,)) <*> f . arr fst <*> arr snd
    = pure ((.) (id `cross` g) . (,)) <*> f . arr fst <*> arr snd
    = pure ((.) (id `cross` g)) <*> (pure (,) <*> f . arr fst) <*> arr snd
    = pure (id `cross` g) <*> (pure (,) <*> f . arr fst <*> arr snd)
    = pure (id `cross` g) <*> first f
    = arr (id `cross` g) . first f

Of course, this series just wouldn’t be itself if we didn’t have a long ugly proof in there somewhere, so here it is: the proof of [A7].

arr assoc . first (first f)
    = pure assoc <*> first (first f)
    = pure assoc <*> (pure (,) <*> first f . arr fst <*> arr snd)
    = pure ((.) assoc) <*> (pure (,) <*> first f . arr fst) <*> arr snd
    = pure ((.) assoc . (,)) <*> first f . arr fst <*> arr snd
    = pure (. snd) <*> (pure ((.) assoc . (,)) <*> first f . arr fst) <*> id
    = pure ((. snd) . (.) assoc . (,)) <*> first f . arr fst <*> id
    = pure ((. snd) . (.) assoc . (,))
      <*> (pure (,) <*> f . arr fst <*> arr snd) . arr fst <*> id
    = pure ((. snd) . (.) assoc . (,))
      <*> (pure (,) . arr fst <*> f . arr fst . arr fst
      <*> arr snd . arr fst) <*> id
    = pure ((. snd) . (.) assoc . (,))
      <*> (pure (,) . arr fst <*> arr fst . arr fst . first (first f)
      <*> arr snd . arr fst) <*> id
    = pure ((. snd) . (.) assoc . (,))
      <*> (pure (,) <*> arr (fst . fst) . first (first f)
      <*> arr (snd . fst)) <*> id
    = pure ((.) ((. snd) . (.) assoc . (,)) . (,))
      <*> arr (fst . fst) . first (first f) <*> arr (snd . fst) <*> id
    = pure (. (snd . fst)) <*> (pure ((.) ((. snd) . (.) assoc . (,)) . (,))
      <*> arr (fst . fst) . first (first f)) <*> id <*> id
    = pure (.) <*> pure (. (snd . fst))
      <*> pure ((.) ((. snd) . (.) assoc . (,)) . (,))
      <*> arr (fst . fst) . first (first f) <*> id <*> id
    = pure ((. (snd . fst)) . (.) ((. snd) . (.) assoc . (,)) . (,))
      <*> arr (fst . fst) . first (first f) <*> id <*> id
    = pure (\x y z -> (x, (snd (fst y), snd z)))
      <*> arr (fst . fst) . first (first f) <*> id <*> id
    = pure join <*> (pure (\x y z -> (x, (snd (fst y), snd z)))
      <*> arr (fst . fst) . first (first f)) <*> id
    = pure (\((a,b),c) ((d,e),f) -> (a, (e, f))) <*> first (first f) <*> id
    = pure (. (snd `cross` id))
      <*> (pure (,) <*> (pure (fst . fst) <*> first (first f))) <*> id
    = pure (. (snd `cross` id))
      <*> (pure (,) <*> arr (fst . fst) . first (first f)) <*> id
    = pure (. (snd `cross` id))
      <*> (pure (,) <*> f . arr (fst . fst)) <*> id
    = pure (,) <*> f . arr (fst . fst) <*> arr (snd `cross` id)
    = pure (,) . arr assoc <*> f . arr fst . arr assoc <*> arr snd . arr assoc
    = (pure (,) <*> f . arr fst <*> arr snd) . arr assoc
    = first f . arr assoc

Not pretty, by any stretch of the imagination, but it’s done.

To be continued…

Quite a bit remains here: we still have one Arrow law remaining, we need to show that our four new Category+Applicative laws follow from the Arrow axioms in the other direction, and we need to show that the maps we’ve defined between Applicative and Arrow are inverse to each other.  With luck, this and more will come in the next exciting installment.

Follow

Get every new post delivered to your Inbox.

Join 74 other followers