Rubrication

I've been working with System F quite a bit lately, as it has a complicated enough typing system to be interesting, without having the full insanity of dependent types. I've been working with System F including sums products and recursive types. However, all of these can actually be encoded directly in System F. At first I thought this was merely a curiosity. It turns out however that for recursive types, the built in variety has some serious advantages. System F allows you to take types as arguments as well as terms. From this system you can weave together an impressive array of very expressive types. First I'll define a few of these, and then I'll further describe what I find really fascinating. The basic idea is that we can apply a function such as (Λ X . λ f : X→X, x : X. f x) to some types and terms and we evaluate in a way analogous to the λ-Calculus: (Λ X . λ f : X→X, x : X. f x) [T] g t ⇒ g t Now lets look at how w...

Standard functional programming languages like Haskell and SML use polymorphic type systems. These type systems however, are not sound. What this means is that the type-systems themselves can not be used to prove properties of the software in the sense of "total correctness". To see that this is true, we can get a "proof" (read program) of inhabitation of any arbitrary type A, by simply using the program: data Bot {- Look Ma! No constructors! -} bot :: Bot bot = bot Clearly when we say that bot is an inhabitant of Bot, we dont mean that it actually produces a value of type Bot, since there aren't any as Bot has no constructors! We can easily use this type of proof to prove something like A ∧ ¬ A which leads to a pretty degenerate logic. However, the type system is still *useful* in the sense that if the program ever *does* terminate, it's sure to do so with the appropriate type. This means we can get the full class of Turing complete programs, a...

I was playing around with the Peano numerals in Haskell (as I often do), because I remember briefly reading about a generalisation of exponentiation in a paper once when I didn't have time to read it. I decided I'd quickly look at it again now that I was in a mood to procrastinate. > data Nat = Z | S Nat deriving Show This data type is usually identified with the peano numerals. In fact as we will see, in haskell it isn't quite the natural numbers. We take Z to mean 0 and take (S n Z) or (S (S (S ... Z))) n times, to mean n. It's basically a unary number system where the length of the string gives us the number. It is pretty straightforward to write the basic arithmetic operations on the peano numerals. > add x Z = x > add x ( S y ) = S ( add x y ) > mult x Z = Z > mult x ( S y ) = add x ( mult x y ) > expt x Z = ( S Z ) > expt x ( S y ) = mult x ( expt x y ) Here we can see an extension of this series fairly easil...

A while ago I wrote a post about how one can use coq to make a proper monad module. I was just thinking today that it would be nice to have a tool for haskell that would allow one to write down conjectures and discharge them automatically with a theorem prover. Supercompilation makes a nice clean theorem prover for haskell since one could express the equations of interest in haskell itself. Below is an example of the list monad, and then the 3 monad laws written as conj1,conj2 and conj3. I prove the first law by manual supercompilation. The next two are left as an exercise for the interested reader. equal xs ys = case xs of [] -> case ys of [] -> True _ -> False (x:xs') -> case ys of [] -> False (y:ys') -> case (eq x y) of False -> False ...

Program transformation is a sort of meta-compilation where the source and target languages are the same. In this sense it can be seen as an automorphism on the set of programs in a language. As was pointed out by Turchin, it is sometimes possible to prove properties of programs simply by performing a program transformation. Basically a program, and a program which verifies it's behaviour (a predicate) can be replaced with a truth value if the program transformation is sufficiently powerful. An obvious example of course, which can be calculated using partial evaluation would be something like (max (< 3) (1::2::1::nil)). In fact very complex properties can be proved automatically by Distillation, a particularly powerful program transformation system. In my research I've been working with the μ-Calculus, which is a type of temporal logic that is very powerful (LTL, CTL, CTL* can all be embedded in the μ-Calculus) and good for describing reactive systems. It uses a noti...

I've lately been working on my disertation concering a program transformation technique known as Distillation. Distillation is a technique inspired by supercompilation. Supercompilation involves mapping terms from a particular language to other terms of the same language. It can be though of as a semantics preserving rewriting system, or a function which maps terms to other terms which are equal modulo some semantic interpretation relation. A really strait-forward description of supercompilation is given by XXX on his paper on supercompilation for Haskell. This work leverages work by Gluck and Sorenson but presents generalisation in a very clear and declarative way, which is a notable exception to most of the literature in this field. Generalisation is actually quite a tricky problem. Generalisation has some of the same problems as the old problem with standards. That is, the thing about standards is that there are so many to chose from. It takes quite a bit of effort to ...

I've mentioned a number of times that given a sufficiently rich type theory we can use the type to provide a specification for the function, such that the function is correct by construction. I'd like to give a simple example of how this works in the Coq proof assistant. The following code is an illustration of how the type theory of Coq allows you to fully specify the behaviour of functions. Kragen Sitaker made the comment that there weren't too many reasonable interpretations of the function of the type given to the assoc function: A -> list (A * B) -> option B that is, a function taking an element of type A, a list of pairs of A and B, to the possibility of a B (and possible failure). That got me wondering how hard it would be to tighten the noose so that there was only one way to interpret the type but still possibly many implementations that satisfy the type, all of which will yield the same result. The following code illustrates that this is indeed p...