Rubrication

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...

In my last post I described how unbelievably cool modules are in Coq. Well it turns out that there is some disagreement in the community about whether one should even use them! Why? Because the type system in Coq is so powerful we hardly even need them. In fact with a bit of syntactic sugar for inductively defined types and the generation of constructors we magically get something like first class modules (first-class meaning modules that are actually values that can be passed around to functions etc...). Enter the Record. Record MonadBind : Type := { M : forall (A : Type), Type; bind : forall (A B : Type), M A -> (A -> M B) -> M B; ret : forall (A : Type), A -> M A; left_unit : forall (A B : Type) (f : A -> M B) (a : A), bind A B (ret A a) f = f a; right_unit : forall (A B : Type) (m : M A), bind A A m (ret A) = m; bind_assoc : forall (A B C : Type) (m : M A) (f : A -> M B) (g : B -> M C) (x : B), bind B C (bi...

I've been playing with the Coq proof assistant over the past few days, following closely on some frustrations that I've been having with using SML's module system and a bit of toying with type-classes in Haskell. The gist of the problem is this. Although you can define type-classes and modules such that external users of these modules/type-classes see a uniform interface, consistency is left as an exercise for the implementer. This is not really acceptable in my view. When you are writing software, often times *you* are the implementer. What you really want is for these modules not just to provide a consistent interface to outsiders, but to guarantee the correctness of the implementation! Isn't that the whole point of types? If we can't do that, why are we using types? Ok, so in Coq I *can* get the properties I've been wanting out of SML's module system. For instance take the following implementation of the Monad signature: Module Type MONAD. S...