On Wed, Dec 30, 2009 at 1:12 PM, Mads Lindstrøm
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