Support monads

[goldfirere]

We're surprisingly close to being able to support monads (and, with them, list comprehensions). Singletonizing the basic class definitions works. But there's danger on the horizon.

The problem has all to do with CUSKs. As Note [CUSKification] in Promote describes, we have little control over when GHC infers a CUSK. And this causes havoc when we want GHC to infer the kind of higher-kinded type variables. Specifically, the PFunctor class has a CUSK, and so the user needs to write class Functor (f :: * -> *). Putting in the kind annotations here isn't so, so terrible.

What's worse is that we run into similar problems elsewhere. I haven't tracked down the precise details, but compiling Base.hs on the monads branch led to an error where a defunctionalization symbol has a CUSK, and thus inferring that a kind variable should be higher-kinded fails.

Short of fixing CUSKs in GHC, the solution might be to emit GADT-style declarations of defunctionalization symbols instead of H98-style. This would allow us finer control of whether we have a CUSK. (Recall that, with TypeInType, all kind variables must be explicitly quantified in order to have a CUSK. So we just won't do that.) This is tantalizingly close. But I'm not going to get there tonight.

Checklist:

• Add Functor, Applicative, Monad, Alternative, MonadPlus, and MonadZip classes, as well as supporting functions. (Fix #184 by adding support for monads  #314)
• Add Identity, Const, Foldable, and Traversable, as well as supporting functions. (Promote and single Foldable, Traversable, Const, and Identity #337)
• Add support for deriving Functor, Foldable, and Traversable. (Support deriving Functor, Foldable, and Traversable #344)

[RyanGlScott]

If we're adding an Applicative class as part of this work, then we'll need this instance:

instance Monoid a => Applicative ((,) a)

But currently, we don't have a Monoid (or Semigroup) class within singletons. Adopting GHC 8.4 is good timing for this, now that Semigroup has become a superclass of Monoid, making adding the two in tandem much easier.

[RyanGlScott]

Also, if we're going to be adding Control.Monad at some point, then we'll need to implement Foldable/Traversable as well, since it's required by the function:

mapM :: (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b)

Which is re-exported from Control.Monad.

Of course, Foldable and Traversable might suffer from the same higher-kinded, defunctionalization-related CUSK issues mentioned in #184 (comment), so perhaps that's out-of-reach for the time being. But one thing we can do in preparation for their eventual arrival is to add the Identity and Const newtypes:

newtype Identity a = Identity { runIdentity :: a }
newtype Const a (b :: Type) = Const { getConst :: a } -- Kind-restricted

Why would we need these? Because they're used in two definitions in Data.Traversable:

fmapDefault :: forall t a b . Traversable t => (a -> b) -> t a -> t b
fmapDefault f = runIdentity . traverse (Identity . f)

foldMapDefault :: forall t m a . (Traversable t, Monoid m) => (a -> m) -> t a -> m
foldMapDefault f = getConst . traverse (Const . f)

(Plus, Const is re-exported from Control.Applicative.)

As far as I know, nothing is blocking us from adding Identity or Const, so that might be good intermediate step.

[RyanGlScott]

Also, I figured out what CUSK issue you're referring to. Here's a minimized example:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -ddump-splices #-}
module Bug where

import Data.Kind
import Data.Singletons.TH

$(singletons
    [d| class App (f :: * -> *) where
          (**>) :: f a -> f b -> f b
      |])

This generates the following defunctionalization data type:

data (:**>$$) (l1 :: f a) (l2 :: TyFun (f b) (f b)) where ...

About which GHC complains:

Bug2.hs:13:1: error:
    You have written a *complete user-suppled kind signature*,
    but the following variable is undetermined: k0 :: *
    Perhaps add a kind signature.
    Inferred kinds of user-written variables:
      a :: k0
      f :: k0 -> *
      b :: k0
      l1 :: f a
      l2 :: TyFun (f b) (f b)
   |
13 | data (:**>$$) (l1 :: f a) (l2 :: TyFun (f b) (f b)) where
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

It turns out, though, that there is a way to hack around this:

$(singletons
    [d| class App (f :: * -> *) where
          (**>) :: (f :: * -> *) a -> f b -> f b
      |])

That's somewhat unsightly, but it's a serviceable workaround.

[RyanGlScott]

Pull request #314 adds the Functor, Applicative, and Monad classes.

I'll work on adding Foldable and Traversable (and thus Const and Identity) separately.

[RyanGlScott]

Although Monad and its immediate immediate family have been implemented, there are some remaining loose ends to tie up.

[RyanGlScott]

Pull request #337 is about the second bullet point (Foldable, Traversable, Const, and Identity).

[RyanGlScott]

Finally, #344 implements the last bullet point (DeriveFunctor, DeriveFoldable, and DeriveTraversable).