Hi A function inc5 inc5 :: Float -> Float inc5 x = x + 5 can only be a member of a type class A, if we make all functions from Float -> Float members of type class A. Thus, I assume, that _type_ class is named type class, as membership is decided by types. However, it makes no sense to say that all functions from Float -> Float are invertible or continuous. We would want to specifically say that inc5 is continuous, not all Float -> Float functions. Thus, we could have another abstraction, lets call it _value_ class, where we could say that an individual value (function) could be member. We could say something like: class Invertible (f :: a -> a) where invert :: f -> (a -> a) instance Invertible inc5 where invert _ = \x -> x - 5 In many cases this would be too specific. We would like to say, that applying the first argument to `+` returns an invertible function. Something like: instance Invertible (`+` x) where invert (x +) = \y -> y - x We would properly also like to say, that composing two invertible functions results in another invertible function. I guess there are many more examples. 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. /Mads Lindstrøm
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
Mads Lindstrøm schrieb:
Hi
A function inc5
inc5 :: Float -> Float inc5 x = x + 5
can only be a member of a type class A, if we make all functions from Float -> Float members of type class A. Thus, I assume, that _type_ class is named type class, as membership is decided by types.
However, it makes no sense to say that all functions from Float -> Float are invertible or continuous. We would want to specifically say that inc5 is continuous, not all Float -> Float functions. Thus, we could have another abstraction, lets call it _value_ class, where we could say that an individual value (function) could be member. We could say something like:
class Invertible (f :: a -> a) where invert :: f -> (a -> a)
instance Invertible inc5 where invert _ = \x -> x - 5
In many cases this would be too specific. We would like to say, that applying the first argument to `+` returns an invertible function. Something like:
instance Invertible (`+` x) where invert (x +) = \y -> y - x
We would properly also like to say, that composing two invertible functions results in another invertible function. I guess there are many more examples.
Maybe you could define types like newtype InvertibleFunction a b = InvertibleFunction (a -> b) newtype ContinuousFunction a b = ContinuousFunction (a -> b) or newtype AttributedFunction attr a b = AttributedFunction a b where attr can be Invertible, Continuous, or (Invertible, Continuous). Then you may define a type class that provides a functional inverse, if attr shows invertibility.
participants (3)
-
Henning Thielemann -
Luke Palmer -
Mads Lindstrøm