Coming Up‎ > ‎

November Meetup - 06.10.2012

posted 22 Oct 2012, 05:33 by Ed Lambda   [ updated 22 Oct 2012, 05:36 ]
Who: Robert Atkey
When: 6th November, 7pm @ The Outhouse pub

Title: "Theorems for Free"

Static type systems for programming languages have several well-known benefits: the eradication of certain classes of bugs at compile time, the use of types as machine-checked documentation, and the use of types as a high-level design language.

A less well-known benefit of static type systems is the automatic derivation of useful properties of programs just from their types. These properties often exploit the uniform behaviour that polymorphic programs have when instantiated at different types. For example, functions that have the (Haskell) type:
  h : forall a. [a] -> [a]
will (nearly (*)) always satisfy the following property:
  forall types a, b.
     forall f : a -> b.
       forall l : [a].
         h (map f l) = map f (h l)

Intuitively, this property holds because 'h' must "act the same" whether the input type is '[a]' or '[b]'. This kind of property can be used to rewrite programs for optimisation purposes, for example.

(*) nearly: this gets more complicated when non-termination and 'seq' are taken into account.

This property of the function 'h' can be deduced purely from its type alone, without looking at the actual implementation. Hence, Wadler called these properties "Theorems for Free" [1].

I'll talk about the different kinds of Theorems for Free that one can obtain, and what uses they can be put to. I'll also talk about some recent work [2] that applies the Theorems for Free idea to programs that manipulate geometric data, providing free theorems that state how the behaviour of programs can be invariant under geometric transformations like scaling, rotating and translation.

[1] Wadler, P. "Theorems for Free!"

[2] Atkey, R., Johann, P., Kennedy, A.. "Abstraction and Invariance for Algebraically Indexed Types"