[Haskell-cafe] Value classes

[Luke Palmer]

On Wed, Dec 30, 2009 at 1:12 PM, Mads Lindstrøm
<mads_lindstroem at yahoo.dk> wrote:
> This idea, of value classes, do not feel all that novel. Somebody has
> properly thought about it before, but gave it a different name. If
> anybody has links to some papers it would be much appreciated. If
> anybody has some thoughts of the desirability of value class it would
> also be much appreciated.

Yes, it would be nice.  But there is a problem: implementing it would
require higher-order unification, or in the simplest case, comparing
functions for equality, neither of which are decidable.  I.e. if you
wanted to say:

add5 x = x + 5
instance Invertible add5 where ...

Suppose (+) were not a primitive, but implemented in terms of some
other operations. Then you would have to somehow "reroll" a function
to express it in terms of (+), and it isn't obvious how to do this
(not obvious to the extent that it is not possible in general!).

The obvious solution is to assume that \x -> x + 5 is not invertible,
but add5 is... despite them being equal.  This is an obvious violation
of referential transparency (replacing add5 by its definition would
break code).  However, if you are willing to throw out that property,
it might be interesting to explore the ramifications of this.

Proof-oriented languages like Agda and Coq would take a different
approach.  Rather than Invertible being a property that is reduced,
you have another type -- invertible : forall a, (a -> a) -> Prop --
which is the type of *proofs* that a function is invertible.  Now you
have something tangible, and you can have values whose types are
theorems:

compose : forall f g, invertible f -> invertible g -> invertible (f . g)

Though it looks like a theorem, it is a function from proofs that f is
invertible and proofs that g is invertible to proofs that f . g is
invertible.  This is important, because the user needs to specify the
flow of information through the proof, something a computer cannot
(yet) do automatically.  Reasoning this way has the same effect as
your "value classes", but mind it is *much* more complicated to use.
If only we could solve those undecidable problems :-P

In any case, the way I would do this in Haskell is to make a type and
operations for invertible functions:

data Invertible a b = Inv (a -> b) (b -> a)

apply :: Invertible a b -> a -> b
apply (Inv f f') = f
inverse :: Invertible a b -> Invertible b a
inverse (Inv f f') = Inv f' f
compose :: Invertible b c -> Invertible a b -> Invertible a c
compose (Inv f f') (Inv g g') = Inv (f . g) (g' . f')

The tricky part here is ensuring that the two arguments of Inv are, in
fact, inverses.  There are various ways to solve that, with varying
levels of assurance.  But "value classes" had the same problem; you
could have said:

instance Invertible add5 where
    inverse x = x - 3

And the compiler would have gone right ahead and trusted you.

Luke