I've seen a couple of messages now about Simon's proposal for
a RULES mechanism in Haskell, but it's clear that I've missed
several of the messages, including the original proposal. I
suspect this is a result of recent changes in the way that the
list is handled, which should be resolved by now. Unfortunately,
the missing articles are also not available from the archive at
haskell.org.
[Aside: As a general comment to all readers of the Haskell mailing
list, perhaps I can suggest: if you've posted something to the list
within the last two weeks, and it hasn't received the kind of
response that you were expecting, then please consider reposting,
as many of us may have missed it the first time round. Thanks!]
Returning to the main subject of this posting ... the idea of adding
rules to class declarations has been around for a long time. In fact
the original Wadler and Blott paper that introduced type classes
(How to make ad-hoc polymorphism less ad-hoc) hints briefly at this
exact idea in its conclusions. Later, in the closing section of my
own paper on Computing with Lattices (JFP 2, 4, 1992), I wrote about
this in a little more detail, and observed that extending the syntax
of Haskell to include rules would allow rules to be type checked and/or
fed as input to a proof checker.
Shortly after that, in a joint report with Luc Duponcheel on `Composing
Monads' (http://www.cse.ogi.edu/~mpj/pubs/composing.html), we used an
uninterpreted === operator to state the monad laws directly in Haskell
notation. The trick here was to define:
data Law a -- Uninterpreted data type
(===) :: a -> a -> Law a
x === y = error "uncomputable equality"
Now we can state laws such as the following:
mapId :: Functor f => Law (f a -> f a)
mapId = fmap id === id
mapCompose :: Functor f => (b -> c) -> (a -> b) -> Law (f a -> f c)
mapCompose f g = fmap f . fmap g === fmap (f . g)
Note that free variables in these laws are represented by variables on
the left hand side, with names like mapId and mapCompose serving as names
for each rule. Because these are treated as normal Haskell definitions,
they are also subjected to the same process of type checking and type
inference. I've written out explicit type signatures for these rules,
but they could also have been inferred from just the definition. There
is still a distinct benefit in having a compiler type check laws like this,
even if you take them no further, for example as a hint to optimizers or
as input to proof checkers. Note also that by embedding the laws in
Haskell, we get consistency in the type system ... Haskell has constructor
classes, and so this shows up in the laws: the above laws are intended to
hold for each instance of the "Functor" class, as reflected in the types.
Several observations:
- It might be nice to hide the === operator and the law datatype inside
a compiler so that they are truly uninterpreted. Also, one might add
a few additional operators and connectives.
- It might be nice to use a syntax that distinguishes laws from regular
function definitions. If this is done, then it will be easier for a
Haskell compiler will be able to identify laws as dead code, and for a
Haskell-->ProofChecker tool to identify the laws. The syntax that I
played with looked like the following:
MapCompose f g => fmap f . fmap g === fmap (f . g)
This doesn't cause any serious parsing conflicts ... it doesn't even
require any new input tokens!
- I think it is a mistake to use a syntax that embeds laws inside some
special comment pragma notation. Treating laws as proper language
objects has several advantages, not least being the ability to name
the laws, and control uses of that name (such as import or export from
a module) using precisely the same mechanisms that we have in the rest of
the language.
- Incorporating proofs into a script means defining an interpretation for
the Law datatype and associated operators. One could imagine having
several implementations of these, each targeted at a different prover
and/or logic. Lennart Augustsson has experimented with at least one
approach to this.
- Since I wrote about this in my Computing with Lattices paper, I have
realized that it is a mistake to think about laws as being *part of*
a class declaration. Laws should be allowed anywhere that a normal
declaration is permitted. There are several reasons for this:
* Laws are useful for values that are not overloaded, and hence
do not get defined in a class declaration.
* Most laws describe *interactions* between several operators, and not
just the properties of one operator. So the MapCompose law, for
example, is about the interaction of fmap and (.) and could equally
well be placed with the definition of (.), or even in a separate
module of useful laws.
* The values in a class declaration have top-level scope, and hence
so should any associated laws. As part of a language design, one
might decide to allow laws in a class declaration (or indeed in
any other position where a normal declaration is permitted), but
the scoping should be the same as for any other value defined in
the same place. (This is the same situation that we have with
fixity declarations in Haskell 98.)
I hope my comments here are of interest. I look forward to seeing the
messages that got all this started again, and I hope to hear more from
other interested parties!
All the best,
Mark
