Pre-Proposal: Implication instances

This post is inspired by this recent complaint Martin Escardo: "{- I think I am going to teach Haskell monads lik…" - Mathstodon

Monad is currently defined like this:

class Applicative m => Monad m where
  (>>=) :: m a -> (a -> m b) -> m b
  return :: a -> m a

But really, we’d like to say that each Monad instance implies an Applicative instance. Like this:

class Monad m where
  (>>=) :: m a -> (a -> m b) -> m b
  return :: a -> m a
instance Monad m => Applicative m

I’d argue we want to write such instance implications like this, because they are more intuitive in my opinion or if you don’t agree then at least it means we wouldn’t have to also write instances for Applicative and Functor manually.

But this wreaks havoc (in the form of overlapping instances). For example if you now tried to write an Applicative instance for a type manually. For example:

newtype ZipList a = ZipList [a]

instance Applicative ZipList where
  pure x = ZipList (repeat x)
  ZipList fs <*> ZipList xs = ZipList (zipWith ($) fs xs)

foo :: ZipList ()
foo = pure ()

You get an error like this:

T.hs:24:7: error: [GHC-43085]
    • Overlapping instances for Applicative ZipList
        arising from a use of ‘pure’
      Matching instances:
        instance Monad m => Applicative m -- Defined at T.hs:8:10
        instance Applicative ZipList -- Defined at T.hs:16:10
    • In the expression: pure ()
      In an equation for ‘foo’: foo = pure ()
   |
24 | foo = pure ()
   |       ^^^^

So it cannot choose between the implication instance and the manually written instance. But there is an easy solution to that: just require the user to explicitly state that no monad instance can ever be defined:

instance Unsatisfiable (Text "ZipList has no Monad instance") => Monad ZipList

This way the compiler can know that the implication instance cannot be used to get an instance for ZipList and can safely commit to the manually written instance. This does require the unsatisfiable instance to be in the same module as the Applicative instance. A bare Applicative instance without an accompanying unsatisfiable Monad instance should not be allowed.

In general my proposal is to add a special kind of “implication instance” of the form:

implication instance C1 a => C2 a

And require that each manual instance of the superclass (e.g. Applicative) would be accompanied by an unsatisfiable subclass (e.g. Monad) instance.

Some pre-emptive Q&As:

  • Q: If the implication instance is defined later in another module that could break existing instances. What should be done about that?
    A: Only allow implication instances in the same module as the two type classes that are involved.

  • Q: For some instances we can define a more performant implementation than the standard instance generated by implication from a subclass. Would that still be possible?
    A: I’d say yes, these should be definable as usual but only in the same module as the subclass instance.

  • Q: How does this interact with deriving?
    A: I haven’t given it too much thought. I think most derived instances can be allowed without problems because they should be unique (except for GeneralizedNewtypeDeriving, DerivingVia, and DeriveAnyClass). But I think there would be little reason to use derived instances in addition to the implied instances you get automatically.

  • Q: Wouldn’t this be a massive breaking change?
    A: Yes, sadly. Perhaps that’s enough reason to not change Monad in base in the foreseeable future. But we could still use this in alternative preludes.

  • Q: Can’t we make the unsatisfiable instance implicit?
    A: Yes, but I think that would be surprising behavior.

  • Q: How does this interact with MultiParamTypeClasses and FunctionalDependencies?
    A: I don’t know yet.

Here’s a full example of my proposed syntax:

class Functor f where
  fmap :: (a -> b) -> f a -> f b

class Applicative f where
  pure :: a -> f a
  (<*>) :: f (a -> b) -> f a -> f b

implication instance Applicative f => Functor f where
  fmap f x = pure f <*> x

class Monad m where
  (>>=) :: m a -> (a -> m b) -> m b
  return :: a -> m a

implication instance Monad m => Applicative m where
  pure = return
  p <*> q = p >>= \f -> q >>= \x -> return (f x)

-- Example instance

data List a = Nil | Cons a (List a)

append :: List a -> List a -> List a
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

-- We get 'instance Functor List' and 'instance Applicative List' for free

instance Monad List where
  return x = Cons x Nil
  Nil >>= _ = Nil
  Cons x xs >>= k = append (k x) (xs >>= k)

-- Example non-superclass instance

newtype ZipList a = ZipList [a]

-- We get 'instance Functor ZipList' for free

instance Applicative ZipList where
  pure x = ZipList (repeat x)
  ZipList fs <*> ZipList xs = ZipList (zipWith ($) fs xs)

instance Unsatisfiable (Text "ZipList has no Monad instance") => Monad ZipList

foo :: ZipList ()
foo = pure () -- no error

This reminds me of

2 Likes

Those seem quite a bit more complicated than my proposal and they seem to have a slightly different goal in mind. For example, my proposal truly decouples the definition of Monad from the definition of Applicative. Only the external implication instance mentions both. Still, those two proposals seem very well thought out so I should look into how their requirements mesh with my proposal.

I am now also thinking of a different implementation strategy that doesn’t require defining all the classes and instances in one place and avoids having to manually write the unsatisfiable instances: just do backtracking search for these implication instances. I think their restricted form means that you never get into poor efficiency cases and the open world assumption also does not influence the correctness in these cases. But I should think more about this tomorrow with a fresh mind.

1 Like

I am a dum-dum; how would this work?

My expectation is that GHC would only look at the two available Monad instances with matching heads and then complain about the overlap, not that it would try both, notice that one of them leads to needing to solve an Unsatisfiable constraint, and then happily select the other. I skimmed the Unsatisfiable proposal but didn’t see anything there about backtracking. Your most recent comment suggests backtracking search as an alternate implementation strategy for implication instances but how would this work without introducing backtracking? Or am I missing something else about how GHC does instance search?

My original idea was to change GHC’s instance search such that it would keep a list of implication instances and a list of unsatisfiable instances. Then it would only try using implication instances if the premise is not unsatisfiable.

I now think backtracking (without explicit unsatisfiable instances) would work pretty much as well, but it would be more implicit for better or for worse.

The real remaining issue is that of manually overriding instances. That can be done for performance reasons, or to make them more general. However, a naive backtracking solver would not be able to give guarantees about which instance is picked.

You could say this is incoherent in general, but in the current system there is already room for semantic inconsistency due to the Applicative and Monad instances not aligning, e.g. p <*> q = p >>= \f -> q >>= \x -> return (f x) is not checked by the compiler. So if implication instances cause incoherence then that means your instances are not lawful. Theoretically this is not a problem.

But still, a straightforward backtracking search does not give us a guarantee that we always choose the most specific (and probably most performant) instance. Consider this example:

foo :: Monad m => m ()
foo = pure ()

We can always resolve the Applicative instance arising from pure using the implication instance from the given Monad m constraint, but there might be a more efficient implementation depending on which m is passed at run time (for pure this is very unlikely but this is just a simplified example).

The current system solves this issue by embedding the Applicative instance inside the Monad instance. After desugaring we would end up with a dictionaries like this:

data Functor f = Functor { fmap :: (a -> b) -> f a -> f b }
data Applicative f = Applicative { functor :: Functor f, pure :: a -> f a, apply :: f (a -> b) -> f a -> f b }
data Monad m = Monad
  { applicative :: Applicative m
  , return :: a -> m a
  , bind :: m a -> (a -> m b) -> m b
  }

So you can always extract the more specific Applicative dictionary from the Monad dictionary.

To resolve this issue with implication instances, we can choose the exact same implementation strategy. The only requirement then is that implication instances are located in the same module as the premise class declaration. So you’d have to write class Monad m where ... in the same module as implication instance Monad m => Applicative m.

I’m starting to see that the default superclass instances proposal is more similar to what I’m proposing here than I gave it credit for.

Still, I’d propose a few changes:

  • Decouple the superclasses completely so that the definition of Monad does not refer to Applicative at all. Unfortunately, as I tried to explain in my last comment this does mean that the implication instance still must be in the same module as the class for guarantees about instance selection. But I think the conceptual separation is worth it.

  • Do more implicitly. The default superclass instances requires users to explicitly hide instances in some cases, because:

    This quiet exclusion policy is not enough to handle the case of multiple candidate intrinsic instances arising from multiple intrinsic superclasses (e.g., Traversable and Monad giving competing Functor instances), so some explicit hiding form is required even under the “silent pre-emption” plan.

    I don’t agree with this. The solver can simply pick one of them arbitrarily. As I tried to explain in my previous comment, the type class laws ensure coherence. So, I think no explicit opt-out is necessary at all.

All well and good when the shared superclass is Functor. But is the below program valid, and if so, what does it print? If it is invalid due to overlapping instances, is there going to be a special case that recognizes Functor-derived classes like Monad and Traversable as not conflicting?

class Alpha a where
  alpha :: a -> String

class Bravo a where
  bravo :: a -> a -> String

implication instance Bravo a => Alpha a where
  alpha a = bravo a a

class Charlie a where
  charlie :: [a] -> String

implication instance Charlie a => Alpha a where
  alpha a = charlie [a]

data Foo = Foo

instance Bravo Foo where
  bravo _ _ = "bravo"

instance Charlie Foo where
  charlie _ = "charlie"

-- What does this print?
main :: IO ()
main = putStrLn $ alpha Foo

It’s invalid because the laws are violated. The implication instance induces the laws:

alpha a = bravo a a
alpha a = charlie [a]

But the instances don’t satisfy these laws.

Here’s a similar program that you can write with Applicative and Travesable:

implication instance Applicative a => Functor a where
  fmap f x = pure f <*> x

implication instance Traversable a => Functor a where
  fmap f x = runIdentity (traverse (Identity . f) x)

data Foo a = Foo String deriving Show

instance Applicative Foo where
  pure _ = Foo "applicative"
  _ <*> _ = Foo "apppicative"

instance Travesable Foo where
  traverse _ _ = pure (Foo "traversable")

-- What does this print?
main :: IO ()
main = putStrLn $ fmap id (Foo "")

…isn’t the only one about the Functor => Applicative => Monad (re)arrangement: e.g. from slide 18 of 29 of Monads and Interaction: Lecture 1:


…was F-A-M really worth it for teaching or industrial Haskell? Or are there more examples like:

There is no fork: an Abstraction for Efficient, Concurrent, and Concise Data Access (2014)

…which educators can then use to justify the added complexity?

Alternatively, is there another proposal somewhere to make these classes independent of each other, much like how Num has been independent of Eq and Show since GHC 7.4? At least then people can decide which instances are actually necessary, rather that being required to define all of them…

Hrm:

Just out of curiosity: having seen this post…was ApplicativeDo one of the “selling points” of the F-A-M transition? The restrictions needed to use it does seem (to me, anyway) to provide further evidence against that proclamation.

That’s hugely a matter of opinion. I can think of plenty of uglier things in GHC 7.10. And I still use Hugs which never went in for the class rearrangements. I find nothing ugly.