Skip to main content

Posts

Showing posts from 2007

The type says everything

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

We don't need no stinking modules!

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

How a real module system should work

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

Coq

A few months ago I started messing around with The Coq Proof Assistant to figure out what exactly it was, and proceeded to go through the tutorial. Coq provides a nice interface for doing proofs in an interactive session. It was a lot of fun but didn't seem particularly useful for my research. As I've been playing with the notion of Total Functional Programming, I ended up reading (and actually doing homework) from a book entitled "Type Theory and Functional Programming" . This book is excellent by the way! I highly recommend it to anyone interested in dependent types/proof theory/type theory. It has a very lucid style and makes a lot of complex notions in type theory very easy to understand. I even got to find an error in one of the homework examples (now listed in the errata) which is always fun. After working through the first 5 chapters I started looking around for a system that would let me apply some of the principles that I had learned. As it tu

Protected access using lightweight capabilities

The following is some SML code that implements the natural numbers using peano arithmetic in the SML type system. These numbers can be used to protect access to list functions. I haven't yet figured out if addition is possible, but I'm hoping that it is. It could be really handy! signature SLIST = sig type 'a nat type Z type 'a S val S : 'a nat -> 'a S nat val P : 'a S nat -> 'a nat val Z : unit -> Z nat val zerop : 'a nat -> bool val toInt : 'a nat -> int type ('elt,'n) slist val snil : unit -> ('elt, Z nat) slist val scons : 'elt -> ('elt, 'n nat) slist -> ('elt, 'n S nat) slist val :+: : 'elt * ('elt, 'n nat) slist -> ('elt, 'n S nat) slist val shd : ('elt, 'n S nat) slist -> 'elt val stl : ('elt, 'n S nat) slist -> ('elt, 'n nat) slist val slen : ('elt, '

Automated Deduction and Functional Programming

I just got "ML for the working programmer" in the mail a few days ago, and worked through it at a breakneck pace since receiving it. It turns out that a lot of the stuff from the "Total Functional Programming" book is also in this one. Paulson goes through the use of structural recursion and extends the results by showing techniques for proving a large class of programs to be terminating. Work with co-algebras and bi-simulation didn't quite make it in, except for a brief mention about co-variant types leading to the possibility of a type: D := D → D which is the type of programs in the untyped lambda calculus, and hence liable to lead one into trouble. I have to say that having finished the book, this is the single most interesting programming book that I've read since "Paradigms of Artificial Intelligence Programming" and "Structure and Interpretation of Computer Programs". In fact, I would rate this one above the other

Total Functional Programming

Recently on Lambda the Ultimate there was a post called "Total Functional Programming".  The title didn't catch my eye particularly, but I tend to read the abstract of any paper that is posted there that doesn't sound terribly boring.  I've found that this is a fairly good strategy since I tend to get very few false positives this way and I'm too busy for false negatives. The paper touches directly and indirectly on subjects I've posted about here before.  The idea is basically to eschew the current dogma that programming languages should be Turing-complete, and run with the alternative to the end of supplying "Total Functional Programming" .  At first glance this might seem to be a paper aimed at "hair-shirt" wearing functional programming weenies.  My reading was somewhat different. Most hobbiest mathematicians have some passing familiarity with "Turing's Halting Problem" and the related "Goedel's Inco

Addition in the lambda calculus

I just spent a couple of very cold weeks in Anchorage Alaska.  I went out with a bunch of friends to a bar on the night prior to leaving, where I met up with an old friend (and listened to two other friends play music).  I started describing the lambda calculus to him since it is related to my work and he was curious what I was up to.  In any case I found myself unable to produce addition of the church numerals off the top of my head, which I found pretty disturbing since it shows that I probably didn't quite understand it in the first place.  Therefor I sat down this morning to see if I couldn't reconstruct it from first principles.  It turns out that it is relatively easy. First, let us start with a bit of notation, and a description of the lambda calculus .  Since wikipedia describes the lambda calculus in detail, I'll just show how one procedes with calculations.  As examples let us start with the church numerals .  1 = (λf x.f x) 2 = (λf x.f f x) 3 = (λf x.f f f