## Friday, March 16, 2012

### Tail recursion in Python

[Python-Dev] Proper tail recursion

If tail-call elimination is an optimization, it is the kind of optimization that you have to keep your eye on: if you've been writing your code thinking it's there, it better really be there. Tail-call elimination can make or break a program. Run a tail-recursive loop that services requests indefinitely, and you'll see it's not just an optimization whether the stack grows with each call.

Still, tail recursion is not everybody's style. As Guido says:

I don't think it's a good idea to try to encourage a Scheme-ish "solve everything with recursion" programming style in Python.

And there's the truth: Python's goal is to restrict your programming style. Why are the following awkward (albeit possible) in Python?

• Lazy evaluation

• Sum-of-product types (as in Haskell)

• Enforced private members / fix the set of fields for a class

• Tail recursion

• User-defined control structures (as in Scala or Ruby)

• User-defined literals, syntax, pattern matching, or any extention to the basic building blocks of the language.

They are awkward because there was another way of doing it, and, when there's more than one way of doing it, Python makes a choice.

Now, I must be honest, if every language took it upon itself to enforce a particular style I would not find that exquisitely pleasant. I am grateful that languages like Scala and C++ and Ruby exist. But I am also glad that we have at least one language we can reach for when we need a homogeneous style.

Personally, I turn to a functional style when I can. And, yes, the awkwardness of functional programming in Python does occasionally irritate me ("Python: As much Lisp as a C programmer can (under)stand." -- Nathan Sanders). But, at the end of the day, when I go to push my changes, that irritation is more than offset by a tiny feeling of confidence in the code I just wrote that someone else will understand it.

## Wednesday, March 14, 2012

### Agda as a Programming Language: Using Haskell for basically everything

Agda would not be useful if it had to reinvent all of its wheels. Luckily it is faily easy to use Haskell from Agda.

     wordcount.agda

1  module wordcount where
2
4  open import IO.Primitive renaming (putStrLn to putStrLnCo)
5  open import Data.List
6  open import Data.String
7  open import Function using (_∘_)
8
9  -- Data.Nat is unary. This is terribly inefficient. Ideally
10  -- we would use Haskell numbers, but that is not convenient.
11  open import Data.Nat
12
13  -- Data.Nat.Show was written before Agda had typeclass support.
14  open import Data.Nat.Show renaming (show to showNat)
15  open import Data.Char
16
17  putStrLn = putStrLnCo ∘ toCostring
18
19  infixl 1 _>>_
20  postulate
21      _>>_  : ∀ {a b} {A : Set a} {B : Set b} → IO A → (IO B) → IO B
22  {-# COMPILED _>>_  (\_ _ _ _ -> (>>)) #-}
23
24  module CmdlineArgs where
25      {-# IMPORT System #-}
26      postulate sysArgs : IO (List String)
27      {-# COMPILED sysArgs (System.getArgs) #-}
28
29  module FileIO where
30      {-# IMPORT System.IO #-}
31      postulate Handle : Set
32      {-# COMPILED_TYPE Handle System.IO.Handle #-}
33      postulate hGetLine : Handle -> IO String
34      {-# COMPILED hGetLine (System.IO.hGetLine) #-}
35      postulate hGetContents : Handle -> IO String
36      {-# COMPILED hGetContents (System.IO.hGetContents) #-}
37      postulate IOMode : Set
38      {-# COMPILED_TYPE IOMode System.IO.IOMode #-}
41      -- This won't work if it's not universe-polymorphic. I Don't know why.
42      postulate withFile : ∀ {u} {A : Set u} -> String -> IOMode -> (Handle -> IO A) -> IO A
43      {-# COMPILED withFile (\_ _ -> System.IO.withFile) #-}
44
45  open CmdlineArgs
46  open FileIO
47
48  wordsInString : String -> ℕ
49  wordsInString s = ws1 (toList s) where
50      mutual
51          ws1 : List Char -> ℕ
52          ws1 [] = 0
53          ws1 (' ' ∷ rest) = ws1 rest
54          ws1 (c ∷ cs) = suc (ws2 cs)
55
56          ws2 : List Char -> ℕ
57          ws2 [] = 0
58          ws2 (' ' ∷ rest) = ws1 rest
59          ws2 (c ∷ cs) = ws2 cs
60
61  -- Agda does not have case expressions, so we use a local
62  -- function to pattern match.
64  main = sysArgs >>= doArgs where
65      -- Agda's type inference is not as good as Haskell's;
66      -- We have to specify some amount of signature.
67      doArgs : _ -> _
68      doArgs (path ∷ []) =
69          withFile path ReadMode \hl ->
70              hGetContents hl >>= \text ->
71              let count = wordsInString text in
72              putStrLn (showNat count)
73      doArgs _ =
74          putStrLn "Usage: wordcount <filename>"



### Agda as a Programming Language: Hello World

While checking out Agda, I found a lot of information on using Agda to prove things, but very little on using Agda to write programs. So I will post here what I learn, and maybe it will help someone.

As to why you would use Agda to write programs, well, I had a reason, but that's for another day.

# Hello World

Agda keeps changing; the old Hello Worlds no longer compile (I have yet to find a single working example on the internet). After some struggle I managed to produce one:

     hello.agda

1  -- Compiles with Agda 2.3.0 and standard library 0.6
2  -- on 2012-03-13
3
4  module hello where
5
6  open import IO.Primitive
7  open import Data.String
8
10
12  main = putStrLn (toCostring "Hello, World!")



To run this program you will need:

Both of these can be installed with cabal.

Then run:

  1  agda -i <path to standard library source> -i . -c hello.agda
2  ./hello



So, in my case,

  1  agda -i ~/install/lib-0.6/src -i . -c hello.agda
2  ./hello



# Peculiarities of the program

• IO deals with Costrings rather than Strings (for some reason). A string literal is a String, so we convert it with toCostring. We could also have done:

  1  open import IO.Primitive renaming (putStrLn to putStrLnCo)
2
3  putStrLn : String -> Hask.Unit
4  putStrLn s = putStrLnCo (toCostring s)


• putStrLn is literally just the Haskell function of the same name; as such it returns Haskell's Unit type; Agda has its own Unit type (in Data.Unit), but these are not the same. So the result of main must be IO Foreign.Haskell.Unit.

• Agda has another IO library in IO; it might be better, but I didn't understand it, so I used IO.Primitive.

# More IO

     someio.agda

1  module someio where
2
4  open import IO.Primitive renaming (putStrLn to putStrLnCo)
5  open import Data.String
6  open import Function using (_∘_)
7
8  putStrLn = putStrLnCo ∘ toCostring
9
10  infixl 1 _>>_
11
12  postulate
13      _>>_  : ∀ {a b} {A : Set a} {B : Set b} → IO A → (IO B) → IO B
14      getLine : IO String
15
16  {-# COMPILED _>>_  (\_ _ _ _ -> (>>)) #-}
17  {-# COMPILED getLine (getLine) #-}
18
20  main =
21      putStrLn "Hello, World!" >>
22      putStrLn "Whatup!" >>
23      getLine >>= \up ->
24      putStrLn ("Your face is " ++ up)


• IO.Primitive does not define >>, so we do.
• (\_ _ _ _ -> (>>)) throws away the type arguments, because Haskell does not have type arguments.
• Agda has no do notation.

# The most useful Agda resources I have found

## Friday, March 9, 2012

### More on static typing

As I've said earlier, I find static typing aesthetically appealing but am skeptical about its practical value.

Type systems are the chemo of programming. They are designed to make things harder. You hope that most of what it does is make mistakes harder, but you know from experience that static typing introduces a grain of trickiness into everything.

What do people find so appealing about dynamic languages?:

You know, maybe the dynamic crowd just wants freedom to not have to think as carefully about what they're doing. The software might not be correct or robust, but maybe it doesn't have to be.

-- Apocalisp

The whole answer is very good, but the author has a fundamental misconception: that the only cases where a dynamic language admits a program that a static language rejects is when the program is incorrect. Consider that the following python code is perfectly correct:

a = [ ]
for i in range(0, 8, 2):
a.append(i)
for j in range(i): a.append('x')

print(a)

total = 0
i = 0
while i**2 < len(a):
total += a[i**2]
i += 1
print(total)


but that it would not pass a static type checker. You could of course struggle a long time to prove via the type system that the while loop accesses only those elements of a that happen to be numbers (you could probably do it, but it would be a long and painful journey). But more importantly, even if you don't do it, the code is still correct.

The difficulty of static type systems is not that they require your code to be more correct, but that they require you demonstrate its correctness in a certain way. That certain way is a pretty elegant one, but it is also a terribly specific one, and so there will always be correct code to which a static type system is poorly suited.

Unit testing statically typed functional code

Unit tests do introduce redundancy, which means that when requirements change, the code implementing them and the tests covering this code must both be changed. [...] given how statically typed functional programming covers a lot of the ground unit tests are intended for, it feels like it's a constant overhead one can simply reduce without penalty.

-- back2dos

Some of the bug-finding power of static typing comes from redundancy; in fact, if you want to catch inadvertant changes in behavior introduced by refactoring, you will need to specify explicit type signatures, which are redundant.

I wonder, are there any statically typed programming languages which provide tools to check whether the inferred type of a function changes across different versions of the code?

If you have specs which can be mapped directly to function declarations - fine. But typically those are two completely different levels of abstractions.

-- Doc Brown

Of course, in theory all levels of abstraction can be checked statically; but how many people are leet enough to actually do that? (Consider -- what would you need to do to write a statically verified sorting function). If unit tests can take you to 97% sure that your code is correct (and still correct after a refactoring), how much time are you willing to spend on that extra 3%?

## Thursday, March 8, 2012

### Thomas Carlyle on Agile

But indeed Conviction, were it never so excellent, is worthless till it convert itself into Conduct. Nay properly Conviction is not possible till then; inasmuch as all Speculation is by nature endless, formless, a vortex amid vortices: only by a felt indubitable certainty of Experience does it find any centre to revolve round, and so fashion itself into a system. ... Do the Duty which lies nearest thee, which though knowest to be a Duty! Thy second Duty will already have become clearer.

-- Thomas Carlyle in Sartor Resartus.