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!
Haskell
Developing Programs and Proofs Spontaneously using GADT
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.
Encoding Inductive and Coinductive Types in Polymorphic Lambda Calculus
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.
Polymorphic Types in Haskell without Constructors?
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.
Zipping Half of a List with Its Reversal
Given a list, zip its first half with the reverse of its second half, in only “one and a half” traversals of the list.
Countdown: a case study in origami programming
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]
Quantum functional programming
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
A Haskell quine. That is, a program whose output is itself.