Baby’s First Proof
Unlike many languages that you learn, in Coq, things are truly different. Much like your first functional language after using nothing but imperative languages, you have to re-evaluate things. Instead of just defining functions, you have to prove properties of them. So, let’s take a look at a few basic ways to do that.
Simpl and Reflexivity
Here we have two basic “tactics” that we can use to prove simple properties. Suppose we have some function addition
. We’re all familiar with how this works; 2 + 2 = 4
, right? Prove it:
Lemma two_plus_two:
2 + 2 = 4.
Proof.
Admitted.
First, what is this Admitted.
thing? Admitted basically tells Coq not to worry about it, and just assume it is true. This is the equivalent of your math professor telling you “don’t worry about it, Aristotle says it’s true, are you calling Aristotle a liar?” and if you let this make it into live code, you are a bad person. We must make this right!
Lemma two_plus_two:
2 + 2 = 4.
Proof.
simpl.
reflexivity.
Qed.
That’s better. This is a simple proof; we tell Coq to simplify the expression, then we tell Coq to verify that the left-hand-side is the same as the right-hand-side. One nice feature of Coq is that lets you step through these proofs to see exactly how the evaluation is proceeding. If you’re using Proof General, you can use the buttons Next
, Goto
, and Undo
to accomplish this. If you put the point at Proof.
and click Goto
, Coq will evaluate the buffer up to that point, and a window should appear at the bottom with the following:
1 subgoals, subgoal 1 (ID 2)
============================
2 + 2 = 4
This is telling you that Coq has 1 thing left to prove: 2 + 2 = 4
. Click next, the bottom should change to:
1 subgoals, subgoal 1 (ID 2)
============================
4 = 4
Coq processed the simpl
tactic and now the thing it needs to prove is that 4 = 4
. Obviously this is true, so if we click next…
No more subgoals.
…reflexivity
should succeed, and it does. If we click next one more time:
two_plus_two is defined
This says that this Lemma has been defined, and we can now refer to it in other proofs, much like we can call a function. Now, you may be wondering “do I really have to simplify 2 + 2
?” No, you don’t, reflexivity
will simplify on it’s own, this typechecks just fine:
Lemma two_plus_two:
2 + 2 = 4.
Proof.
reflexivity.
Qed.
So, what’s the point of simpl
then? Let’s consider a more complicated proof.
Induction
Lemma n_plus_zero_eq_n:
forall (n : nat), n + 0 = n.
This lemma state that for any n, n + 0 = n. This is the same as when you’d write ∀
in some math. Other bits of new syntax is n : nat
, which means that n has the type nat. The idea here is that no matter what natural number n is, n + 0 = n. So how do we prove this? One might be tempted to try:
Lemma n_plus_zero_eq_n:
forall (n : nat), n + 0 = n.
Proof.
reflexivity.
Qed.
One would be wrong. What is Coq stupid? Clearly n + 0 = n, Aristotle told me so! Luckily for us, this is a pretty easy proof, we just need to be explicit about it. We can use induction to prove this. Let me show the whole proof, then we’ll walk through it step by step.
Lemma n_plus_zero_eq_n:
forall (n : nat), n + 0 = n.
Proof.
intros n.
induction n as [| n'].
{
reflexivity.
}
{
simpl.
rewrite -> IHn'.
reflexivity.
}
Qed.
Place the point at Proof
and you’ll see the starting goal:
1 subgoals, subgoal 1 (ID 6)
============================
forall n : nat, n + 0 = n
Click next and step over intros n.
1 subgoals, subgoal 1 (ID 7)
n : nat
============================
n + 0 = n
What happened here is intros n
introduces the variable n, and names it n. We could have done intros theNumber
and the bottom window would instead show:
1 subgoals, subgoal 1 (ID 7)
theNumber : nat
============================
theNumber + 0 = theNumber
The intros
tactic reads from left to right, so if we had some Lemma foo : forall (n m : nat), [stuff]
, we could do intros nName mName.
, and it would read in n, and bind it to nName, and then read in m and bind it to mName. Click next and evaluate induction n as [| n'].
2 subgoals, subgoal 1 (ID 10)
============================
0 + 0 = 0
subgoal 2 (ID 13) is:
S n' + 0 = S n'
The induction
tactic implements the standard proof by induction, splitting our goal into two goals: the base case and the n + 1 case. Similarly to intros
, this will create subgoals starting with the first constructor of an ADT, and ending with the last.
On Natural Numbers in Coq
Let us take a second to talk about how numbers are represented in Coq. Coq re-implements all types within itself, so nat
isn’t a machine integer, it’s an algebraic datatype of the form:
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
O
is zero, S O
is one, and S (S (S (O)))
is three. There is a lot of syntax sugar in place that lets you write 49 instead of S (S ( ... ( S O) ... ))
, and that’s a good thing.
The point of all of this is that we can pattern match on nat
much like we can a list.
More Induction
…anyways, all this brings us back to induction and this mysterious as [| n'].
What this is doing is binding names to all the fields of the ADT we are deconstructing. The O
constructor takes no parameters, so there is nothing to the left of the |
. The S
constructor takes a nat
, so we give it the name n'
. Click next and observe the bottom change:
1 focused subgoals (unfocused: 1)
, subgoal 1 (ID 10)
============================
0 + 0 = 0
The curly braces “focuses” the current subgoal, hiding all irrelevant information. Curly braces are optional, but I find them to be very helpful as the bottom window can become very cluttered in large proofs. Here we see the base case goal being to prove that 0 + 0 = 0. Obviously this is true, and we can have Coq verify this by reflexivity.
Click next until the next opening curly brace is evaluated. We see the next subgoal:
1 focused subgoals (unfocused: 0)
, subgoal 1 (ID 13)
n' : nat
IHn' : n' + 0 = n'
============================
S n' + 0 = S n'
So, what do we have here? This is the n + 1 case; here the n’ in S n'
is the original n. A particularly bored reader may try to prove forall (n : nat), S n = n + 1
and I’ll leave that as an exercise. However, this follows from the definition of nat
.
Also of note here is IHn'
. IH
stands for induction hypothesis, and this is that n’ + 0 = n’. So, how do we proceed? Click next and observe how the subgoal changes:
1 focused subgoals (unfocused: 0)
, subgoal 1 (ID 15)
n' : nat
IHn' : n' + 0 = n'
============================
S (n' + 0) = S n'
It brought the + 0
inside the S
constructor. Notice that now there is n' + 0
on the left hand side. Click next and watch closely what happens:
1 focused subgoals (unfocused: 0)
, subgoal 1 (ID 16)
n' : nat
IHn' : n' + 0 = n'
============================
S n' = S n'
Here we use the induction hypothesis to rewrite all occurrences of n' + 0
, which was the left hand side of the induction hypothesis as n'
, which was the right hand side of the induction hypothesis. This is what the rewrite
tactic does. Notice now that the subgoal is S n' = S n'
which reflexivity
will surely find to be true. So, what would happen if we had done rewrite <- IHn'.
?
1 focused subgoals (unfocused: 0)
, subgoal 1 (ID 16)
n' : nat
IHn' : n' + 0 = n'
============================
S (n' + 0 + 0) = S (n' + 0)
It rewrote all instances of n'
, which was the right hand side of the induction hypothesis with n' + 0
which was the left hand side of the induction hypothesis. Obviously, this isn’t what we want. I should note that you can undo this by rewriting to the right twice…
{
simpl.
rewrite <- IHn'.
rewrite -> IHn'.
rewrite -> IHn'.
reflexivity.
}
…and it will technically work. But don’t do this, it’s silly and there’s no room for silliness in a rigorous mathematical proof.
Personally, I have a hard time keeping it straight what the left and right rewrites do. I sometimes find myself just trying one, and then the other if I guessed wrong. Think of it like this: rewrite -> foo
rewrites the current goal, replacing all occurrences of the thing on the left hand side of the equation of foo
with the thing on the right hand side of the equation. It changes from the left to the right. And vice-versa for rewrite <-
, which changes from the right to the left.
Functional Doubly Linked Lists
It’s often been said that functional programming just isn’t cut out for certain tasks. File IO? Please… Databases? Forget about it!
I’ve always figured that the humble Doubly Linked list was on this list. After all, how do we implement these in C? An implementation would probably look something like this:
struct _DList
{
struct DList * next;
struct DList * prev;
void * element;
} DList;
In this case, the element pointed to by prev and next have pointers to this element, if they aren’t NULL. The Doubly Linked list isn’t exactly a complicated structure, this is basically the way to do it. So, how would we do this in Haskell?
In the past, I’ve thought there were three answers to this question:
1) Use C pointers. This would involve use of unsafePerformIO
, and you’d be a monster.
2) Use a singly linked list, and pretend it’s doubly linked. This would involve a “prev” function that just walks from the beginning of the list to the element before the current one. You’d be an even bigger monster than the guy who did option 1.
3) Don’t use a doubly linked list. To me, this is actually reasonable. In a world where arrays are basically always better, the only reason to use a list is because they’re very easy to deal with. If you need the level of complexity of a doubly linked list, you’re probably just better off with a different data structure.
But recently, I thought of a way to implement a doubly linked list in Haskell without being a bad person.
Preserved Here For Posterity
The implementation is actually quite simple. Here’s our type:
data DoublyLinkedList a =
DList [a] [a] |
Nil
Obviously, we have our Nil
type for the empty list. We also have DList, which has two lists. Why two? On the left, we have the previous elements. This starts empty. On the right, we have our next elements. As we walk the list, we pop elements from the head of the right list to the head of the left list. The head of the right list is our current element. Let’s see some functions:
get :: DoublyLinkedList a -> a
get (DList _ (x:xs)) = x
This function returns the “current” element; the element at the current position in the list.
next :: DoublyLinkedList a -> DoublyLinkedList a
next (DList _ []) = undefined
next (DList prev (c:next)) = DList (c:prev) next
prev :: DoublyLinkedList a -> DoublyLinkedList a
prev (DList [] _) = undefined
prev (DList (c:prev) next) = DList prev (c:next)
These two functions move the cursor forward or backward. As you can see, when next is called, the current element is popped from the next list, and pushed onto the previous list. The opposite happens when prev is called. I’ve left the edge cases undefined, but a real implementation should do something sane here. (return a Maybe, throw an exception, etc…)
insert :: DoublyLinkedList a -> a -> DoublyLinkedList a
insert Nil e = DList [] [e]
insert (DList prev next) e = DList prev (e:next)
Elements are inserted in front of the current element.
makeDouble :: [a] -> DoublyLinkedList a
makeDouble [] = Nil
makeDouble l = DList [] l
…and it is trivial to convert a singly linked list into a doubly linked list. We can even add a pretty show instance!
instance (Show a) => Show (DoublyLinkedList a) where
show Nil = "Nil"
show (DList prev (c:next)) = (show $ reverse prev) ++
"*[" ++
(show c) ++
"]*" ++
show next
Obviously, we could go crazy and make a Monad instance and other things, but you get the idea. The final solution was very simple. One could even say simpler than the C version as you don’t have to worry about updating the next and prev pointers when adding elements. Sure, it took a bit of thought, but like many things in Haskell, the result was simple and elegant.
Checking Our Heads With Liquid Haskell
Consider this function:
headInTail :: [a] -> [a]
headInTail l = (tail l) ++ [head l]
Pretty straightforward, right? It takes a list, extracts the head and sticks it in the tail. Surely you’ve written something like this before. It should be fine, right?
*Main> headInTail [1,2,3]
[2,3,1]
…checks out. Let’s try a few more:
*Main> headInTail "hello"
"elloh"
*Main> headInTail ["cat"]
["cat"]
…good. And the moment we’ve all been waiting for:
*Main> headInTail []
*** Exception: Prelude.tail: empty list
Oh yeah, head
and tail
don’t work for empty lists… Normally, we have some choices on how to proceed here. We could wrap the function in a Maybe
:
maybeHeadInTail :: [a] -> Maybe [a]
maybeHeadInTail [] = Nothing
maybeHeadInTail l = Just $ headInTail l
…which introduces an annoying Maybe
to deal with just to stick our heads in our tails. Or, we could just do something with the empty list:
headInTail :: [a] -> [a]
headInTail [] = []
headInTail l = (tail l) ++ [head l]
…but what if returning the empty list isn’t the correct thing to do?
Another choice is to document this behavior (as head
and tail
do), and just never call headInTail []
. But how can we guarantee that we never attempt to call this function on an empty list? Shouldn’t this be the type system’s problem?
Unfortunately, not all is roses and puppies. Sometimes the type system cannot help us. Sometimes somebody thought it’d be a good idea to use Haskell’s Evil exception system. Whatever the case, there are tools to help us.
Liquid Haskell
Liquid Haskell is a static code analysis tool that is used to catch just these sorts of problems. Liquid Haskell allows us to define invariants which will be enforced by the tool. Liquid Haskell is a research project that is still in development. As such, it has some rough spots, however it’s still very much capable of helping us with our problem here. But before we begin, we need to get the tool installed.
To install the tool, execute:
cabal install liquidhaskell
…simple right? Unfortunately, we’re not quite done. We need to install an SMT solver. This tool is used by Liquid Haskell. Currently, the tool defaults to Z3. I’m not sure how to use a different solver (and Z3 works just fine), so I suggest you you Z3. You’ll have to build Z3, and place the binary somewhere on the PATH
. After this is done, and assuming your .cabal/bin
directory is also on the PATH
, testing your source file is a simple as:
liquid [FILE].hs
Let’s Have A Look
Create a haskell source file that contains the following:
headInTail :: [a] -> [a]
headInTail l = (tail l) ++ [head l]
After that’s done, let Liquid Haskell analyze your file:
liquid [YOUR_FILE].hs
A bunch of stuff should scroll by, then in a second you’ll see something similar to the following:
**** UNSAFE *********************************************
Doop.hs:5:22: Error: Liquid Type Mismatch
Inferred type
VV : [a] | VV == l && len VV >= 0
not a subtype of Required type
VV : [a] | len VV > 0
In Context
VV : [a] | VV == l && len VV >= 0
l : [a] | len l >= 0
If you go to the line and column indicated, you’ll find the argument to tail. Conveniently, it seems that Liquid Haskell comes pre-loaded with definitions for some library functions. Normally, you’ll have to define those yourself. In fact, let’s do just that.
The next logical step here is to write a specification for our function. This specification is a statement about what sorts of values the function can take. Add the following to your source file, in the line above the signature for headInTail:
{-@ headInTail :: {l:[a] | len l > 0} -> [a] @-}
If you re-run liquid
on your source file, you’ll see that the warning went away, and the program now indicates that your source is “SAFE”. So, what does this refinement mean?
Basically, these refinements are machine-checked comments. They have no impact on the program, they exist for Liquid Haskell. Think of it as being like an enhanced type signature. Like a normal type signature, we start with the name of the function, then two colons. This part, however:
{l:[a] | len l > 0}
…should be new. Basically, this part says that the list should not be empty. You should read it as “l is a [a] such that len l is greater than zero.” A lot of the notation used by Liquid Haskell comes from formal logic. Let’s break this down some more:
l:[a]
Here we bind a symbol, l, to the first list argument. At any point to the right of this symbol until the end of the scope defined by {}
, we can reference this symbol.
{... | ...}
The pipe symbol indicates that we are going to make some statement about the type on the left hand side.
len l > 0
Here we state that the length of l must be greater than 0. It looks like we are calling a function, and we sort of are; len is a measure which is a special function that is used in specifications. However, the subject of measures is a post for another day.
You may now be thinking: “Well this is all well and good, but what’s to stop me from calling this function on an empty list?” To answer that, let’s implement main:
main =
do i <- getLine
putStrLn $ headInTail i
Add this to your source file, and then run liquid [YOUR_FILE].hs
and you’ll notice that Liquid Haskell has a problem with your attempt to call headInTail
:
**** UNSAFE *********************************************
Doop.hs:3:29: Error: Liquid Type Mismatch
Inferred type
VV : [Char] | VV == i && len VV >= 0
not a subtype of Required type
VV : [Char] | len VV > 0
In Context
VV : [Char] | VV == i && len VV >= 0
i : [Char] | len i >= 0
Liquid Haskell is telling you that it can’t prove that the length of i
is greater than 0. If you execute your main function, you should see that it works as expected. Type in a string, and it’ll do the right thing. Push enter right away and you’ll get an exception.
*Main> main
hello
elloh
*Main> main
*** Exception: Prelude.tail: empty list
…ick… Let’s fix this:
main =
do i <- getLine
case i of
[] -> putStrLn "Get your head checked."
_ -> putStrLn $ headInTail i
Now if you analyze your file, Liquid Haskell should be happy. Honestly, you should be happy too: the tool caught this problem for you. It didn’t go to testing messed up, and the bug certainly didn’t escape testing unfound. Your program is now objectively better:
*Main> main
isn't that neat?
sn't that neat?i
*Main> main
Get your head checked.
Again, This Time In Reverse!
Today we’ll be doing Exercise 5 from The C Programming Language. Today’s exercises aren’t terribly challenging, but there is some good stuff in here. The problem is:
Modify the temperature conversion program to print the table in reverse order, that is, from 300 degrees to 0.
I bet you thought we were done with temperature conversion, didn’t you? I’m right there with you, but luckily for us, this is also the section that introduces the for
loop, so this is much less tedious. The new program for modification:
#include <stdio.h>
int main (int argc, char ** argv)
{
for (int fahr = 0; fahr <= 300; fahr = fahr + 20)
{
printf("%3d %6.1f\n", fahr, (5.0/9.0)*(fahr-32));
}
}
I made a few minor modifications. I gave main
the correct signature to keep gcc from complaining, and I also moved the initialization of fahr
to the loop. As you may know this is not valid C, and the compiler will throw an error. You might also know that this was made to be valid C in the C 99 revision. To compile this, you just need to add the -std=c99
flag to your gcc call.
To complete this exercise, you only need to modify the loop declaration. Change this line…
for (int fahr = 0; fahr <= 300; fahr = fahr + 20)
…to this…
for (int fahr = 300; fahr >= 0; fahr = fahr - 20)
Pretty straight forward stuff here. fahr
starts at 300 instead of 0, and the loop continues so long as it remains greater than 0. Instead of adding 20 each iteration, we subtract it. This can be compiled like so:
gcc -std=c99 -Wall ex5.c -o ex5
In Haskell
Unfortunately, the authors of The C Programming Language did not see fit to include a starting Haskell program for us to modify. This seems like a pretty serious oversight to me, but we’ll just have to make due. Luckily for us, we can use the temperature conversion program I wrote for the last entry in this series. This program handles conversions, and we can use it to produce a table of all conversions between 0 and 300 degrees.
While I’ve established that Haskell does in fact have loops, we won’t be using them here. Instead we’ll be using ranges, functors, and sequencing to solve this problem in a more functional way.
First, we need a list of every 20th number between 0 and 300:
[300.0, 280.0 .. 0.0]
The ..
there basically says “You get the idea, do that.” If you put enough information into it so that the compiler can figure out the pattern, and start and end points, the compiler will fill the rest in. In this case, I gave the first two values, telling the compiler I want increments of 20, and I gave it the last value so it knows where to stop.
Unfortunately, as you recall, my conversion program needs members of the Temperature
typeclass. Surely I don’t plan to make Double
a member, right? Right. We need to map a function over this list to produce a list of Temperature
s. But what function should we use?
Something that beginning Haskellers may not realize is that constructors are in fact functions!
Prelude> :t Just
Just :: a -> Maybe a
Prelude> :t Left
Left :: a -> Either a b
…and of course…
*Main> :t Fahrenheit
Fahrenheit :: Double -> Fahrenheit
That’s right, we can map Fahrenheit
over a functor just like any other function!
map Fahrenheit [300.0, 280.0 .. 0.0]
This will produce a list of every 20th Fahrenheit
temperature between 300 and 0. However, we aren’t done yet. We actually need a list of Conversion
s, because this type is required for our insertConv
function. To get this we can map toConversion
over this list:
map toConversion $ map Fahrenheit [300.0, 280.0 .. 0.0]
…but that’s starting to get a bit ugly, there must be a better way. Normally, I’m not terribly fond of function composition, in this case it will make our life easier.
Function Composition
Haskell provides an operator .
that is used for function composition. Let’s take a look at its type:
Prelude> :t (.)
(.) :: (b -> c) -> (a -> b) -> a -> c
The composition operator takes a function that takes some type b
as an argument, and that returns some type c
. It takes a second function that takes some type a
as an argument, and that returns some type b
. Finally, it returns some type c
.
What does this do for us? Basically, it takes a function a -> b
, and a function b -> c
, and turns them into a function a -> c
. Let’s see an example:
Prelude> :t show
show :: Show a => a -> String
The function show
takes a member of the Show
typeclass and returns a String
.
Prelude> :t putStr
putStr :: String -> IO ()
The function putStr
takes a String
, and returns an IO
action.
Prelude> :t putStr . show
putStr . show :: Show a => a -> IO ()
When we compose the two functions, we get a function that takes a member of the Show
typeclass, and returns an IO
action.
Logically, calling putStr . show someShowable
is the same as calling putStr $ show someShowable
or putStr (show someShowable)
. However, putStr . show
is a valid function, where putStr $ show
and putStr (show)
are compiler errors if you don’t give show
an argument.
How does this help us?
*Main> :t Fahrenheit
Fahrenheit :: Double -> Fahrenheit
*Main> :t toConversion
toConversion :: (Temperature a, Temperature b) => a -> (a, b)
*Main> :t toConversion . Fahrenheit
toConversion . Fahrenheit :: Temperature b => Double -> (Fahrenheit, b)
By composing toConversion
and Fahrenheit
, we end up with a function that takes a Double
as an argument and returns a Conversion
from Fahrenheit
. We can then map
this function over our list of Double
s:
map (toConversion . Fahrenheit) [300.0, 280.0 .. 0.0]
Next, we need to turn these Conversion
s into TableBuilder
s. This is a simple matter of composing insertConv
:
map (insertConv . toConversion . Fahrenheit) [300.0, 280.0 .. 0.0]
The type of this new function is:
:t (insertConv . toConversion . Fahrenheit)
(insertConv . toConversion . Fahrenheit) :: Double -> TableBuilder ()
…or at least it would be if the type inferrer could figure out the type of toConversion
. Unfortunately for us, it can’t because the implementation is purposely ambiguous. We need to add a type signature to it:
(insertConv . (toConversion :: Fahrenheit -> (Fahrenheit, Celsius))
. Fahrenheit)
Sequencing
Now we are ready to create our table. This part is actually very easy. Thanks to the library function sequence_
we won’t even need a do
block. What does this function do? Let’s look at its signature:
Prelude> :t sequence_
sequence_ :: Monad m => [m a] -> m ()
Prelude> :t sequence
sequence :: Monad m => [m a] -> m [a]
There are two variations of this function. The first, sequence_
evaluates each monadic action, and ignores the results. Basically, suppose we have some function: func :: a -> Monad b
let mList = map func ["foo", "bar", "baz"]
in sequence_ mList
…is equivalent to…
do func "foo"
func "bar"
func "baz"
return ()
The second variation evaluates each monadic action, and returns a list of all the results. Suppose we have our same function: func :: a -> Monad b
let mList = map func ["foo", "bar", "baz"]
in sequence mList
…is equivalent to…
do foo <- func "foo"
bar <- func "bar"
baz <- func "baz"
return [foo, bar, baz]
If you have a list of monads, you can use sequence
or sequence_
to have them all evaluated. Use sequence
if you care about the resulting values, use sequence_
if you only care about the monad’s side effect. Which do we want? Let’s look at the signature of insertConv
:
*Main> :t insertConv
insertConv
:: (Temperature a, Temperature b) =>
Conversion a b -> TableBuilder ()
If we were to use sequence
, we’d get a resulting value with the type TableBuilder [()]
. Since nobody has any use for a list of empty tuples, we’ll be using sequence_
.
So, what does our main look like?
main = do temps <- return (map (insertConv . (toConversion :: Fahrenheit -> (Fahrenheit, Celsius))
. Fahrenheit)
[300.0, 280.0 .. 0.0])
putStrLn $ prettyPrint $ buildTable $ do sequence_ temps
This produces the following output:
------------------------------
|| Fahrenheit || Celsius ||
------------------------------
|| 300.0 |> 148.9 ||
|| 280.0 |> 137.8 ||
|| 260.0 |> 126.7 ||
|| 240.0 |> 115.6 ||
|| 220.0 |> 104.4 ||
|| 200.0 |> 93.3 ||
|| 180.0 |> 82.2 ||
|| 160.0 |> 71.1 ||
|| 140.0 |> 60.0 ||
|| 120.0 |> 48.9 ||
|| 100.0 |> 37.8 ||
|| 80.0 |> 26.7 ||
|| 60.0 |> 15.6 ||
|| 40.0 |> 4.4 ||
|| 20.0 |> -6.7 ||
|| 0.0 |> -17.8 ||
------------------------------
K&R Challenge 3 and 4: Functional Temperature Conversion
The other day, I implemented the C solution to exercises 3 and 4 in The C Programming Language, today I’ll be implementing the Haskell solution. As a reminder, the requirements are:
Modify the temperature conversion program to print a heading above the table
… and …
Write a program to print the corresponding Celsius to Fahrenheit table.
I could take the easy way out, and implement the Haskell solution almost identically to the C solution, replacing the for
loop with a call to map
, but that’s neither interesting to do, nor is it interesting to read about. I’ll be taking this problem to the next level.
Requirements
For my temperature program, I’d like it to be able to convert between any arbitrary temperature unit. For the purposes of this post, I will be implementing Celsius, Fahrenheit, Kelvin (equivalent to Celsius, except 0 degrees is absolute zero, not the freezing point of water), and Rankine (the Fahrenheit version of Kelvin).
That said, nothing about my solution should rely on the fact that these four temperature scales are being implemented. A programmer should be able to implement a new temperature unit with minimal changes to the program. Ideally, just by implementing a new type.
Additionally, given a bunch of conversions, the program should be able to output a pretty table showing any number of temperature types and indicating what converts to what.
First, Conversion
This problem is clearly broken up into two sub-problems: conversion, and the table. First, we need to handle conversion. This being Haskell, the right answer is likely to start by defining some types. Let’s create types for our units:
newtype Celsius = Celsius Double deriving (Show)
newtype Fahrenheit = Fahrenheit Double deriving (Show)
newtype Kelvin = Kelvin Double deriving (Show)
newtype Rankine = Rankine Double deriving (Show)
I’ve chosen to make a type for each unit, and since they only contain one constructor with one field, I use a newtype
instead of a data
. Now, how to convert these? A straightforward solution to this would be to define functions that convert each type to each other type. Functions that look like:
celsiusToFahrenheit :: Celsius -> Fahrenheit
celsiusToKelvin :: Celsius -> Kelvin
...
rankineToKelvin :: Rankine -> Kelvin
rankineToCelsius :: Rankine -> Celsius
A diagram for these conversions looks like this:
That’s a lot of conversions! One might argue that it’s manageable, but it certainly doesn’t meet requirement #1 that implementing a new unit would require minimal work; to implement a new conversion, you’d need to define many conversion functions as well! There must be a better way.
Let’s think back to chemistry class. You’re tasked with converting litres to hours or somesuch. Did you do that in one operation? No, you used a bunch of intermediate conversion to get to what you needed. If you know that X litres are Y dollars, and Z dollars is one 1 hour, then you know how many litres are in 1 hour! These are called conversion factors.
Luckily for us, our conversions are much simpler. For any temperature unit, if we can convert it to and from celsius, then we can convert it to and from any other unit! Let’s define a typeclass for Temperature
:
class Temperature a where
toCelsius :: a ->
Celsius
fromCelsius :: Celsius ->
a
value :: a ->
Double
scaleName :: a ->
String
convert :: (Temperature b) =>
a ->
b
convert f = fromCelsius $ toCelsius f
Our Temperature
typeclass has five functions: functions to convert to and from celsius, a function to get the value from a unit, a function to get the name of a unit, and a final function convert
. This final function has a default implementation that converts a unit to celsius, then from celsius. Using the type inferrer, this will convert any unit to any other unit!
convert Rankine 811 :: Kelvin
convert Celsius 123 :: Fahrenheit
convert Kelvin 10000 :: RelativeToHeck
Now to implement a new temperature, you only need to implement four functions, as convert
is a sane solution for all cases. This arrangement gives us a conversion diagram that looks like:
Much better. Let’s go through our Temperature
implementations for our types:
instance Temperature Celsius where
toCelsius c = c
fromCelsius c = c
value (Celsius c) = c
scaleName _ = "Celsius"
Of course Celsius
itself has to implement Temperature
. It’s implementation is trivial though; no work needs to be done.
instance Temperature Fahrenheit where
toCelsius (Fahrenheit f) = Celsius ((5 / 9) * (f - 32))
fromCelsius (Celsius c) = Fahrenheit ((9 / 5) * c + 32)
value (Fahrenheit f) = f
scaleName _ = "Fahrenheit"
Now things are heating up. The conversion functions are identical to the C implementation.
instance Temperature Kelvin where
toCelsius (Kelvin k) = Celsius (k - 273.15)
fromCelsius (Celsius c) = Kelvin (c + 273.15)
value (Kelvin k) = k
scaleName _ = "Kelvin"
The Kelvin
implementation looks much like the Fahrenheit
one.
instance Temperature Rankine where
toCelsius (Rankine r) = toCelsius $ Fahrenheit (r - 459.67)
fromCelsius c = Rankine $ 459.67 + value (fromCelsius c :: Fahrenheit)
value (Rankine r) = r
scaleName _ = "Rankine"
The conversion between Fahrenheit and Rankine is much simpler than the conversion between Celsius and Rankine; therefore I will do just that. After converting to and from Fahrenheit, it’s a simple matter of calling toCelsius
and fromCelsius
.
Bringing The Monads
Now that the easy part is done, we get to create the table. Our table should have as many columns as it needs to display an arbitrary number of conversions. To that end, let’s define a data structure or two:
data ConversionTable = ConversionTable [String]
[[TableRowElem]] deriving (Show)
data TableRowElem = From Double | To Double
| NullConv Double
| Empty deriving (Show)
The ConverstionTable
, like the name suggests, is our table. The list of strings is the header, and the list of lists of TableRowElem
are our conversions. Why not just have a list of Double
? We need to have our cells contain information on what they mean.
To that end, I created a TableRowElem
type. From
is an original value, To
is a converted value, NullConv
represents the case were we convert from some type to the same type, and Empty
is an empty cell. The problem of how to place elements into this data structure still remains however. To solve that, things are going to get a bit monadic. Let’s define some intermediate builder types:
type Conversion a b = (a, b)
toConversion :: (Temperature a, Temperature b) =>
a ->
(a, b)
toConversion a = (a, convert a)
First we have Conversion
, and the corresponding toConversion
function. This simply takes a unit, and places it in a tuple with its corresponding conversion. Next, we have the TableBuilder
:
type TableBuilder a = WriterT [[TableRowElem]]
(State [String]) a
Here we have a WriterT
stacked on top of a State
monad. The writer transformer contains the list of table rows, and the state monad contains the header. The idea is that as rows are “logged” into the writer, the header is checked to make sure no new units were introduced. To this end, if only two units are introduced, the table will have two columns. If 100 units are used, then the table will have 100 columns.
NOTE: I realize that WriterT
and State
are not in the standard library. I only promised to limit the usage of libraries for Haskell solutions. This means avoiding the use of things like Parsec or Happstack. Frameworks and libraries that vastly simplify some problem or change the way you approach it. To this end, if I feel a monad transformer or anything along these lines are appropriate to a problem, I will use them. I’ll try to point out when I do though. Besides, I could have just re-implemented these things, but in the interest of not being a bad person and re-inventing the wheel, I’ve decided to use a wheel off the shelf.
So, how do we use this TableBuilder
? I’ve defined a function for use with this monad:
insertConv :: (Temperature a, Temperature b) =>
Conversion a b ->
TableBuilder ()
insertConv (a, b) =
do oldHeader <- lift $ get
workingHeader <- ensureElem a oldHeader
finalHeader <- ensureElem b workingHeader
lift $ put finalHeader
tell [buildRow a b finalHeader []]
where ensureElem a h = return $ case ((scaleName a) `elem` h)
of True -> h
False -> h ++ [(scaleName a)]
buildRow _ _ [] r = r
buildRow a b (h:xs) r
| (scaleName a) == (scaleName b) && (scaleName a) == h = r ++ [NullConv $ value a]
| (scaleName a) == h = buildRow a b xs (r ++ [From $ value a])
| (scaleName b) == h = buildRow a b xs (r ++ [To $ value b])
| otherwise = buildRow a b xs (r ++ [Empty])
Yeah, that one is kind of a doosey. Let me walk you through it. This function takes a Conversion
, and returns a TableBuilder
.
In the first four lines of the do
block, we update the header. We lift
the State
monad, then get
we call ensureElem
with the first and second units, then we put
the new updated header back into the State
monad.
The ensureElem
function checks the header list to see if the current unit is a member. If it is, the header list is returned unchanged, if it’s not the unit is appended to the end and the new list is returned. In this way, whenever a conversion is added to the table, the header is updated.
After updating the header, we call tell
with the result of buildRow
, “writing” the row into the Writer
monad. The buildRow
function recursively adds TableRowElem
s to the result list depending on the current heading. In this way, conversions are placed in the appropriate column.
In addition to that function, I’ve defined a function to simplify working with the TableBuilder
:
buildTable :: TableBuilder a ->
ConversionTable
buildTable b = let result = runState (runWriterT b) []
in ConversionTable (snd result)
(snd $ fst result)
Working with some of these MTL
monads can be confusing for people coming from imperative backgrounds. I’ve been working with Haskell for almost a year now and I still get extremely confused by them. It can take some muddling through haddoc pages to work them out, but the good news is that you mainly just need to define one function that takes a monad (in the form of a do
block), and returns a whatever. The buildTable
function takes a TableBuilder
, and returns a ConversionTable
. It handles calls to runState
and runWriterT
, and then unwraps the resulting tuple and builds the ConversionTable
.
This function can be called like this:
buildTable $ do insertConv someConversion
insertConv someOtherConversion
… and so on. The only thing to remember is that the final value of a
for the do
block must be ()
. Conveniently, insertConv
return a value of type TableBuilder ()
, so if the last call is to this function, then you are good. You can also always end it with return ()
if you like.
Pretty Printing
Finally, we have the matter of printing a nice pretty table. For that, we need yet another function:
prettyPrint :: ConversionTable ->
String
prettyPrint (ConversionTable h r) = let widestCol = last $ sort $ map length h
columnCount = length h
doubleCell = printf ("%-" ++ (show widestCol) ++ ".1f")
stringCell = printf ("| %-" ++ (show widestCol) ++ "s |")
emptyCell = replicate widestCol ' '
horizontalR = (replicate (((widestCol + 4) * columnCount) + 2) '-') ++ "\n"
formatRow row = "|" ++ (concat $ map formatCell row) ++ "|\n"
formatCell (From from) = "| " ++ (doubleCell from) ++ " |"
formatCell (To to) = "> " ++ (doubleCell to) ++ " |"
formatCell Empty = "| " ++ emptyCell ++ " |"
formatCell (NullConv nc) = "| " ++ (doubleCell nc) ++ " |"
in horizontalR
++ ("|" ++(concat $ map stringCell h) ++ "|\n")
++ horizontalR
++ (concat $ map formatRow (normalizeRowLen (columnCount) r))
++ horizontalR
where normalizeRowLen len rows = map (nRL' len) rows
where nRL' len' row
| (length row) < len' = nRL' len' (row ++ [Empty])
| otherwise = row
Yeah… Sometimes the littlest things take the most work. You’d think all this plumbing we’ve been doing would be the most complecated bit, but you’d be wrong. Let’s try to make sense of this mess function by function:
widestCol = last $ sort $ map length h
This function determines the widest column based on the header. Typically, this is going to be “Fahrenheit”, but it doesn’t have to be. It should be noted that if a data cell is wider than this, then the pretty printer will mess up. Like most things in life, there is room for improvement here. That said, unless you’re converting the temperature of the core of the sun, you probably won’t have an issue here.
columnCount = length h
Returns the number of columns in the table. Used by the horizontal rule function.
doubleCell = printf ("%-" ++ (show widestCol) ++ ".1f")
Ahh, our old friend printf
. It exists in Haskell and works in much the same way as it did in C. The doubleCell
function converts a temperature value to a string, left aligns it, pads it by widestCol
, and has it show one decimal place.
stringCell = printf ("| %-" ++ (show widestCol) ++ "s |")
Much like with doubleCell
, this function pads, and left-aligns a string. This is used by the header.
emptyCell = replicate widestCol ' '
This one is pretty self-explanatory. It prints an empty cell of the appropriate width.
horizontalR = (replicate (((widestCol + 4) * columnCount) + 2) '-') ++ "\n"
This function prints a horizontal rule. This will be a solid line of “-” across the width of the table.
formatRow row = "|" ++ (concat $ map formatCell row) ++ "|\n"
This function formats a table data row. It maps formatCell
over the list of cells, flattens it, then adds a pretty border around it.
formatCell (From from) = "| " ++ (doubleCell from) ++ " |"
formatCell (To to) = "> " ++ (doubleCell to) ++ " |"
formatCell Empty = "| " ++ emptyCell ++ " |"
formatCell (NullConv nc) = "| " ++ (doubleCell nc) ++ " |"
In this function, much of the work is done. It formats the cell using doubleCell
or emptyCell
, the applies a border to the cell. It denotes a cell containing a To
by adding a >
on the left.
Now that we’ve covered the let
-bound functions, let’s talk about the actual function body:
horizontalR
concat $ map stringCell h) ++ "|\n")
horizontalR
concat $ map formatRow (normalizeRowLen (columnCount) r))
horizontalR
This bit is prett straightforward. First, it prints a horizontal line. Second, it maps stringCell
over the header list, flattens it, and gives it a border. Third it prints another horizontal line. Fourth is maps formatRow
over the normalized row list, then flattens it. Finally, one last horizontal line. After this is all said and done, it concats it all together.
You may be wondering about that normalizeRowLen
function. If you were paying particularly close attention to the insertConv
function, you may have noticed an issue. Let’s walk through it in ghci:
*Main> let fc = toConversion (Fahrenheit 100) :: (Fahrenheit, Celsius)
*Main> buildTable $ do insertConv fc
ConversionTable ["Fahrenheit","Celsius"] [[From 100.0,To 37.77777777777778]]
We add one conversion, we get two columns. Everything seems to be in order here, but let’s add another conversion and see what happens:
*Main> let fc = toConversion (Fahrenheit 100) :: (Fahrenheit, Celsius)
*Main> let cr = toConversion (Celsius 100) :: (Celsius, Rankine)
*Main> buildTable $ do {insertConv fc; insertConv cr;}
ConversionTable ["Fahrenheit","Celsius","Rankine"] [[From 100.0,To 37.77777777777778],[Empty,From 100.0,To 671.6700000000001]]
See the problem? Let’s add some newlines to make it clearer:
ConversionTable ["Fahrenheit","Celsius","Rankine"]
[[From 100.0,To 37.77777777777778],
[Empty,From 100.0,To 671.6700000000001]]
As we add more columns, the rows with less columns are never updated to have the new column count. Logically, this is fine, since the extra entries would just be Empty
anyways, but our pretty printer would print this table like so:
--------------------------------------------
|| Fahrenheit || Celsius || Rankine ||
--------------------------------------------
|| 100.0 |> 37.8 ||
|| || 100.0 |> 671.7 ||
--------------------------------------------
As you add more and more columns, the problem gets worse and worse. Enter our normalizeRowLen
function:
normalizeRowLen len rows = map (nRL' len) rows
where nRL' len' row
| (length row) < len' = nRL' len' (row ++ [Empty])
| otherwise = row
This is another fairly straightforward function. If the row has the same number of columns as the header, it is returned unchanged. If it doesn’t, Empty
is added to the end until it does.
With that, our program is complete. Let’s try it out:
main = do k <- return (toConversion $ Kelvin 100 :: (Kelvin, Rankine))
f <- return (toConversion $ Fahrenheit 451 :: (Fahrenheit, Kelvin))
r <- return (toConversion $ Rankine 234 :: (Rankine, Celsius))
c <- return (toConversion $ Celsius 9 :: (Celsius, Fahrenheit))
nc <- return (toConversion $ Rankine 123 :: (Rankine, Rankine))
putStrLn $ prettyPrint $ buildTable $ do insertConv k
insertConv f
insertConv r
insertConv c
insertConv nc
In our main
, we create a bunch of conversions. Then we prettyPrint
them and putStrLn
the result. The following will be printed to the console:
----------------------------------------------------------
|| Kelvin || Rankine || Fahrenheit || Celsius ||
----------------------------------------------------------
|| 100.0 |> 180.0 || || ||
|> 505.9 || || 451.0 || ||
|| || 234.0 || |> -143.2 ||
|| || |> 48.2 || 9.0 ||
|| || 123.0 || || ||
----------------------------------------------------------
Any type that implements Temperature
can be put into a table this way. To add a new unit to the program, it’s as easy as implementing four one-line functions!
On ArrayLists and Vectors
Long ago, when I first started doing Java, I struggled against Java’s limitations regarding the resizing of arrays. Eventually after poking around for solutions, I found the ArrayList
. Before that, I found the Vector
, but for whatever reason, NetBeans was saying that Vector
was deprecated, so I settled on ArrayList
, and it was fine.
A few years later, I took my first class on C++, and learned about the std::vector
. I was also introduced to the concepts of the vector and the linked list. Needless to say, I was confused. If vectors and linked lists aren’t the same thing, then what is this ArrayList
thing? At the time, I elected not to pursue the question, needing to focus on figuring out these “pointer” things they were making us learn. I put it out of my mind.
Flash forward to today. This morning I was travelling the internet, and I came across a forum thread. The topic of the ArrayList
came up. Curiosity finally overcame me, and I looked into the issue.
So, About Those ArrayLists…
The Java Collections framework is broken up into various datatype interfaces. There is an interface for lists, queues, maps, sets, and deqeues.
You’ll notice that there is no vector interface. While a list and an array have different semantics and use cases, you can use them roughly in the same way. “Array indexing” can be implemented on a list by iterating to the nth node, and arrays can be traversed like a list. Since there’s nothing a list can do that a vector can’t and vice versa, it follows that they can both implement the same interface. Sun had to make a choice: name that interface “list” or “vector”. They went with list.
Given that Java’s vector type implements the list interface, it follows that they would reflect that in the name: ArrayList
. For all intents and purposes, ArrayList
is equivalent to C++’s std::vector
. ArrayList
implements the Collections framework’s list interface, but it is a growable array. It behaves like a vector, indexing is cheap, resizing is expensive. Java also provides a LinkedList
that behaves like a linked list.
So, what about Java’s Vector
? It seems that Vector
predates the Collections framework. After the introduction of the Collections framework Vector
was retrofitted to be a part of it, also implementing the list interface. So, what’s the difference between ArrayList
and Vector
? Vector
is synchronized, and therefore is safe to use in threaded code. Due to this it is significantly slower than ArrayList
.
Simply put: use ArrayList
in single-threaded code, and Vector
in multi-threaded code.
Why Names Matter
This is why names matter. One might not think much of it, but imagine how many hiring managers would be out an interview question if ArrayList
and Vector
had been named Vector
and SynchronizedVector
respectively?
List as a Monad
Much ink has been spilled on the subject of “Lists as Monads”. Just the fact that they are of course, not what it means for you. This doesn’t really seem surprising to me; there are better monads to use to describe how monads work. Additionally, lists have their own special functions for working with them; you don’t fmap
a list, you just call map
.
Presumably, Lists as Monads is something that seasoned Monadimancers understand. Maybe it’s some sort of rite of passage. But no more. Today I’ll shed light on the arcane mysteries of Lists as Monads.
Motivation
But first we need a problem to solve. For my example I’ll be using the cartesian product of two lists. The cartesian product of two sets (we’ll be using lists) is defined as:
A X B is the set of all ordered pairs (a, b) such that:
a is a member of set A and
b is a member of set B
…translated into Haskell we should get a function with the following signature:
cartProd :: [a] -> [b] -> [(a, b)]
How might this function look? Well, we’d need three functions. The first function should have the signature:
cartProd'' :: a -> b -> (a, b)
This function is pretty straight forward, it pairs an a
and a b
. Next we’d need the function:
cartProd' :: [b] -> a -> [(a, b)]
This function maps (cartProd'' a)
over b
, producing the list [(a, b)]
. Finally, we need a function to tie it all together:
cartProd :: [a] -> [b] -> [(a, b)]
This function maps (cartProd' b)
over a
, then concat
s the resulting list of lists. An implementation might look like this:
cartProd :: [a] -> [b] -> [(a, b)]
cartProd l r = concat $ map (cartProd'' r) l
where cartProd' :: [b] -> a -> [(a, b)]
cartProd' r l = map (cartProd''' l) r
where cartProd'' :: a -> b -> (a, b)
cartProd'' l r = (l, r)
Did you go cross-eyed? Not exactly the most concise function that’s ever been written. Surely there is a better way…
Binding Our Lists
You may remember a few weeks back I talked about using the Maybe Monad. The gist of that post being that if you’re inside a do
block, you can treat your Maybe
as if it were just a plain value. It turns out that we can do something similar with Lists.
The Monad
instance for []
is somewhat complicated, but it’s operation is straight forward. If >>=
takes a Monad a
, a function that takes an a
and returns a Monad b
, and returns a Monad b
, what happens if we bind a simple function to [1]
?
Prelude> [1] >>= (\a -> return $ a + 1)
[2]
…ok, so it added 1 to 1, and stuffed it into a list. Seems pretty straight forward. Let’s try something a little more complicated:
Prelude> [1, 2] >>= (\a -> return $ a + 1)
[2,3]
…so this time it added 1 to each list node, as if we’d called map ((+) 1) [1, 2]
. Let’s try something else:
Prelude> [1] >>= (\a -> [(a + 1), (a - 1)])
[2,0]
…this time we tried it in reverse. We bound [1]
to a function that returns a list with two elements. The resulting list contained two elements. Again, nothing ground breaking here, but what if we do both?
Prelude> [1, 2] >>= (\a -> [(a + 1), (a - 1)])
[2,0,3,1]
…now we get a list with four elements: 1+1, 1-1, 2+1, and 2-1. To replicate this behavior we can’t just map the lambda over the original list. We need to add a call to concat. Let’s expand this our a bit further:
Prelude> [1, 2] >>= (\a -> [(a + 1), (a - 1)]) >>= (\b -> [b, b])
[2,2,0,0,3,3,1,1]
…all simple functions, but if we were to try to do this without the use of List’s monadic functions it’d become a mess like my cartProd
function. Speaking of which…
The Better Way
Getting back to our original topic. Now that we have a feel for how List’s monadic interface works, how could we re-implement cartProd
to not be terrible? Simple:
cartProd :: [a] -> [b] -> [(a, b)]
cartProd l r = do l' <- l
r' <- r
[(l', r')]
I’m often hesitant to toot my own horn and call something I wrote “elegant”, but it’s hard to argue that this function isn’t. In three short lines, I managed to re-implement that nested monstrosity I wrote before. There is one fairly massive gotcha here…
In the first and second lines, we bind our two lists to a label. It’s important to note that the order of these matters. The lists will be cycled through from the bottom up. Meaning that for each element of l, all elements of r will be evaluated. For example, using our cartProd
:
Prelude> cartProd [1,2] [3,4]
[(1,3),(1,4),(2,3),(2,4)]
1 is paired with 3, then 1 is paired with 4, then 2 is paired with 3 and 2 is paired with 4. Were we to swap the order in which we bind l and r to look like this:
cartProd :: [a] -> [b] -> [(a, b)]
cartProd l r = do r' <- r
l' <- l
[(l', r')]
Then the output would look like this:
Prelude> cartProd [1,2] [3,4]
[(1,3),(2,3),(1,4),(2,4)]
1 is paired with 3, then 2 is paired with 3, then 1 is paired with 4, then 2 is paired with 4. Before the first element of the tuple was grouped together where here the second element is. For our purposes, both results are valid per the definition of cartesian product, but that may not hold for you so be careful.