blog

The task is to write a program that computes Fibonacci numbers such that it is obvious the program is correct. It's a sort of "Fibonacci readable" benchmark, and I contend to there exists no solution written in an imperative style that is satisfactory.

Our first functional solution is in Haskell. I like this one because it makes it obvious that memoization will occur, plus it's a pretty cute demonstration of laziness.

fib :: Int -> Int
fib n = fibs !! n
    where fibs = 1 : 1 : zipWith (+) fibs (tail fibs)

Idris brings something to the table too: guaranteed termination. We could do this in Haskell too, but as there is no support for Peano arithmetic in base, it seems wise to avoid it. Idris' totality checking is also more thorough than what Haskell does, even with the appropriate compiler flags.

fib : Nat -> Nat
fib Z = S Z
fib (S Z) = S Z
fib (S (S k)) = fib (S k) + fib k

ATS is a beautifully iconoclastic language, and our fib example is no different. The is an unabashedly functional approach with the speed of C. We check for termination (as we did in Idris) though strictly speaking that is optional in ATS.

fnx fib { n : int | n >= 0 } .<n>. (i : int(n)) : int =
  case+ i of
    | _ when i - 2 >= 0 => ( fib(i-1) + fib(i-2) )
    | _ => 1

Finally, I found this example kind of amusing. Sixten doesn't yet have strings literals, nor does it have infix operators. But it's still clearer than any solution you can write in Ruby.

fib : Int -> Int
fib 0 = 1
fib 1 = 1
fib n = addInt (fib (subInt n 1)) (fib (subInt n 2))

You can check out some of the imperative solutions proposed here.