Haskell 98 + Hierarchical modules is pretty much feature complete as far as I'm concerned. I realise that most people would demand to add higher ranked types and multi-parameter type classes, but the only extension I'm crying out for is pattern guards.

However, there is one operation that I think would be useful - pattern equality.

Consider the data type:

> type RegExp = [Atom]

> data Atom = Atom String | Star String

Now imagine you want to check that all atoms in a regular expression are Star's. Easy enough in Haskell:

> all isStar r

Unfortunately the definition of isStar - something that is conceptually very simple - is rather verbose:

> isStar (Star _) = True

> isStar _ = False

The reason is that in Haskell pattern matching is used to control program flow, not as an expression. One extension I often find myself wanting is some kind of "pattern match equality". Stealing the ~= operator for the moment, imagine:

> all (~= Star _) r

The ~= operator can be seen as pattern equality. It can be given a very simple semantics:

> x ~= y === case x of {y -> True; _ -> False}

Of course, now you've got pattern matching in there, its natural to allow fuller pattern matching:

> all (~= Star x | null x) r

Note that the original pattern match desugaring still allows this to be valid.

What do people think of this suggestion? Do people think it would be generally useful?

Disclaimer: This is not a carefully thought out feature proposal. Stealing ~= for syntax is completely unacceptable, something like <- would have to be chosen, if the grammar rules would permit it.

## Tuesday, February 13, 2007

## Wednesday, February 07, 2007

### Logical implication in Haskell

Logical implication is a common enough operator, usually written "a => b" for a implies b. Haskell doesn't feature a => operator, it would be a syntax error because that symbol is reserved for class constraints. Both QuickCheck and SmallCheck feature incompatible ==> operators for implication.

But Haskell does provide a boolean implication operator, namely (<=)! Yes, by writing the implication symbol backwards, you get standard forward implication!

But Haskell does provide a boolean implication operator, namely (<=)! Yes, by writing the implication symbol backwards, you get standard forward implication!

## Sunday, February 04, 2007

### Haskell and Set Theory

As part of my PhD, one thing I've been doing recently is specifying and working with set theory operations. Haskell is the perfect language for this, because in most cases the set theory can be implemented almost directly. Let's take a few examples to show how neat Haskell is at this.

I've done all the set theory in LaTeX - I guess most people who know set theory probably know LaTeX as well! I've also used xs/ys for sets, and x/y for elements from the sets. Although this isn't the way most mathematics would have been written, it does actually make it a bit more readable with some explicit typing :)

Subset

Subset is defined as:

xs \subset ys = \forall x \in xs, x \in ys

subset xs ys = all (\x -> x `elem` ys) xs

subset xs ys = all (`elem` ys) xs

The first version is the direct translation. We can of course make Haskell a bit closer to set theory with:

forAll = flip all

Now we have:

subset xs ys = forAll xs (`elem` ys)

That is a pretty direct translation of the mathematics.

Cross-product

One operation I wanted to specify recently was:

merge xs ys = { c | \exists x \in xs, \exists y \in ys, c = x <> y}

(where <> is an operation I had defined myself)

This time you can use Haskell's list comprehensions to obtain a translation:

merge xs ys = [x <> y | x <- xs, y <- ys]

In this case the Haskell is actually shorter the the corresponding mathematics.

Conclusion

I could give more examples of where the mathematics and the Haskell overlap closely, but they are almost too easy.

Almost every piece of set theory that I've tried to define in Haskell comes out looking very much like the original. This closeness allows me to work in mathematics, and then translate things to Haskell easily without worrying about having made mistakes in the translation.

The facilities of Haskell that make the set theory translation so direct include:

I've done all the set theory in LaTeX - I guess most people who know set theory probably know LaTeX as well! I've also used xs/ys for sets, and x/y for elements from the sets. Although this isn't the way most mathematics would have been written, it does actually make it a bit more readable with some explicit typing :)

Subset

Subset is defined as:

xs \subset ys = \forall x \in xs, x \in ys

subset xs ys = all (\x -> x `elem` ys) xs

subset xs ys = all (`elem` ys) xs

The first version is the direct translation. We can of course make Haskell a bit closer to set theory with:

forAll = flip all

Now we have:

subset xs ys = forAll xs (`elem` ys)

That is a pretty direct translation of the mathematics.

Cross-product

One operation I wanted to specify recently was:

merge xs ys = { c | \exists x \in xs, \exists y \in ys, c = x <> y}

(where <> is an operation I had defined myself)

This time you can use Haskell's list comprehensions to obtain a translation:

merge xs ys = [x <> y | x <- xs, y <- ys]

In this case the Haskell is actually shorter the the corresponding mathematics.

Conclusion

I could give more examples of where the mathematics and the Haskell overlap closely, but they are almost too easy.

Almost every piece of set theory that I've tried to define in Haskell comes out looking very much like the original. This closeness allows me to work in mathematics, and then translate things to Haskell easily without worrying about having made mistakes in the translation.

The facilities of Haskell that make the set theory translation so direct include:

- Higher order functions (i.e. all, forAll)
- Sections (`elem` xs) being equal to \x -> elem x xs
- Infix operators such as + and `elem`, along with priorities
- Beautiful syntax
- Lazy evaluation can make some operators more efficient (but is not incredibly important)

Subscribe to:
Posts (Atom)