I've been wondering, is it ever possible to have two (extensionally) different Functor instances for the same type? I do mean in Haskell; i.e. (,) doesn't count. I've failed to either come up with any examples or prove that they all must be the same using the laws. Thanks, Luke
Luke Palmer wrote:
I've been wondering, is it ever possible to have two (extensionally) different Functor instances for the same type? I do mean in Haskell; i.e. (,) doesn't count. I've failed to either come up with any examples or prove that they all must be the same using the laws.
For "not-too-exotic" datatypes, in particular for algebraic data types with polynomial structure (no exponentials, embedded function types, and other nasties), I would conjecture that indeed there is always exactly one Functor instance satisfying the identity and composition laws. But for proving this the two equational laws would not be enough. Rather, one would also need to use that fmap must be sufficiently polymorphic. Basically, a proof by a version of free theorems, or equivalently in this case, properties of natural transformations. And no, I don't have a more constructive proof at the moment ;-) Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de
Janis Voigtlaender wrote:
Luke Palmer wrote:
I've been wondering, is it ever possible to have two (extensionally) different Functor instances for the same type? I do mean in Haskell; i.e. (,) doesn't count. I've failed to either come up with any examples or prove that they all must be the same using the laws.
For "not-too-exotic" datatypes, in particular for algebraic data types with polynomial structure (no exponentials, embedded function types, and other nasties), I would conjecture that indeed there is always exactly one Functor instance satisfying the identity and composition laws.
But for proving this the two equational laws would not be enough. Rather, one would also need to use that fmap must be sufficiently polymorphic. Basically, a proof by a version of free theorems, or equivalently in this case, properties of natural transformations.
And no, I don't have a more constructive proof at the moment ;-)
Let me be a bit more precise. A free theorem can be used to prove that any f :: (a -> b) -> [a] -> [b] which satisfies f id = id also satisfies f = map (for the Haskell standard map). Also, a free theorem can be used to prove that any f :: (a -> b) -> Tree a -> Tree b for data Tree a = Node (Tree a) (Tree a) | Leaf a which satisfies f id = id also satsifies f = fmap for the following definition: fmap f (Leaf a) = Leaf (f a) fmap f (Note t1 t2) = Node (fmap f t1) (fmap f t2) That gives the desired statement of "unique Functor instances" for the list type and the above Tree type. And the same kind of proof is possible for what I called "not-too-exotic" datatypes. And since all these proofs are essentially the same, it is no doubt possible to give a generic argument that provides the more general statement that for all such datatypes exactly one Functor instance exists. Makes sense? Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de
Janis Voigtlaender wrote:
A free theorem can be used to prove that any
f :: (a -> b) -> [a] -> [b]
which satisfies
f id = id
also satisfies
f = map (for the Haskell standard map).
Here comes the full proof. Feed http://linux.tcs.inf.tu-dresden.de/~voigt/ft/ with the type of f. The output is: For every f :: forall a b . (a -> b) -> [a] -> [b] holds: forall t1,t2 in TYPES, g :: t1 -> t2. forall t3,t4 in TYPES, h :: t3 -> t4. forall p :: t1 -> t3. forall q :: t2 -> t4. (forall x :: t1. h (p x) = q (g x)) ==> (forall y :: [t1]. map h (f p y) = f q (map g y)) Set p = id and g = id. It results: forall t3,t4 in TYPES, h :: t3 -> t4. forall q :: t3 -> t4. (forall x :: t3. h (id x) = q (id x)) ==> (forall y :: [t3]. map h (f id y) = f q (map id y)) The precondition is obviously fulfilled whenever h = q. So we get, for every h, forall y :: [t3]. map h (f id y) = f h (map id y) Now note that we assume f id = id, and also know map id = id. This gives: forall y :: [t3]. map h y = f h y This is the desired extensional equivalence of map and f. All we needed was a free theorem and the identity law. The same kind of proof works for the Tree type, and friends. Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de
Luke Palmer wrote:
I've been wondering, is it ever possible to have two (extensionally) different Functor instances for the same type? I do mean in Haskell; i.e. (,) doesn't count. I've failed to either come up with any examples or prove that they all must be the same using the laws.
For "not-too-exotic" datatypes, in particular for algebraic data types with polynomial structure (no exponentials, embedded function types, and other nasties), I would conjecture that indeed there is always exactly one Functor instance satisfying the identity and composition laws.
Are identity and composition sufficient to guarantee that the mapped function is actually applied? instance Functor f where fmap _ x = x fmap id fx ~ fx ~ id fx fmap f (fmap g fx) ~ fmap f fx ~ fx ~ fmap (f . g) fx Claus
Claus Reinke wrote:
Luke Palmer wrote:
I've been wondering, is it ever possible to have two (extensionally) different Functor instances for the same type? I do mean in Haskell; i.e. (,) doesn't count. I've failed to either come up with any examples or prove that they all must be the same using the laws.
For "not-too-exotic" datatypes, in particular for algebraic data types with polynomial structure (no exponentials, embedded function types, and other nasties), I would conjecture that indeed there is always exactly one Functor instance satisfying the identity and composition laws.
Are identity and composition sufficient to guarantee that the mapped function is actually applied?
instance Functor f where fmap _ x = x
Such an fmap will not have the required type (a -> b) -> f a -> f b Consider "fmap even". Then a=Int, b=Bool, x::f Int, (fmap even x)::f Bool, type error since you assumed fmap even x = x ! Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de
Luke Palmer
I've been wondering, is it ever possible to have two (extensionally) different Functor instances for the same type? I do mean in Haskell; i.e. (,) doesn't count. I've failed to either come up with any examples or prove that they all must be the same using the laws.
Thanks, Luke
A related question would be: are there two abstractions whose underlying representations (as algebraic data types) are isomorphic? For example, suppose that we represented both lists and sets as [a]. One would expect the Functor instances for list and set to be different, since sets can't contain duplicates. Unfortunately, it's not possible to express this in Haskell, because we can't assume an Eq constraint when defining our Functor instance. I suspect that the answer to the question is, yes, you can have different Functor instances. All you need is a sum-product type that it's possible to interpret as two different abstractions, leading to two different Functor instances.
DavidA wrote:
I suspect that the answer to the question is, yes, you can have different Functor instances. All you need is a sum-product type that it's possible to interpret as two different abstractions, leading to two different Functor instances.
The sum-product types are exactly the "not-too-exotic" types to which my proof applies. So as long as extensional equivalence means Haskell equivalence, and not some "modulo an interpretation" equivalence (like considering two lists equivalent if they contain the same elements but in potentially different order), the answer is no, one cannot have different funtor instances. Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de
Janis Voigtlaender
DavidA wrote:
I suspect that the answer to the question is, yes, you can have different Functor instances. All you need is a sum-product type that it's possible
to
interpret as two different abstractions, leading to two different Functor instances.
The sum-product types are exactly the "not-too-exotic" types to which my proof applies. So as long as extensional equivalence means Haskell equivalence, and not some "modulo an interpretation" equivalence (like considering two lists equivalent if they contain the same elements but in potentially different order), the answer is no, one cannot have different funtor instances.
Ciao, Janis.
Okay, I see. Well that's interesting, because it suggests that your proof might break under modest extensions to the language. The thing that led me to suggest list / set as an example was consideration of Data.Set. Conceptually, this should be a Functor instance - given f :: a -> b, we should be able to derive fmap f :: Data.Set a -> Data.Set b, eg fmap f xs = (fromList . map f . toList) xs However, we can't currently express this in Haskell, because Data.Set requires Ord a. However, there have been some proposals to fix this. I assume that if they went through, then it would be possible to define a type which could be interpreted as either a list or a set, with different functor instances in either case.
DavidA wrote:
Okay, I see. Well that's interesting, because it suggests that your proof might break under modest extensions to the language.
Yes. The free theorem used was a "naive" one, for the simplest possible model of Haskell, not even taking care of possible nontermination and seq. But http://linux.tcs.inf.tu-dresden.de/~voigt/ft/ can produce less naive ones as well. In particular, it can also produce free theorems for types involving class constraints, like Eq or Ord. That would deal with situations where the type variables a and b in the type of fmap were class-constrained, as you suggest. And finally, another plug: explanations for precisely the kind of type-based reasoning I used in the earlier mail can be found in the thesis I advertised today on the general list: http://wwwtcs.inf.tu-dresden.de/~voigt/habil.pdf Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de
participants (4)
-
Claus Reinke -
DavidA -
Janis Voigtlaender -
Luke Palmer