23

A recent question asked generally about boundaries between various Haskell classes. I came up with Handler as an example of a valid Functor with no sensible instance of Apply**, where

class Functor f => Apply f where
  (<.>) :: f (a -> b) -> f a -> f b
  -- optional bits omitted.

However, I've not yet been able to find an example of a valid Functor that cannot be made a valid (if senseless) instance of Apply. The fact that Apply has had (see update) but a single law,

(.) <$> u <.> v <.> w = u <.> (v <.> w)

seems to make this rather tricky.

pigworker (Conor McBride) previously gave an example of a Functor that is not Applicative, but he relied on pure to do so, and that's not available in Apply.

** Then later I realized there actually might be a sensible (although slightly strange) Apply instance for Handler, that conceptually collects simultaneous exceptions.


Update

Edward Kmett has now accepted two additional laws I proposed for Apply (to validate optimizations I made to the Apply (Coyoneda f) instance):

x <.> (f <$> y) = (. f) <$> x <.> y
f <$> (x <.> y) = (f .) <$> x <.> y

It would be interesting to see whether these additions change the answer to this question.

Community
  • 1
  • 1
dfeuer
  • 48,079
  • 5
  • 63
  • 167
  • Forgive my ignorance, but what's `Apply` _for_, exactly? It seems far less useful than `Applicative` because `Apply` lacks a unit: when you're smashing things together, you typically want something to smash them into. – Benjamin Hodgson Mar 29 '16 at 22:36
  • 2
    @BenjaminHodgson, sometimes there isn't one. Notable examples (see the documentation for `Apply`) include `Map k` and `IntMap`, but also, e.g., `Const (NonEmpty a)`. – dfeuer Mar 29 '16 at 22:40
  • 2
    Taking the "functors as containers" analogy, it *seems* like one should always be able to implement `Apply`: simply count up the number of contained elements in the two arguments, pick the container shape of the smaller one (on ties defaulting, say, left), and fill in the container entries in a zip-y way. But this is just an intuition, I'm afraid, not a proof. – Daniel Wagner Mar 30 '16 at 01:10
  • @DanielWagner, based on the blog post [Functors are Containers](http://bartoszmilewski.com/2014/01/14/functors-are-containers/) by Bartosz Milewski, along with your latest comment, one potentially promising choice of functor might be an infinite sum of infinite products, where (somehow) comparison of cardinalities among the cases is never computable. So there'd be no way to come up with an injection from one argument to the other, or to choose something smaller than both. This is all very hand-wavy, of course, and departs the nice world of inductive types. – dfeuer Mar 30 '16 at 02:27
  • @DanielWagner How do you zip together `(Real -> a)` and `((Real -> Bool) -> a)`? – Cirdec Apr 01 '16 at 15:52
  • @Cirdec, I believe you do it by producing an injection from `Real` to `Real -> Bool`, assuming that's possible in Haskell. – dfeuer Apr 01 '16 at 16:12
  • @Cirdec For example: `combine :: (a -> b -> c) -> (Real -> a) -> ((Real -> Bool) -> b) -> (Real -> c); combine with f g = \r -> with (f r) (g (r ==))`. Substitute your favorite decidable function of type `Real -> Real -> Bool` if you don't believe `(==)` is decidable -- even `\_ _ -> False` if absolutely necessary. – Daniel Wagner Apr 01 '16 at 20:21

3 Answers3

10

The "sum" of two functors (Data.Functor.Sum from transformers) seems to be an example.

One can easily map over one branch or the other, but how to implement <.> when the function-in-the-functor and the argument-in-the-functor lie in different branches?

ghci> import Data.Functor.Sum
ghci> import Data.Functor.Identity
ghci> let f = InL (Const ())   :: Sum (Const ()) Identity (Int -> Int)
ghci> let x = InR (Identity 5) :: Sum (Const ()) Identity Int
ghci$ f <.> x = ..... ?
danidiaz
  • 26,936
  • 4
  • 45
  • 95
  • 5
    `Const ()` is a bad choice, because `Sum (Const ()) f` is isomorphic to `Compose Maybe f`, which has a perfectly good `Apply` instance whenever `f` does. But this should work with a *non-constant* left branch. – dfeuer Mar 29 '16 at 23:26
  • 4
    A hypothesis: it is not possible to implement `instance (Apply f, Apply g) => Apply (Sum f g)`; but for any choice of `f` and `g` that are instances of `Apply` it is possible to implement `instance Apply (Sum f g)`. – Daniel Wagner Mar 30 '16 at 00:22
  • @DanielWagner, that sounds plausible, but it would take considerably more theory than I know to prove it if it's true. Falsifying it will probably be easier, if it's false. – dfeuer Mar 30 '16 at 00:26
  • 2
    For `Apply` `f` and `g`, `Sum f g` is `Apply` if there exists an `Apply` homomorphism from `f` to `g` or the other way. Source: exercise 1.21 on page 19 [here](https://www.cs.ox.ac.uk/projects/utgp/school/conor.pdf) asks for an analogous proof for `Applicative`, which is easily adapted for `Apply`. – András Kovács Mar 30 '16 at 08:38
  • @AndrásKovács But this question is about the other direction: when is `Sum f g` patently *not* `Apply`? I doubt very much you can claim that this holds when neither `f` nor `g` has an `Apply` homomorphism to the other -- i.e. I suspect you can argue only that the "obvious" way to instantiate `Apply` doesn't work, not that all ways to instantiate `Apply` don't work. – Daniel Wagner Apr 01 '16 at 20:23
  • @DanielWagner fair enough, I was just throwing this out as something potentially relevant. – András Kovács Apr 01 '16 at 21:15
  • @dfeuer On the other hand, Falsifying it will probably be extremely difficult if it turns out to be true. XD – PyRulez Apr 19 '16 at 00:42
10

Yes, there are Functors with no Apply instance. Consider the sum of two functions (which are exponents in algebraic data types):

data EitherExp i j a
    = ToTheI (i -> a)
    | ToTheJ (j -> a)

There's a Functor instance for all is and js:

instance Functor (EitherExp i j) where
    fmap f (ToTheI g) = ToTheI (f . g)
    fmap f (ToTheJ g) = ToTheJ (f . g)

but there's no Apply instance for all is and js

instance Apply (EitherExp i j) where
    ...
    ToTheI f <.> ToTheJ x = ____

There's no way to fill in the blank ____ with an i -> b or a j -> b when all you have is f :: i -> a -> b and x :: j -> a. To do so we'd have to know something about i and j, but there's no way to look inside every type i or j in Haskell. Intuition rejects this answer; if you know anything about i or j, like that they are inhabited by a single value, then you can write an Apply instance for EitherExp

class Inhabited a where
    something :: a

instance (Inhabited i, Inhabited j) => Apply (EitherExp i j) where
    ...
    ToTheI f <.> ToTheJ x = ToTheI (const ((f something) (x something)))

But we don't know that every i and every j is Inhabited. The Void type isn't inhabited by anything. We don't even have a way to know that every type is either Inhabited or Void.

Our intuition is actually very good; when we can inspect how types are constructed, for algebraic data types there are no Functors that don't have Apply instances. What follow are two answers that might be more pleasing to our intuition.

No ...

... for algebraic data types. There are 3 possibilities. The structure is void, the structure can be empty, or the structure can't be empty. If the structure is void then it's absurdly an Apply. If it can be empty, chose any empty instance and return it constantly for any apply. If it can't be empty then it's a sum of structures that each can't be empty, a law-abiding apply can be made by applying one of the values from the first to one of the values from the second and returning it in some constant structure.

The apply law is very lax. Apply doesn't need to make any sense. It doesn't need to be "zip-y". It doesn't need to be fmap when combined with things suspiciously like pure from Applicative; there's no notion of pure with which to write a law requiring it to make sense.

When the structure can be empty

Chose any empty instance and return it constantly for any apply

u <.> v = empty

Proof

  (.) <$> u  <.> v  <.> w = u <.> (v <.> w)
(((.) <$> u) <.> v) <.> w = u <.> (v <.> w) -- by infixl4 <$>, infixl4 <.>
(_                ) <.> w = u <.> (_      ) -- by substitution
                    empty = empty           -- by definition of <.>

When the structure can't be empty

If the structure f can't be empty, there exists a function extract :: forall a. f a -> a. Choose another function c :: forall a. a -> f a that always constructs the same non-empty structure populated with the argument everywhere and define:

u <.> v = c (extract u $ extract v)

With the free theorems

extract (f <$> u) = f (extract u)
extract . c = id

Proof

  (.) <$> u  <.> v  <.> w = u <.> (v <.> w)
(((.) <$> u) <.> v) <.> w = u <.> (v <.> w) -- by infixl4 <$>, infixl4 <.>
(c (extract ((.) <$> u) $ extract v)) <.> w = u <.> (v <.> w) -- by definition
(c ((.) (extract u)     $ extract v)) <.> w = u <.> (v <.> w) -- by free theorem 
c (extract (c ((.) (extract u) $ extract v)) $ extract w) = u <.> (v <.> w) -- by definition
c (           ((.) (extract u) $ extract v)  $ extract w) = u <.> (v <.> w) -- by extract . c = id
c (((.) (extract u) $ extract v) $ extract w) = u <.> c (extract v $ extract w) -- by definition
c (((.) (extract u) $ extract v) $ extract w) = c (extract u $ extract (c (extract v $ extract w))) -- by definition
c (((.) (extract u) $ extract v) $ extract w) = c (extract u $            (extract v $ extract w) ) -- by extract . c = id
let u' = extract u
    v' = extract v
    w' = extract w
c (((.) u' $ v') $ w') = c (u' $ (v' $ w'))
c ((u' . v') $ w') = c (u' $ (v' $ w')) -- by definition of partial application of operators
c (u' $ (v' $ w')) = c (u' $ (v' $ w')) -- by definition of (.)

A little more deserves to be said about defining extract for the exponential types, functions. For a function i -> a there are two possibilities. Either i is inhabited or it isn't. If it is inhabited, choose some inhabitant i and define

extract f = f i

If i is uninhabited (it's void) then i -> a is the unit type with the single value absurd. Void -> a is just another elaborate empty type that doesn't hold any as; treat it as a structure that can be empty.

When the structure is void

When the structure is void there are no ways to construct it. We can write a single function from every possible construction (there are none to pass to it) to any other type.

absurd :: Void -> a
absurd x = case x of {}

Void structures can be Functors with fmap f = absurd. In the same way they can have an Apply instance with

(<.>) = absurd

We can trivially prove that for all u, v, and w

(.) <$> u  <.> v  <.> w = u <.> (v <.> w)

There are no u, v, or w and the claim is vacuously true.


With some caveats about accepting the axiom of choice to choose an index a for the exponential type a -> b


Yes ...

... for Haskell. Imagine there's another base Monad other than IO, let's call it OI. Then Sum IO OI is a Functor but can never be an Apply.

... for the real world. If you have a machine to which you can send functions (or arrows in a category other than Hask), but cannot combine two of the machines together or extract their running state, then they are a Functor with no Apply.

Cirdec
  • 24,019
  • 2
  • 50
  • 100
  • 1
    Here is a value that is neither inhabited nor isomorphic to `Void`: `forall a. Either a (a -> Void)`. This is because Haskell's type system corresponds for the most part to intuitionistic logic. Intuitionistic logic specifically lacks that statement as an axiom or theorem, but since it is a subset of classical logical it doesn't contain its negation either. – PyRulez Apr 19 '16 at 00:47
  • @PyRulez, I wouldn't be surprised if Haskell were anti-classical. That is, I wouldn't be surprised if you *could* refute that. Certainly, Idris can refute it, and earlier versions of Agda. Agda tweaked things a bit to be consistent with the excluded middle. – dfeuer Apr 19 '16 at 00:53
  • @dfeuer How do you refute it in Idris? – PyRulez Apr 19 '16 at 00:55
  • @PyRulez, it's complicated and I don't understand it. It's some sort of diagonal argument, IIRC. I think David Christiansen translated it from Agda. – dfeuer Apr 19 '16 at 01:10
  • @PyRulez Interesting. I debated pointing out that this requires accepting the law of the excluded middle as well as the axiom of choice, but decided that was too trivial to be worth mentioning. I was wrong. – Cirdec Apr 19 '16 at 02:18
  • @Cirdec Feel free to implement it into your answer if you feel so inclined. – PyRulez Apr 19 '16 at 02:21
  • You may want to check whether/how the new state of affairs described in my update affect this answer. – dfeuer May 19 '16 at 15:21
  • @dfeuer The proofs for the new laws are trivial for empty data-structures if we notice that `f <$> empty = empty`. The laws for non-empty structures can be proven simply by using `Identity . extract` in place of `extract`, `c . runIdentity` in place of `c` and appealing to the proofs for `Identity`. – Cirdec May 19 '16 at 17:45
  • As an example of why the law-abiding `Apply` would sometimes make little practical sense, consider the functor `type A a = Either a (a, a)`. This is an example of a "data structure that is always non-empty". Also this is an example of a sum of two functors where there exists a natural transformation from one to the other. However, zipping two values of this functor will discard some data and so makes little intuitive sense: Right (x,y) `zip` Left(z) = Left((x,z)). We have discarded `y` here. – winitzki Apr 10 '18 at 20:23
  • @winitzki It's worse than that. The law-abiding apply I describe is essentially `Right (x,y) \`zip\` Right (a, b) = Left ((x, a))`. – Cirdec Apr 10 '18 at 20:40
  • This reminds me of the correspondence (Applicative - Monoid) / (Apply - Semigroup). Compared to Monoid, Semigroup is missing the identity and its laws. So there are lots of semigroups, but far fewer monoids. Any type `a` is a semigroup with a definition of `combine` such as: a `combine` b = a, discarding one of the arguments. There are, however, use cases for this kind of thing. – winitzki Apr 10 '18 at 22:32
4

This isn't exactly what you're looking for, but it's close so I thought I'd share it. The standard Writer monad has an extra constraint on its Apply instance (namely, that the w type be an instance of Monoid or Semigroup) that the Functor instance does not, so that Writer Foo is a Functor but not Apply if Foo is not a Semigroup/Monoid:

data Writer w a = Writer w a

instance Monoid w => Apply (Writer w) where
  Writer w1 f <.> Writer w2 x = Writer (mappend w1 w2) (f x)

However, this isn't really an example of what you're asking for, because it's actually possible to create a law-abiding instance of Apply without a Monoid constraint:

instance Apply (Writer w) where
  Writer w1 f <.> Writer w2 x = Writer w1 (f x)

The problem with this instance is that it does not allow for a matching Applicative instance, since there would be no way to implement pure such that you get a left identity, that is:

pure id <.> x /= x

This is just a long-ish way of giving you the same answer you already had from Conor: a demonstration that relies on pure to break the instance.

Michael Snoyman
  • 31,100
  • 3
  • 48
  • 77
  • I was mostly curious about whether there is a *specific* functor (i.e., a type constructor) of this sort. That said, a result about constraints on a parameterized one could be interesting, if you were able to produce one. – dfeuer Mar 30 '16 at 15:48