Reference types

[C T McBride]

Hi Simon

On Tue, 5 Feb 2002, Simon Peyton-Jones wrote:

> 2.  I'd be interested to know of any other examples you have of
>     *bi-directional* functional depenencies.  The above simplification
>     nukes my only convincing example.  (Usually one set of
>     type variables determines another, but not vice versa.)

The kind of programming I do at the type level in `Faking It'

  http://www.dur.ac.uk/c.t.mcbride/faking.ps

is fairly ordinary recursive programming on datatype expressions
using type classes with functional dependencies.  Just as many logic
programs have more than one functional (or partial-functional) mode,
so do many type class programs.

An artificial, but simple example

> data Empty

> class Add x y z | x y -> z, z x -> y

> instance Add Empty y y

> instance Add x y z => Add (Maybe x) y (Maybe z)

The two functional dependencies indicate that the compiler can be expected
either to add or to subtract in order to determine a missing instance
variable.

Of course, depending on the types of the operations for which Add is used,
not all of the possible functional dependencies may be relevant. There
is one example in `Faking It'---zipWith for vectors---which requires two
such dependencies. I'm sure I've got some other examples lurking
about; these things do pop up.

Whether such examples are `convincing' is another matter. Type-level
functional programming is a rather bizarre application of the class
system. I nonetheless find it very useful; I just wish type-level
functional programming was a less bizarre application of something rather
more like functional programming. 

Cheers

Conor