## How to Compute Fibonacci Numbers?

Some inductive proofs and some light program derivation about Fibonacci numbers. If you think the fastest way to compute Fibonacci numbers is by a closed-form formula, you should read on!

Skip to content
# Haskell

## How to Compute Fibonacci Numbers?

## Developing Programs and Proofs Spontaneously using GADT

## Encoding Inductive and Coinductive Types in Polymorphic Lambda Calculus

## Polymorphic Types in Haskell without Constructors?

## Zipping Half of a List with Its Reversal

## Countdown: a case study in origami programming

## Quantum functional programming

## A Haskell Quine

Some inductive proofs and some light program derivation about Fibonacci numbers. If you think the fastest way to compute Fibonacci numbers is by a closed-form formula, you should read on!

I am curious about the possibility of developing Haskell programs spontaneously with proofs about their properties and have the type checker verify the proofs for us, in a way one would do in a dependently typed language. I tried to redo part of the merge-sort example in Altenkirch, McBride, and McKinna’s introduction to Epigram: deal the input list into a binary tree, and fold the tree by the function merging two sorted lists into one.

An indcutive type μF is simulated by ` forall x . (F x -> x) -> x`

, while a coinductive type νF is simulatd by ` exists x . (x -> F x, x)`

. When they coincide, we can build hylomorphisms, but also introduces non-termination into the language.

I was trying to simulate church numerals and primitive recursion in second rank polymorphism of Haskell. However, polymorphic types in Haskell can only be instantiated with monomorphic types.

Given a list, zip its first half with the reverse of its second half, in only “one and a half” traversals of the list.

R. S. Bird and S-C. Mu, Countdown: a case study in origami programming. In *Journal of Functional Programming Vol. 15(5)*, pp. 679-702, 2005.

[GZipped Postscript]

S-C. Mu and R. S. Bird, Quantum functional programming. In *2nd Asian Workshop on Programming Languages and Systems* , KAIST, Dajeaon, Korea, December 17-18, 2001.

[GZipped Postscript]

A Haskell quine. That is, a program whose output is itself.