Re: [Haskell-cafe] Unique functor instance
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:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Unique functor instance
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:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Unique functor instance
Are identity and composition sufficient to guarantee that the mapped function is actually applied? eek - f :: a -> b, not f :: a -> a, so that example doesn't work !! Sorry for the noise, Claus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Unique functor instance
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Unique functor instance
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:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Unique functor instance
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:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
