Tuesday, July 19, 2011

Random Functional/Math Readings

an optimization technique used primarily to speed up computer programs by having function calls avoid repeating the calculation of results for previously-processed inputs.


= Self-balancing Binary Search Tree


Type arithmetic (or type-level computation) are calculations on the type-level, often implemented in Haskell using functional dependencies to represent functions.
 data Zero
 data Succ a
 class Add a b ab | a b -> ab, a ab -> b
 instance Add Zero b b
 instance (Add a b ab) => Add (Succ a) b (Succ ab)

Functional dependencies are used to constrain the parameters of type classes

Peano numbers are a simple way of representing the natural numbers using only a zero value and a successor function.

The Curry–Howard correspondence is the direct relationship between computer programs and proofs in programming language theory and proof theory. Also known as Curry–Howard isomorphism, proofs-as-programs correspondence and formulae-as-types correspondence, it is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the American mathematician Haskell Curry and logician William Alvin Howard.